7 ms·

I like how the author boils the idea down into a simple comparison between two alternative approaches to a simple task: getting the first element of a list. Two

I like how the author boils the idea down into a simple comparison between two alternative approaches to a simple task: getting the first element of a list. Two alternatives are presented: parseNonEmpty and validateNonEmpty. From the article: > The difference lies entirely in the return type: validateNonEmpty always returns (), the type that contains no information, but parseNonEmpty returns NonEmpty a, a refinement of the input type that preserves the knowledge gained in the type system. Both of these functions check the same thing, but parseNonEmpty gives the caller access to the information it learned, while validateNonEmpty just throws it away. This might not seem like much of a distinction, but it has far-reaching implications downstream: > These two functions elegantly illustrate two different perspectives on the role of a static type system: validateNonEmpty obeys the typechecker well enough, but only parseNonEmpty takes full advantage of it. If you see why parseNonEmpty is preferable, you understand what I mean by the mantra “parse, don’t validate.” parseNonEmpty is better because after a caller gets a NonEmpty it never has to check the boundary condition of empty again. The first element will always be available, and this is enforced by the compiler. Not only that, but functions the caller later calls never need to worry about the boundary condition, either. The entire concern over the first element of an empty list (and handling the runtime errors that result from failure to meet the boundary condition) disappear as a developer concern.

waynesonfire 4y ago
Does this scale? What if you have 10 other conditions?
- ElevenLathe 4y ago
  I think what you're getting at is that it seems ponderous to have types named things like NonEmptyListWhereTheThirdElementIsTheIntegerFourAndTheOtherElementsAreStringsOfLengthSixOrUnder and the answer is that you shouldn't do that, but instead name it something in the problem domain (of whatever the program is about) like WidgetDescription or whatever.
  - tialaramex 4y ago
    And naming is actually a valuable activity. Knowing this is not merely NonEmptyListWhereTheThirdElementIsTheIntegerFourAndTheOtherElementsAreStringsOfLengthSixOrUnder but actually WidgetDescription is a valuable insight. Deciding this thing is specifically a WidgetDescription, not a Widget or a WidgetLabel, or a WidgetAssociatedText and definitely not a ThingyDescription, can help both users and other developers produce a mental model of what's going on that results in a better experience for everyone.
  - dwohnitmok 4y ago
    No the trickier problem is that without dependent types you are forced into a very specific, linear chain of validation or else deal with a combinatorial explosion of functions and types. To take your type as an example, you could imagine a function validation : String -> Maybe FinalWidget but maybe `validation` is really big and unwieldy and you want to reuse parts of it elsewhere so you break it down into a pipeline of -- Let's say a RawWidget is, operationally, a non-empty string validation0 : String -> Maybe RawWidget -- Let's say a RefinedWidget is a string consisting only of capital letters validation1 : RawWidget -> Maybe RefinedWidget -- A FinalWidget is a non-empty string of capital letters that has no whitespace validation2 : RefinedWidget -> Maybe FinalWidget This is over-constrained. You don't really want to force yourself into a scenario where you must call validation0, then validation1, and finally validation2 because maybe in another code path it's more expedient to do it in another order. But the types don't line up if you do it in another order. And maybe you don't really care about `RawWidget` and `RefinedWidget`, but you're forced to create them just to make sure that you can build up to a `FinalWidget`. This is where dependent types would really help relax those constraints.
    - Quekid5 4y ago
      I don't disagree that dependent types would help (and be really cool for lots of other uses!), but let's consider what the usual validation rules that we really need are: non-empty, basic interval constraints (non-negative/positive), only contains a certain set of characters... simple stuff like that, usually. If we're going wild, an interesting case would be effectful validation and how that fits in. In practice, what happens with any non-basic validation is that the server says 3xx, try again. Anyway, validation/parsing is mostly pretty simple stuff where the "validate" bit is a simple function... and function composition works just fine. (Assuming you can name the result type of your parse/validate individually according to your domain.)
- dangets 4y ago
  I would think stacking 10 generic conditions wouldn't scale if you are trying to mix and match arbitrarily. If you are trying to mix NonEmpty and AllEven and AllGreaterThan100 for the List example, then you would get the combinatorial explosion of types. In practice, I find it is usually something like 'UnvalidatedCustomerInfo' being parsed into a 'CustomerInfo' object, where you can validate all of the fields at the same time (phone number, age, non-null name etc.). Once you have parsed it into the internal 'CustomerInfo' type - you don't need to keep re-validating the expected invariants everywhere this type is used. There was a good video on this that I wish I could find again, where the presenter gave the example of using String for a telephoneNumber field instead of a dedicated type. Any code that used the telephoneNumber field would have to re-parse and validate it "to be safe" it was in the expected format. The topic of having untrusted external types and internal trusted types is also explained in the book `Domain Modeling Made Functional` which I highly recommend.
  - hansvm 4y ago
    In Zig at least, the types-as-values framework means it'd be pretty easy to support arbitrary mixing and matching. If nobody beats me to it, I'll make a library to remove the boilerplate for that idea this weekend.
    - hansvm 4y ago
      https://github.com/hmusgrave/pdv https://github.com/hmusgrave/pdv
  - JamesSwift 4y ago
    You would also run into a form of "type erasure" in most cases and would need a combinatorial explosion of methods unless the type system was able to 'decorate' the generic parameter with additional information. e.g. imagine a `parseNonEmpty` and a `parseAllEven` method. Both take a list and return either a `NonEmpty` or `AllEven` type. If I call `parseNonEmpty` and get a `NonEmpty`, then pass to `parseAllEven`, I now have erased the `NonEmpty` as I'm left with an `AllEven`. I would need a `parseAllEvenFromNonEmpty` to take a `NonEmpty` and return a `AllEven & NonEmpty`.
  - 4y ago
- crvdgc 4y ago
  At least in Haskell this can be expressed as type classes. For each condition, you can create a (possibly empty) type class to guarantee that the condition is met. Then the call site type class constraints will be checked at compile time.
  - dwohnitmok 4y ago
    This doesn't really work because you still end up needing specific types for the output of every "parser" you have and then you still need a way of combining those types together. Or you get the ability to forge evidence (e.g. you use the evidence provided by a parser for one integer as evidence for another). This works better for dependency injection scenarios (the Has* pattern).
- layer8 4y ago
  The code size of the “parse” version of a program is at worst linear in the code size of the corresponding “validate” version, so I’d say yes.
- dwohnitmok 4y ago
  This is where dependent types would shine. function processUserInput(input: String, requirement: InputReqs[input]): Unit = ... type InputReqs[input] = { // We'll say that a Proposition takes Boolean expressions and turn them into types notTooLong: Proposition[length(input) < 128], authorIsNotBlocked: AuthorIsNotBlocked[input], sanitized: Sanitized[input], ... } where you might have the following functions (which are all examples of parse don't validate) function checkIfAuthorIsBlocked(author: String, input: String): Maybe[AuthorIsNotBlocked[input]] = ... // Create a pair that contains both the sanitized String and a tag that it has been sanitized function sanitizeString(input: String): (output: String, Sanitized[output]) = ... where just by types alone I know that e.g. length checking must occur after sanitization (because sanitizeString generates a new `output` that is distinct from `input`) and don't have to write down in docs somewhere that you might cause a bug if you check lengths before sanitization because maybe sanitization changes the length of the input. Note that this is also strictly stronger than a simple precondition/postcondition system or some sort of assertion system because properties of the input that we care about may not be observable at runtime/from the input alone (e.g. AuthorIsNotBlocked can't be asserted based only on input: you'd have to change the runtime representation of input to include that information).
- cdaringe 4y ago
  Somebody somewhere in system will be checking. At the boundary likely scales the best because you dont burn cycles that otherwise would be distributed and likely redundant in system. If you have a massive model, its feasible that it makes sense to defer partial/subparsing? Parser combinators seem to be pretty rippin fast for the most part, at least those ive used in ocaml and rust.
deleted 4y ago
[deleted]
epolanski 4y ago
Also, parsing composes, validating, doesn't. I once had to implement a feature on a real estate website. For a given location I would get a list of stats (demographics, cost per square meter, average salary in the area, etc). Of those stats some themselves contained lists. At the beginning I modeled everything with arrays in react. This led to passing down lists and having to check at multiple steps whether they were non-empty and handle that case. Then I modeled everything with a NonEmptyArray guard in TypeScript ``` interface NonEmptyArray<A> extends Array<A> { 0: A // tells the typesystem that index 0 exists and is of type A } function isNonEmpty(as: A[]): as is NonEmptyArray<A> { return as.length > 0 } ``` then after receiving the response with those lists I could parse them into NonEmptyArrays, remove all of the checks of emptiness inside the react components till handling the fact that some of these elements were empty trickled up to the outermost component and everything became very clean and simple to understand/maintain.

waynesonfire 4y ago

Does this scale? What if you have 10 other conditions?

ElevenLathe 4y ago
I think what you're getting at is that it seems ponderous to have types named things like NonEmptyListWhereTheThirdElementIsTheIntegerFourAndTheOtherElementsAreStringsOfLengthSixOrUnder and the answer is that you shouldn't do that, but instead name it something in the problem domain (of whatever the program is about) like WidgetDescription or whatever.
- tialaramex 4y ago
  And naming is actually a valuable activity. Knowing this is not merely NonEmptyListWhereTheThirdElementIsTheIntegerFourAndTheOtherElementsAreStringsOfLengthSixOrUnder but actually WidgetDescription is a valuable insight. Deciding this thing is specifically a WidgetDescription, not a Widget or a WidgetLabel, or a WidgetAssociatedText and definitely not a ThingyDescription, can help both users and other developers produce a mental model of what's going on that results in a better experience for everyone.
- dwohnitmok 4y ago
  No the trickier problem is that without dependent types you are forced into a very specific, linear chain of validation or else deal with a combinatorial explosion of functions and types. To take your type as an example, you could imagine a function validation : String -> Maybe FinalWidget but maybe `validation` is really big and unwieldy and you want to reuse parts of it elsewhere so you break it down into a pipeline of -- Let's say a RawWidget is, operationally, a non-empty string validation0 : String -> Maybe RawWidget -- Let's say a RefinedWidget is a string consisting only of capital letters validation1 : RawWidget -> Maybe RefinedWidget -- A FinalWidget is a non-empty string of capital letters that has no whitespace validation2 : RefinedWidget -> Maybe FinalWidget This is over-constrained. You don't really want to force yourself into a scenario where you must call validation0, then validation1, and finally validation2 because maybe in another code path it's more expedient to do it in another order. But the types don't line up if you do it in another order. And maybe you don't really care about `RawWidget` and `RefinedWidget`, but you're forced to create them just to make sure that you can build up to a `FinalWidget`. This is where dependent types would really help relax those constraints.
  - Quekid5 4y ago
    I don't disagree that dependent types would help (and be really cool for lots of other uses!), but let's consider what the usual validation rules that we really need are: non-empty, basic interval constraints (non-negative/positive), only contains a certain set of characters... simple stuff like that, usually. If we're going wild, an interesting case would be effectful validation and how that fits in. In practice, what happens with any non-basic validation is that the server says 3xx, try again. Anyway, validation/parsing is mostly pretty simple stuff where the "validate" bit is a simple function... and function composition works just fine. (Assuming you can name the result type of your parse/validate individually according to your domain.)
dangets 4y ago
I would think stacking 10 generic conditions wouldn't scale if you are trying to mix and match arbitrarily. If you are trying to mix NonEmpty and AllEven and AllGreaterThan100 for the List example, then you would get the combinatorial explosion of types. In practice, I find it is usually something like 'UnvalidatedCustomerInfo' being parsed into a 'CustomerInfo' object, where you can validate all of the fields at the same time (phone number, age, non-null name etc.). Once you have parsed it into the internal 'CustomerInfo' type - you don't need to keep re-validating the expected invariants everywhere this type is used. There was a good video on this that I wish I could find again, where the presenter gave the example of using String for a telephoneNumber field instead of a dedicated type. Any code that used the telephoneNumber field would have to re-parse and validate it "to be safe" it was in the expected format. The topic of having untrusted external types and internal trusted types is also explained in the book `Domain Modeling Made Functional` which I highly recommend.
- hansvm 4y ago
  In Zig at least, the types-as-values framework means it'd be pretty easy to support arbitrary mixing and matching. If nobody beats me to it, I'll make a library to remove the boilerplate for that idea this weekend.
  - hansvm 4y ago
    https://github.com/hmusgrave/pdv https://github.com/hmusgrave/pdv
- JamesSwift 4y ago
  You would also run into a form of "type erasure" in most cases and would need a combinatorial explosion of methods unless the type system was able to 'decorate' the generic parameter with additional information. e.g. imagine a `parseNonEmpty` and a `parseAllEven` method. Both take a list and return either a `NonEmpty` or `AllEven` type. If I call `parseNonEmpty` and get a `NonEmpty`, then pass to `parseAllEven`, I now have erased the `NonEmpty` as I'm left with an `AllEven`. I would need a `parseAllEvenFromNonEmpty` to take a `NonEmpty` and return a `AllEven & NonEmpty`.
- 4y ago
crvdgc 4y ago
At least in Haskell this can be expressed as type classes. For each condition, you can create a (possibly empty) type class to guarantee that the condition is met. Then the call site type class constraints will be checked at compile time.
- dwohnitmok 4y ago
  This doesn't really work because you still end up needing specific types for the output of every "parser" you have and then you still need a way of combining those types together. Or you get the ability to forge evidence (e.g. you use the evidence provided by a parser for one integer as evidence for another). This works better for dependency injection scenarios (the Has* pattern).
layer8 4y ago
The code size of the “parse” version of a program is at worst linear in the code size of the corresponding “validate” version, so I’d say yes.
dwohnitmok 4y ago
This is where dependent types would shine. function processUserInput(input: String, requirement: InputReqs[input]): Unit = ... type InputReqs[input] = { // We'll say that a Proposition takes Boolean expressions and turn them into types notTooLong: Proposition[length(input) < 128], authorIsNotBlocked: AuthorIsNotBlocked[input], sanitized: Sanitized[input], ... } where you might have the following functions (which are all examples of parse don't validate) function checkIfAuthorIsBlocked(author: String, input: String): Maybe[AuthorIsNotBlocked[input]] = ... // Create a pair that contains both the sanitized String and a tag that it has been sanitized function sanitizeString(input: String): (output: String, Sanitized[output]) = ... where just by types alone I know that e.g. length checking must occur after sanitization (because sanitizeString generates a new `output` that is distinct from `input`) and don't have to write down in docs somewhere that you might cause a bug if you check lengths before sanitization because maybe sanitization changes the length of the input. Note that this is also strictly stronger than a simple precondition/postcondition system or some sort of assertion system because properties of the input that we care about may not be observable at runtime/from the input alone (e.g. AuthorIsNotBlocked can't be asserted based only on input: you'd have to change the runtime representation of input to include that information).
cdaringe 4y ago
Somebody somewhere in system will be checking. At the boundary likely scales the best because you dont burn cycles that otherwise would be distributed and likely redundant in system. If you have a massive model, its feasible that it makes sense to defer partial/subparsing? Parser combinators seem to be pretty rippin fast for the most part, at least those ive used in ocaml and rust.

deleted 4y ago

[deleted]

epolanski 4y ago

Also, parsing composes, validating, doesn't. I once had to implement a feature on a real estate website. For a given location I would get a list of stats (demographics, cost per square meter, average salary in the area, etc). Of those stats some themselves contained lists. At the beginning I modeled everything with arrays in react. This led to passing down lists and having to check at multiple steps whether they were non-empty and handle that case. Then I modeled everything with a NonEmptyArray guard in TypeScript ``` interface NonEmptyArray<A> extends Array<A> { 0: A // tells the typesystem that index 0 exists and is of type A } function isNonEmpty(as: A[]): as is NonEmptyArray<A> { return as.length > 0 } ``` then after receiving the response with those lists I could parse them into NonEmptyArrays, remove all of the checks of emptiness inside the react components till handling the fact that some of these elements were empty trickled up to the outermost component and everything became very clean and simple to understand/maintain.