The Hindley–Milner type system

The previous chapter left us with a dilemma: either we write all the types by hand (reliable but tedious), or we ask the machine to guess them itself (convenient but undecidable in general). The Hindley–Milner system (HM for short) is the golden mean: the compiler infers the most general type of any expression with no annotations at all.

How do we keep type polymorphism without sliding back into the undecidability of System F? Hindley and Milner solve this by restricting where a quantifier may stand, splitting types into two floors: downstairs — monotypes $\tau$ — types without quantifiers: atomic $\alpha$, applications of type constructors $C\,\tau_1 \ldots \tau_n$ (this is how lists and pairs are built, for example) and arrows. Upstairs — schemes (polytypes) $\sigma$ — monotypes capped with quantifiers:

Quantifiers are allowed only on the outside, at the very front of a type (prenex form): $\forall \alpha.\, \alpha$ $\to \alpha$ is a legal scheme, while $(\forall \alpha.\, \alpha \to \alpha)$ $\to \beta$ is not: here the quantifier has crept inside, to the left of an arrow. Allow this — and you get full System F with its undecidable inference; forbid it — and you lose a little expressiveness but turn type inference into an algorithm. The whole trick of HM lies in this restriction.

There are two transitions between the floors; let us look at both. Downwards — instantiation (Inst): a scheme becomes a monotype $\sigma[\alpha := \tau]$ by substituting any monotype for the bound variable. Upwards — generalization (Gen): if a variable $\alpha$ remains in the inferred type but does not occur free in any assumption of the context ($\alpha$ $\notin \mathrm{free}(\Gamma)$), nothing outside constrains it — we may hang a quantifier on it:

Why these transitions are needed is seen in the rule for $\mathbf{let}$ — the heart of the whole system. Binding a name $x$ to a value $e_0$, we generalize its type to a scheme $\sigma$, and then every use of $x$ in the body $e_1$ instantiates this scheme anew, independently of the others:

The argument of a λ has no such privilege. Generalization happens only in the Let rule, and a function parameter never gets there: while we are typing the body, the function has not yet been applied to anything, and what will arrive as its input is unknown; all we can do is give the argument a single type variable, shared by all its uses in the body. The difference shows on two almost identical terms. The term $\mathbf{let}\;id$ $= \lambda y.\,y\;\mathbf{in}\;(id\;\overline{3},\, id\;\mathbf{true})$ typechecks: $id$ is bound by $\mathbf{let}$, generalized to the scheme $\forall\alpha.\,\alpha$ $\to\alpha$, and each of the two uses instantiates it with its own type. The term $(\lambda id.\,(id\;\overline{3},\, id\;\mathbf{true}))\,(\lambda y.\,y)$ — the same in meaning — no longer typechecks: here $id$ is the argument of a λ, it has no scheme, and a single monotype cannot simultaneously be the type of a function on numbers and on booleans.

Haskell does have type annotations, of course — signatures can (and customarily are) written out. But they are optional: even if there were none at all, the compiler would reconstruct every type by itself — this is done by algorithm W (Damas–Milner). It walks the term, hands every subexpression a fresh type variable, and at every application records an equation: the type of the function must be an arrow from the argument type to the result type. The accumulated equations are solved by Robinson unification — a mechanical matching of two types: for $\alpha$ $\to \beta$ to coincide with $(\gamma\to\gamma)$ $\to \delta$, the substitution $\alpha :$ $= \gamma$ $\to\gamma$, $\beta :$ $= \delta$ suffices. Bare code is enough for the compiler:

compose f g x = f (g x)

-- inferred without a single hint:
-- compose :: (b -> c) -> (a -> b) -> a -> c

Now we can see why the combinators $\mathrm{Y}$, $\Theta$ and $\mathrm{Z}$ cannot be used in Haskell. They are all built on the self-application $x\,x$ — let us try to infer its type. Let $x : \alpha$; since $x$ is applied to itself, $\alpha$ must be an arrow from $\alpha$ to some $\beta$ — we get the equation $\alpha$ $= \alpha$ $\to \beta$. Substitute the right-hand side for $\alpha$ — and $\alpha$ is inside again: $(\alpha\to\beta)$ $\to\beta$, $((\alpha\to\beta)\to\beta)$ $\to\beta$, … — the substitution loops and the type grows without bound. This is exactly what the occurs check cuts short — the ban on a variable occurring in the type substituted for it: without recursive types the equation has no solution. That is why recursion in Haskell is introduced by the primitive $\mathtt{fix}$ and by recursive definitions.