3 ms·

In Haskell, you would use an algebraic data type that can only hold legal values. You would typically only use a newtype when you're just giving a new name to t

In Haskell, you would use an algebraic data type that can only hold legal values. You would typically only use a newtype when you're just giving a new name to the same type. Having a Magnitude newtype over Int doesn't change the range of permissible values but does prevent using a Length where a Magnitude was expected, for example. In all typed languages you'll eventually see a function with multiple arguments of the same type and have to check the documentation (or worse, implementation) to know what each is for. Having a zero cost type alias to make it clear is an improvement and IMO is a form of type safety. Having a data type that can hold illegal values is a bad idea. Using an Int for Length implies you know what to do with negative lengths, for example. A newtype won't help there.

alexmingoia 6y ago
Are you suggesting using Proxy to create a type that masks an Int? How would you deal with text that can only contain certain characters for example?
- codebje 6y ago
  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.
chongli 6y ago
How do you write a data type which can only hold legal email addresses? Or URLs? ZIP codes? Or even dates and times? Expressing all of the requirements of these real-world data formats, within a type system such as Haskell's, seems like an extremely daunting task to me. I have programmed in Haskell a fair bit in the past and I have no idea where I'd begin with those.
- embwbam 6y ago
  Practically, I disagree with the GP. A newtype is fine in these cases. You don't have to say you know what to do with negative Lengths if you have a smart constructor that won't let you create one.
  - codebje 6y ago
    Can you subtract lengths as in "let length3 = length1 - length2" ?
- codebje 6y ago
  You're combining acceptable structural representations with validated as correct inputs - this is a trap to be careful of. It's real-world data, which is rarely 100% clean and correct. If you can only represent clean and correct data, you probably can't handle all the data you'll need to. For an email, a "newtype Email = Text" is, IMO, correct. You can break it down as far as you need though: "data Email = Email (Maybe Name) LocalPart Domain" eg, with the three sub-types being newtypes of text. If you try to go further you'll run into problems that the best definition of "valid" is "works when used." The situation for URLs is similar. ZIP codes is an even trickier one - if you can only represent genuine ZIP codes, what happens if you need to represent an address where someone's accidentally transposed two digits and wound up with an unused ZIP code? If you're not US domestic only, what do you do for the four billion or so humans who don't have a structured address at all? (There's a reason vCard gave up on forcing structured addresses and added a "just whatever this text chunk here says" alternative). If you want to represent "validated version" data then IMO it's sufficient to use a "data ValidatedEmail = ValidatedEmail Email" with a non-exported constructor and a "validateEmail :: Email -> Maybe ValidatedEmail" function. If you're, say, the USPS and really must represent valid ZIP codes and only valid ZIP codes, you'll perhaps wind up in the rabbit hole of defining a hierarchical hot mess of sum types. Or pragmatically accept you will risk invalid ZIP codes to avoid needing to do that.

alexmingoia 6y ago

Are you suggesting using Proxy to create a type that masks an Int? How would you deal with text that can only contain certain characters for example?

codebje 6y ago
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.

chongli 6y ago

How do you write a data type which can only hold legal email addresses? Or URLs? ZIP codes? Or even dates and times? Expressing all of the requirements of these real-world data formats, within a type system such as Haskell's, seems like an extremely daunting task to me. I have programmed in Haskell a fair bit in the past and I have no idea where I'd begin with those.

embwbam 6y ago
Practically, I disagree with the GP. A newtype is fine in these cases. You don't have to say you know what to do with negative Lengths if you have a smart constructor that won't let you create one.
- codebje 6y ago
  Can you subtract lengths as in "let length3 = length1 - length2" ?
codebje 6y ago
You're combining acceptable structural representations with validated as correct inputs - this is a trap to be careful of. It's real-world data, which is rarely 100% clean and correct. If you can only represent clean and correct data, you probably can't handle all the data you'll need to. For an email, a "newtype Email = Text" is, IMO, correct. You can break it down as far as you need though: "data Email = Email (Maybe Name) LocalPart Domain" eg, with the three sub-types being newtypes of text. If you try to go further you'll run into problems that the best definition of "valid" is "works when used." The situation for URLs is similar. ZIP codes is an even trickier one - if you can only represent genuine ZIP codes, what happens if you need to represent an address where someone's accidentally transposed two digits and wound up with an unused ZIP code? If you're not US domestic only, what do you do for the four billion or so humans who don't have a structured address at all? (There's a reason vCard gave up on forcing structured addresses and added a "just whatever this text chunk here says" alternative). If you want to represent "validated version" data then IMO it's sufficient to use a "data ValidatedEmail = ValidatedEmail Email" with a non-exported constructor and a "validateEmail :: Email -> Maybe ValidatedEmail" function. If you're, say, the USPS and really must represent valid ZIP codes and only valid ZIP codes, you'll perhaps wind up in the rabbit hole of defining a hierarchical hot mess of sum types. Or pragmatically accept you will risk invalid ZIP codes to avoid needing to do that.