Comment by lexi-lambda
6 years ago
> Still no static types for "Strings that end with a dot" or "Strings that match [a-z]+"
Sure there are. :) Technically speaking, anyway. Here’s a type for “strings that end with a dot”:
-- | A string that ends in the character '.',
-- represented as a string without its trailing dot.
newtype StringEndingInDot = StringEndingInDot String
fromString :: String -> Maybe StringEndingInDot
fromString str = case reverse str of
'.':cs -> Just $ StringEndingInDot (reverse cs)
_ -> Nothing
toString :: StringEndingInDot -> String
toString (StringEndingInDot str) = str ++ "."
And here’s a type for “strings that match [a-z]+”:
data Letter = A | B | C | D | ... | X | Y | Z
type StringAZ = NonEmpty Letter
Now, admittedly, I would never use either of these types in real code, which is probably your actual point. :) But that’s a situation where there is a pragmatic “escape hatch” of sorts, since you can create an abstract datatype to represent these sorts of things in the type system without having to genuinely prove them:
module StringEndingInDot(StringEndingInDot, fromString, toString) where
newtype StringEndingInDot = StringEndingInDot { toString :: String }
fromString :: String -> Maybe StringEndingInDot
fromString str = case reverse str of
'.':_ -> Just $ StringEndingInDot str
_ -> Nothing
You may rightly complain that’s a lot of boilerplate just to represent this one property, and it doesn’t compose. That’s where the “Ghosts of Departed Proofs” paper (https://kataskeue.com/gdp.pdf) cited in the conclusion can come in. It provides a technique like the above that’s a little more advanced, but brings back composition.
>Technically speaking, anyway. Here’s a type for “strings that end with a dot”:
These are just two functions that wrap and unwrap a string. Your "type" doesn't generate a compile-time error when constructed with the wrong data. This doesn't even handle the simplest use case:
That code doesn't compile because fromString returns Maybe StringEndingInDot and toString takes StringEndingInDot. So it does protect you from misuse.
A properly enforced static type would not need to emit Maybe, because it would be impossible to set it to the wrong value in the first place.
Not to mention that to be truly useful a static type would need some sort of literal that would emit a compile-time error if the supplied init data was wrong.
In short, examples above do not demonstrate Haskell's ability to statically enforce rules like "string needs to end with a dot".
Now, you could make a type that always prepends a dot when asked for a string representation, which happens to enforce this specific constraint, but you cannot use a trick like this for most constraints (such as the second example of "only alpha characters").
2 replies →