6 ms·
Type systems can encode proofs of properties that you want your data to have. For example, suppose you want to write a function that returns the first element o
by sullyj3 6y ago
Type systems can encode proofs of properties that you want your data to have. For example, suppose you want to write a function that returns the first element of a list.
head :: [a] -> a
This is the type of a function "head" that takes a list of values of some arbitrary type a, and returns an a.
if you feed this function an empty list, what will it do? You can reason from the type signature that the only thing it possibly can do is crash, since there's no way to produce a value of type a without knowing what a is in advance.
head (h:_rest) = h
head [] = error "Our function is badly behaved!"
To ensure that our function never crashes, we can encode the fact that our list is nonempty in a datatype.
data Nonempty a = Nonempty a [a]
Ie, a nonempty list must contain a value of type a, and a (possible empty) list of as. Then instead of writing a function that crashes when it receives a nonempty list, we can write a function on nonempty lists that never crashes
head :: Nonempty a -> a
head (Nonempty x _rest) = x
What I'm getting at is that, yes, this is just the "shape" of our data. But you can encode more interesting and valuable properties in that shape than might be apparent at first. There are many other interesting examples of using types to ensure that properties that we want to hold for our values, do in fact hold.
Edit: I should probably add that "If it compiles it works" is absolutely not always true. It's more of a community in-joke than an actual belief. But it does turn out to be true surprisingly frequently.
- neolog 6y agoSure, you can encode various properties in some languages, but it's not that common to actually do so.
- sullyj3 6y agoIn Haskell, it's both common and idiomatic. There's always a tradeoff between the usefulness of having static guarantees, and the complexity of the type system features that enable those guarantees. In some cases it's more trouble than it's worth to enforce certain static properties - you have to weigh the costs and benefits on a case by case basis. But it's nice to have the option, and Haskellers make use of it frequently.
- heavenlyblue 6y agoYou don’t need Haskell to do this however.
- elbear 6y agoYou need a type system that is expressive enough to allow you to encode logic in the types. Of course, Haskell is not only language with such a type system: PureScript, F#, Rust, OCaml, Scala have similar features, although not all.
- tsimionescu 6y agoHow many functions have you seen, in Haskell, that take Nonempty a versus taking [a]? There are reasons why this type of pattern doesn't scale well, and the Haskell designers knew it. Similarly, if they had defined head [a] -> Optional a, that would have produced complications of its own.
- sullyj3 6y agoThe general consensus in the community afaik, is that head :: [a] -> a in Prelude was a mistake, and the default should be to return a Maybe/Optional. Beginners are generally advised to avoid head, and all other partial functions in the Prelude, such as tail and the indexing operator, wherever possible, and rely on pattern matching instead, which is generally sufficient and more idiomatic for the relevant use cases. I agree that having the option to use a partial function is useful, escape hatches are important, but it shouldn't be the go to. Nonempty was just a simple example. You're right that it's not very commonly used (probably because it's not in Prelude), but the general culture of writing type safe interfaces and pushing guarantees to compile time %100 is a thing. A commonly used, more complicated example might be Servant, which is a web library which statically ensures your implementation meets an API spec.
- tsimionescu 6y agoWell, since the Prelude was never changed to at least add an alternative headMaybe, perhaps it was not seen as a deep enough mistake. Yes, I am aware that the Haskell community generally tries to push more guarantees to compile time, and that Haskell's ease of defining and using new types equivalent to existing ones but that signify some property helps a lot in this. Still, there is some limit to this. For example, you have many libraries adding measurement units for Haskell, and many libraries doing linear algebra. But you won't find too many people doing linear algebra with measurement units, because the types of intermediate results explode too much (e.g. a type-safe unit-of-measurement matrix multiplication of 3x3 matrices has 18 type parameters, with complicated restrictions between them).
- iambrj 6y agoFor the curious, I suggest reading Philp Wadler's "Theorems for free!" which explains how to derive a theorem for a given type. Practically, this helps compilers make certain optimizations based on the theorems it derives from the types.
- Kednicma 6y agoAre you sure? https://lobste.rs/s/yyhu4w/real_problems_with_functional_languages#c_jsllxd https://lobste.rs/s/yyhu4w/real_problems_with_functional_lan...
- jimbokun 6y agoShouldn't head return "Maybe a", since the head of an empty list would be "None"? (Not sure if I got the Haskell terminology correct.)
- rowanG077 6y agoIn a better world it would. Currently it the head of an empty list crashes the program. Many people in the Haskell world are really salty about this but they don't want to break the API for it.
- deleted 6y ago[deleted]