2 ms·

In the Length case I'm more suggesting to use an unsigned integer type than any more complex type system trickery to specifically limit the range. There are ty

In the Length case I'm more suggesting to use an unsigned integer type than any more complex type system trickery to specifically limit the range. There are type systems that let you declare a new type to be a sub-range of an existing type, but Haskell's is not one of them.

alexmingoia 6y ago
Dependent types don't provide any safety over smart constructors for parsing, which is the most common use case for types with restricted values. Validating user input, parsing emails or URLs, etc. all must deal with an invalid case at runtime, and dependent types are of no use there.
- remexre 6y ago
  What dependent types would protect you against would be the parser itself returning data. I think it'd be quite difficult to do this for the case of an email or URL, but for cases like "length values must be non-negative," a parser/validator with a type like parseLength :: JSON -> Either Error (Sigma (l : Length). lengthToDouble l >= 0.0) is reasonable, and I'm sure somewhere in the literature there's an indexed monad or something for building parsers/validators out of these, that keeps track of the properties while combining parsers like these.
- codebje 6y ago
  When I say range types I mean a type like '5..23' - a sub-range of some other type. Haskell doesn't have these. Most languages don't - one example that does is Ada: https://en.wikibooks.org/wiki/Ada_Programming/Types/range https://en.wikibooks.org/wiki/Ada_Programming/Types/range As you can see from that link, it's bounds checked at runtime. You could have a modulo type that wraps on overflow, which is of course what most numeric types are in most programming languages, including Haskell, but the modulus is fixed at some power of two for obvious reasons. There's only one thing I truly value out of a good type (or static analysis) system, and that's enabling fearless refactoring. I want the type system to pick up on any downstream consequences of a change I make rather than finding out by phone call at 3am the day after a deploy that some edge case got overlooked. Dependent types can (in theory) give that over smart constructors. If my parser should leave me with, say, a sorted vector, or an assertion that if one field is some value then some other field is Just something, then I'd like to be able to rely on those facts in downstream code making use of the results of the parser. If it's just a smart constructor as we usually write them a later refactor (sorting on a different key, for example) doesn't change anything that any other bit of code can be verified against. A dependent type carrying a proof that a vector is sorted based on some criteria and an assertion about the existed of some value can be verified at compile time. I'm not sure what the status is of dependent types for Haskell. You could do similar propositional assertions now with Ghosts of Departed Proofs, and LiquidHaskell exists for these sorts of assertions, so dependent types aren't the only path to this kind of static safety, either. I won't claim that this is practical - though I would be surprised if it's not practical to do in small doses. Nevertheless, I would still just be reaching for smart constructors in current day Haskell.

alexmingoia 6y ago

Dependent types don't provide any safety over smart constructors for parsing, which is the most common use case for types with restricted values. Validating user input, parsing emails or URLs, etc. all must deal with an invalid case at runtime, and dependent types are of no use there.

remexre 6y ago
What dependent types would protect you against would be the parser itself returning data. I think it'd be quite difficult to do this for the case of an email or URL, but for cases like "length values must be non-negative," a parser/validator with a type like parseLength :: JSON -> Either Error (Sigma (l : Length). lengthToDouble l >= 0.0) is reasonable, and I'm sure somewhere in the literature there's an indexed monad or something for building parsers/validators out of these, that keeps track of the properties while combining parsers like these.
codebje 6y ago
When I say range types I mean a type like '5..23' - a sub-range of some other type. Haskell doesn't have these. Most languages don't - one example that does is Ada: https://en.wikibooks.org/wiki/Ada_Programming/Types/range https://en.wikibooks.org/wiki/Ada_Programming/Types/range As you can see from that link, it's bounds checked at runtime. You could have a modulo type that wraps on overflow, which is of course what most numeric types are in most programming languages, including Haskell, but the modulus is fixed at some power of two for obvious reasons. There's only one thing I truly value out of a good type (or static analysis) system, and that's enabling fearless refactoring. I want the type system to pick up on any downstream consequences of a change I make rather than finding out by phone call at 3am the day after a deploy that some edge case got overlooked. Dependent types can (in theory) give that over smart constructors. If my parser should leave me with, say, a sorted vector, or an assertion that if one field is some value then some other field is Just something, then I'd like to be able to rely on those facts in downstream code making use of the results of the parser. If it's just a smart constructor as we usually write them a later refactor (sorting on a different key, for example) doesn't change anything that any other bit of code can be verified against. A dependent type carrying a proof that a vector is sorted based on some criteria and an assertion about the existed of some value can be verified at compile time. I'm not sure what the status is of dependent types for Haskell. You could do similar propositional assertions now with Ghosts of Departed Proofs, and LiquidHaskell exists for these sorts of assertions, so dependent types aren't the only path to this kind of static safety, either. I won't claim that this is practical - though I would be surprised if it's not practical to do in small doses. Nevertheless, I would still just be reaching for smart constructors in current day Haskell.