Type-Theory

Symptom Someone hands you a function and no source: f :: forall a. [a] -> [a] How much can you say about it? The instinct is nothing: any implementation is possible, that is what polymorphism means. ...

Symptom “Well-typed programs don’t go wrong.” You have heard it. You have probably said it. And then: String s = null; s.length(); // NullPointerException That program is well typed and it went wrong. So either the slogan is false or it means something narrower than it sounds. It means something narrower, and the narrowness is precisely specifiable. ...

Symptom You write this in OCaml or Haskell and annotate nothing: let rec map f = function | [] -> [] | x :: xs -> f x :: map f xs The compiler reports ('a -> 'b) -> 'a list -> 'b list. It found the most general possible type, on its own, with no hints, and it will reject any call that does not fit. ...

Symptom You write a function signature and it looks like a sentence: f :: (a -> b) -> (b -> c) -> (a -> c) Read it aloud: if $a$ implies $b$, and $b$ implies $c$, then $a$ implies $c$. That is transitivity of implication, a rule of logic you have known since school. And the implementation, f g h = h . g, is the proof of it: given evidence for $a$, apply the first, then apply the second. ...