Lesson 7.2 — Hindley–Milner: let-polymorphism and Algorithms W, J and M¶
Techniques: let-polymorphism — type schemes, generalization at
let, instantiation at every use, principal types (Hindley 1969 [Hin69]; Milner 1978 [Mil78]; Damas & Milner 1982 [DM82]); Algorithm W — bottom-up inference with composed substitutions [Mil78, DM82]; Algorithm J — the same inference with one global substitution updated in place [Mil78]; Algorithm M — top-down inference with an expected type (Lee & Yi 1998 [LY98]) · Pebble implements: none directly (Pebble has no polymorphic functions); the lab implements all three for MiniML (labs/ch07-hm, L1–L3) · Drills:hm-trace,generalization· Prerequisites: Lesson 7.1; Lesson 6.1 (judgments) · Time: 6 hours
Chapter 6's checkers needed an annotation on every function parameter (syntax-directed) or at least a context that supplied one (bidirectional). ML-family languages need none: let twice = fun f -> fun x -> f (f x) receives the type ('a -> 'a) -> 'a -> 'a, and twice may then be used at int, at bool, at int list. This lesson gives the type system that makes this precise (Hindley–Milner, HM), the property that makes it usable (every typable program has a principal type from which all others are instances), and the three classic algorithms that compute it. They differ in how they carry the solution of the equations (composed substitutions, one mutable union-find, or an expected type pushed down), which changes their speed and where they report errors, but not the types they find.
1. Problem and motivation¶
Let-polymorphism¶
The problem. A function like twice is correct for every argument type; giving it one monomorphic type would force a copy per use. System F (Girard, Reynolds) allows polymorphism anywhere but makes inference undecidable (Lesson 7.8). Hindley [Hin69] showed that every term of combinatory logic has a principal type scheme; Milner [Mil78] designed ML's type system around a restriction that keeps this property: type variables may be universally quantified only at the top of the type of a let-bound variable, never inside types (rank-1, prenex polymorphism), and a λ-bound variable is always monomorphic. Damas and Milner [DM82] gave the declarative rules and proved the algorithm complete. The result is the type system of Standard ML, OCaml, Haskell 98 (before type classes, Lesson 7.7) and F#, and of this chapter's lab.
Algorithm W¶
The problem. The declarative rules of HM contain two guesses — the type of a λ-bound variable, and the instance at which a polymorphic variable is used — so they do not describe an algorithm. Milner's Algorithm W [Mil78, DM82] replaces each guess by a fresh type variable and computes, bottom-up, a substitution that solves every equation the program imposes, using Robinson unification (Lesson 7.1). Its purely functional presentation (every call returns a substitution and a type) is what the soundness and completeness proofs are about, and it is still the reference against which implementations are checked.
Algorithm J¶
The problem. W composes substitutions and applies them to the whole environment after every subterm; on a program with \(n\) nested lets that alone costs \(\Theta(n^2)\) (the lab measures it, §8). Milner described, in the same paper, Algorithm J [Mil78, §4]: keep one global substitution, updated in place by unification, and never apply it eagerly — dereference type variables when you look at them. With the union-find unifier of Lesson 7.1 this is the algorithm every ML and Haskell compiler actually runs; OCaml's Ctype.unify is J's unifier (§7).
Algorithm M¶
The problem. W and J report a type error where two synthesized types fail to unify — often an application far from the mistake (fun f -> (f 1, f true) fails at the second application, having silently accepted the first). Lee and Yi [LY98] formalized the folklore top-down algorithm that compilers such as OCaml's and GHC's partly use: pass the type the context expects into each subterm (like the checking mode of Lesson 6.4) and unify at the leaves. They proved it sound and complete, like W, and showed that it detects errors earlier. This lesson presents it as Algorithm M; Lesson 7.9 compares the error locations systematically.
2. Definitions and algorithms¶
Definition 7.2.1 (MiniML types and schemes)
Monotypes \(\tau ::= \alpha \mid \mathsf{int} \mid \mathsf{bool} \mid \mathsf{unit} \mid \tau_1 \to \tau_2 \mid \tau_1 \times \tau_2 \mid \tau\ \mathsf{list} \mid \tau\ \mathsf{ref}\), where \(\alpha, \beta, \gamma\) range over type variables. Type schemes \(\sigma ::= \forall \alpha_1 \dots \alpha_n.\, \tau\) (\(n \ge 0\); a monotype is a scheme with \(n = 0\)). \(\mathrm{ftv}(\tau)\) is the set of type variables of \(\tau\); \(\mathrm{ftv}(\forall \vec\alpha.\,\tau) = \mathrm{ftv}(\tau) \setminus \vec\alpha\). Substitutions (Definition 7.1.2) act on monotypes and, avoiding capture, on the free variables of schemes.
Definition 7.2.2 (Contexts, instances, generalization)
A context \(\Gamma\) maps variables to schemes; \(\mathrm{ftv}(\Gamma) = \bigcup_{x} \mathrm{ftv}(\Gamma(x))\). A monotype \(\tau'\) is an instance of \(\sigma = \forall \alpha_1 \dots \alpha_n.\,\tau\), written \(\tau' \le \sigma\), if \(\tau' = [\alpha_1 \mapsto \tau_1, \dots, \alpha_n \mapsto \tau_n]\tau\) for some monotypes \(\tau_i\). The generalization of \(\tau\) in \(\Gamma\) is \(\mathrm{gen}(\Gamma, \tau) = \forall \vec\alpha.\,\tau\) with \(\vec\alpha = \mathrm{ftv}(\tau) \setminus \mathrm{ftv}(\Gamma)\).
Definition 7.2.3 (MiniML)
\(e ::= x \mid n \mid \mathsf{true} \mid \mathsf{false} \mid () \mid \mathsf{fun}\ x \to e \mid e_1\, e_2 \mid \mathsf{let}\ x = e_1\ \mathsf{in}\ e_2 \mid \mathsf{let\ rec}\ f = \mathsf{fun}\ x \to e_1\ \mathsf{in}\ e_2 \mid \mathsf{if}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \mid (e_1, e_2) \mid e_1 \oplus e_2\) with \(\oplus \in \{+, -, *, <, ==\}\) on integers. The initial context \(\Gamma_0\) gives the builtins their schemes, e.g. \(\mathit{fst} : \forall\alpha\beta.\ \alpha \times \beta \to \alpha\), \(\mathit{cons} : \forall \alpha.\ \alpha \to \alpha\ \mathsf{list} \to \alpha\ \mathsf{list}\), \(\mathit{ref} : \forall\alpha.\ \alpha \to \alpha\ \mathsf{ref}\) (the lab's labs/ch07-hm/SPEC.md §2 lists all ten).
Definition 7.2.4 (The Hindley–Milner typing rules)
with the axioms \(n : \mathsf{int}\), \(\mathsf{true}, \mathsf{false} : \mathsf{bool}\), \(() : \mathsf{unit}\), and \(\tau_\oplus = \mathsf{int}\) for \(+ - *\), \(\mathsf{bool}\) for \(<\) and \(==\). Var instantiates a scheme; Let generalizes; Abs binds a monotype. (Lesson 7.3 restricts Let with the value restriction.)
Definition 7.2.5 (Principal type)
A typing of \(e\) is a pair \((\theta, \tau)\) with \(\theta\Gamma \vdash e : \tau\). It is principal for \((\Gamma, e)\) if every typing \((\theta', \tau')\) satisfies \(\theta'\Gamma = \rho\theta\Gamma\) and \(\tau' = \rho\tau\) for some \(\rho\) — every other typing is an instance. For closed \(e\) (\(\mathrm{ftv}(\Gamma) = \emptyset\)) this is the principal type scheme \(\mathrm{gen}(\Gamma, \tau)\).
The running example
\(e_{\mathrm{tw}} = \mathsf{let}\ \mathit{twice} = \mathsf{fun}\ f \to \mathsf{fun}\ x \to f\,(f\,x)\ \mathsf{in}\ \mathit{twice}\ (\mathsf{fun}\ n \to n + 1)\ 0\) (16 subterms, in the lab's syntax let twice = fun f -> fun x -> f (f x) in twice (fun n -> n + 1) 0). Its principal type is \(\mathsf{int}\); \(\mathit{twice}\) receives the scheme \(\forall\alpha.\ (\alpha \to \alpha) \to \alpha \to \alpha\) and is used at \(\alpha = \mathsf{int}\). The ill-typed variant \(e_{\mathrm{bad}} = \mathsf{fun}\ f \to (f\ 1, f\ \mathsf{true})\) has no type.
Let-polymorphism¶
Algorithm 7.2.6 (Generalize and instantiate)
- Input:
Gen: a context \(\Gamma\) and a monotype \(\tau\) (both under the current substitution);Inst: a scheme \(\sigma\). - Output:
Gen: \(\mathrm{gen}(\Gamma, \tau)\);Inst: a monotype \(\tau' \le \sigma\) whose new variables are fresh. - Precondition: the current substitution has been applied to \(\Gamma\) and \(\tau\) (W, M) or is dereferenced on the fly (J).
- Postcondition:
Instreturns the most general instance: every instance of \(\sigma\) is a substitution instance of it. - Invariant: fresh variables are never reused, so instances of one scheme are independent.
Algorithm W¶
Algorithm 7.2.7 (Algorithm W)
- Input: a context \(\Gamma\) and an expression \(e\).
- Output: a pair \((\theta, \tau)\), or failure at a subterm.
- Precondition:
Unifyreturns an idempotent MGU (Algorithm 7.1.7 on types). - Postcondition: \(\theta\Gamma \vdash e : \tau\), and \((\theta, \tau)\) is principal (Theorem 7.2.11).
- Invariant: each recursive call receives the context with all substitutions found so far applied; \(\theta\tau = \tau\) for every returned pair.
function W(Γ, e):
case e of
n, true/false, (): return ([], int / bool / unit)
x: if x ∉ Γ: fail "unbound" at x
return ([], Inst(Γ(x)))
fun x -> e1: β ← fresh; (θ1, τ1) ← W(Γ[x ↦ β], e1)
return (θ1, θ1β → τ1)
e1 e2: (θ1, τ1) ← W(Γ, e1); (θ2, τ2) ← W(θ1Γ, e2); β ← fresh
θ3 ← Unify(θ2τ1, τ2 → β) # failure reported at e1 e2
return (θ3θ2θ1, θ3β)
let x = e1 in e2: (θ1, τ1) ← W(Γ, e1)
(θ2, τ2) ← W(θ1Γ[x ↦ Gen(θ1Γ, τ1)], e2)
return (θ2θ1, τ2)
let rec f = e1 in e2:
β ← fresh; (θ1, τ1) ← W(Γ[f ↦ β], e1)
θ2 ← Unify(θ1β, τ1) # failure reported at e1
(θ3, τ2) ← W(θ2θ1Γ[f ↦ Gen(θ2θ1Γ, θ2τ1)], e2)
return (θ3θ2θ1, τ2)
if e1 then e2 else e3:
(θ1, τ1) ← W(Γ, e1); θ2 ← Unify(τ1, bool) # at e1
(θ3, τ2) ← W(θ2θ1Γ, e2); (θ4, τ3) ← W(θ3θ2θ1Γ, e3)
θ5 ← Unify(θ4τ2, τ3) # at e3
return (θ5θ4θ3θ2θ1, θ5τ3)
(e1, e2): (θ1, τ1) ← W(Γ, e1); (θ2, τ2) ← W(θ1Γ, e2)
return (θ2θ1, θ2τ1 × τ2)
e1 ⊕ e2: (θ1, τ1) ← W(Γ, e1); θ2 ← Unify(τ1, int) # at e1
(θ3, τ2) ← W(θ2θ1Γ, e2); θ4 ← Unify(τ2, int) # at e2
return (θ4θ3θ2θ1, τ⊕)
The positions in the comments are the lab's error-reporting convention (labs/ch07-hm/SPEC.md §3.3).
Algorithm J¶
Algorithm 7.2.8 (Algorithm J)
- Input: a context \(\Gamma\) and an expression \(e\); a global substitution \(\Theta\) (initially empty), mutated in place.
- Output: a type \(\tau\); on return, \(\Theta\) has been extended.
- Precondition:
UnifyInPlace(τ1, τ2)extends \(\Theta\) with an MGU of \(\Theta\tau_1 \doteq \Theta\tau_2\) (union-find, Algorithm 7.1.10); type variables are dereferenced through \(\Theta\) whenever they are inspected. - Postcondition: \(\Theta\Gamma \vdash e : \Theta\tau\), and \(\Theta\) and \(\tau\) agree with W's result up to renaming (Theorem 7.2.12).
- Invariant: \(\Theta\) only grows (bindings are never undone); \(\Gamma\) is never rewritten.
function J(Γ, e):
case e of
n, true/false, (): return int / bool / unit
x: return Inst(Γ(x)) # Inst dereferences through Θ
fun x -> e1: β ← fresh; return β → J(Γ[x ↦ β], e1)
e1 e2: τ1 ← J(Γ, e1); τ2 ← J(Γ, e2); β ← fresh
UnifyInPlace(τ1, τ2 → β); return β
let x = e1 in e2: τ1 ← J(Γ, e1)
return J(Γ[x ↦ Gen(ΘΓ, Θτ1)], e2) # Lesson 7.3 removes ΘΓ
let rec f = e1 in e2:
β ← fresh; τ1 ← J(Γ[f ↦ β], e1); UnifyInPlace(β, τ1)
return J(Γ[f ↦ Gen(ΘΓ, Θτ1)], e2)
if e1 then e2 else e3:
UnifyInPlace(J(Γ, e1), bool)
τ2 ← J(Γ, e2); UnifyInPlace(τ2, J(Γ, e3)); return τ2
(e1, e2): return J(Γ, e1) × J(Γ, e2)
e1 ⊕ e2: UnifyInPlace(J(Γ, e1), int); UnifyInPlace(J(Γ, e2), int)
return τ⊕
Computing \(\mathrm{ftv}(\Theta\Gamma)\) in Gen still costs \(O(\lvert\Gamma\rvert)\) per let; Lesson 7.3's levels remove that cost.
Algorithm M¶
Algorithm 7.2.9 (Algorithm M, after Lee and Yi)
- Input: a context \(\Gamma\), an expression \(e\) and an expected type \(\rho\).
- Output: a substitution \(\theta\) with \(\theta\Gamma \vdash e : \theta\rho\), or failure at a subterm.
- Precondition: as for W; the initial call is \(M(\Gamma_0, e, \beta)\) with \(\beta\) fresh, and the result type is \(\theta\beta\).
- Postcondition: sound and complete like W (Theorem 7.2.13).
- Invariant: \(\rho\) carries everything the context already knows about \(e\)'s type, so a conflict surfaces at the first subterm whose own form contradicts it.
function M(Γ, e, ρ):
case e of
n / true / (): return Unify(ρ, int / bool / unit) # at e
x: return Unify(ρ, Inst(Γ(x))) # at x
fun x -> e1: β1, β2 ← fresh; θ1 ← Unify(ρ, β1 → β2) # at e
θ2 ← M(θ1Γ[x ↦ θ1β1], e1, θ1β2); return θ2θ1
e1 e2: β ← fresh; θ1 ← M(Γ, e1, β → ρ)
θ2 ← M(θ1Γ, e2, θ1β); return θ2θ1
let x = e1 in e2: β ← fresh; θ1 ← M(Γ, e1, β)
θ2 ← M(θ1Γ[x ↦ Gen(θ1Γ, θ1β)], e2, θ1ρ); return θ2θ1
let rec f = e1 in e2:
β ← fresh; θ1 ← M(Γ[f ↦ β], e1, β)
θ2 ← M(θ1Γ[f ↦ Gen(θ1Γ, θ1β)], e2, θ1ρ); return θ2θ1
if e1 then e2 else e3:
θ1 ← M(Γ, e1, bool); θ2 ← M(θ1Γ, e2, θ1ρ)
θ3 ← M(θ2θ1Γ, e3, θ2θ1ρ); return θ3θ2θ1
(e1, e2): β1, β2 ← fresh; θ1 ← Unify(ρ, β1 × β2) # at e
θ2 ← M(θ1Γ, e1, θ1β1); θ3 ← M(θ2θ1Γ, e2, θ2θ1β2)
return θ3θ2θ1
e1 ⊕ e2: θ1 ← Unify(ρ, τ⊕) # at e
θ2 ← M(θ1Γ, e1, int); θ3 ← M(θ2θ1Γ, e2, int)
return θ3θ2θ1
3. Worked examples¶
All traces come from the course oracle (tools/course/lib/hm.py: infer_w, infer_j, infer_m with a trace); variables are numbered in creation order and written \(t_1, t_2, \dots\).
Let-polymorphism¶
In \(e_{\mathrm{tw}}\) the bound expression's type is \((t_4 \to t_4) \to t_4 \to t_4\) after inference (below), and \(\Gamma_0\) contains no type variables, so Gen quantifies \(t_4\): \(\mathit{twice} : \forall t_4.\ (t_4 \to t_4) \to t_4 \to t_4\). The use of \(\mathit{twice}\) is instantiated with a fresh \(t_5\). In \(e_{\mathrm{bad}}\), by contrast, \(f\) is λ-bound: Abs gives it one monotype \(t_1\), the first application forces \(t_1 = \mathsf{int} \to t_2\), and the second needs \(\mathsf{int} = \mathsf{bool}\). Writing \(\mathsf{let}\ f = \mathsf{fun}\ x \to x\ \mathsf{in}\ (f\ 1, f\ \mathsf{true})\) instead types as \(\mathsf{int} \times \mathsf{bool}\) (the lab corpus's 02-let-poly.mml).
Algorithm W¶
W on \(e_{\mathrm{tw}}\): every call of Unify, in order (\(t_1 = f\), \(t_2 = x\), \(t_3\) and \(t_4\) the results of the inner and outer application, \(t_5\) the instance of \(\mathit{twice}\)'s scheme, \(t_6 = n\), \(t_7\), \(t_8\) the results of the two applications of \(\mathit{twice}\)):
| # | at subterm (column) | equation | bindings added |
|---|---|---|---|
| 1 | f x (34) |
\(t_1 = t_2 \to t_3\) | \(t_1 \mapsto t_2 \to t_3\) |
| 2 | f (f x) (31) |
\(t_2 \to t_3 = t_3 \to t_4\) | \(t_2 \mapsto t_4\), \(t_3 \mapsto t_4\) |
| — | let twice |
\(\mathrm{Gen}(\Gamma_0, (t_4 \to t_4) \to t_4 \to t_4)\) | scheme \(\forall t_4.\ (t_4 \to t_4) \to t_4 \to t_4\) |
| 3 | n (58), left operand of + |
\(t_6 = \mathsf{int}\) | \(t_6 \mapsto \mathsf{int}\) |
| 4 | 1 (62), right operand |
\(\mathsf{int} = \mathsf{int}\) | — |
| 5 | twice (fun n -> n + 1) (42) |
\((t_5 \to t_5) \to t_5 \to t_5 = (\mathsf{int} \to \mathsf{int}) \to t_7\) | \(t_5 \mapsto \mathsf{int}\), \(t_7 \mapsto \mathsf{int} \to \mathsf{int}\) |
| 6 | twice (fun n -> n + 1) 0 (42) |
\(\mathsf{int} \to \mathsf{int} = \mathsf{int} \to t_8\) | \(t_8 \mapsto \mathsf{int}\) |
Result: \(\theta t_8 = \mathsf{int}\). Row 2 is where f (f x) forces \(f\)'s argument and result types to coincide; row 5 is where the instance \(t_5\), not the scheme's \(t_4\), is solved — the scheme stays polymorphic.
On \(e_{\mathrm{bad}}\), W unifies \(t_1 = \mathsf{int} \to t_2\) at f 1 (column 11) and then fails unifying \(\mathsf{int} \to t_2 = \mathsf{bool} \to t_3\) at the application f true, column 16.
Algorithm J¶
J performs the same six unifications in the same order, but each one links union-find nodes instead of composing substitutions; the environment is never rewritten:
| step | event | \(\Theta\) after the step (links) |
|---|---|---|
| 1 | unify at f x |
\(t_1 \Rightarrow t_2 \to t_3\) |
| 2 | unify at f (f x): dereference \(t_1\) to \(t_2 \to t_3\), unify with \(t_3 \to t_4\) |
\(t_2 \Rightarrow t_3\), \(t_3 \Rightarrow t_4\) |
| 3 | generalize twice: dereference its type, \((t_4 \to t_4) \to t_4 \to t_4\) |
\(t_4\) marked generic |
| 4 | unify at n |
\(t_6 \Rightarrow \mathsf{int}\) |
| 5 | unify at twice (fun n -> n + 1) |
\(t_5 \Rightarrow \mathsf{int}\), \(t_7 \Rightarrow \mathsf{int} \to \mathsf{int}\) |
| 6 | unify at the outer application | \(t_8 \Rightarrow \mathsf{int}\) |
The chain \(t_2 \Rightarrow t_3 \Rightarrow t_4\) after step 2 is exactly W's composed \(t_2 \mapsto t_4\), stored as links: path compression shortens it on the next find.
Algorithm M¶
M on \(e_{\mathrm{tw}}\) with the root's expected type \(t_1\) (its own numbering): the expected type flows into every subterm, so unifications happen at the leaves:
| # | at subterm (column) | equation (expected \(=\) own form) | bindings added |
|---|---|---|---|
| 1 | fun f -> … (13) |
\(t_2 = t_3 \to t_4\) | \(t_2 \mapsto t_3 \to t_4\) |
| 2 | fun x -> … (22) |
\(t_4 = t_5 \to t_6\) | \(t_4 \mapsto t_5 \to t_6\) |
| 3 | f (31), function of f (f x) |
\(t_7 \to t_6 = t_3\) | \(t_3 \mapsto t_7 \to t_6\) |
| 4 | f (34), function of f x |
\(t_8 \to t_7 = t_7 \to t_6\) | \(t_8 \mapsto t_6\), \(t_7 \mapsto t_6\) |
| 5 | x (36) |
\(t_6 = t_5\) | \(t_6 \mapsto t_5\) |
| 6 | twice (42) |
\(t_{10} \to t_9 \to t_1 = (t_{11} \to t_{11}) \to t_{11} \to t_{11}\) | \(t_{10} \mapsto t_{11} \to t_{11}\), \(t_9 \mapsto t_{11}\), \(t_1 \mapsto t_{11}\) |
| 7 | fun n -> n + 1 (49) |
\(t_{11} \to t_{11} = t_{12} \to t_{13}\) | \(t_{11} \mapsto t_{13}\), \(t_{12} \mapsto t_{13}\) |
| 8 | n + 1 (60, the operator) |
\(t_{13} = \mathsf{int}\) | \(t_{13} \mapsto \mathsf{int}\) |
| 9–11 | n (58), 1 (62), 0 (65) |
\(\mathsf{int} = \mathsf{int}\) each | — |
On \(e_{\mathrm{bad}}\), M has already fixed \(f : \mathsf{int} \to t_4\) when it reaches the second component; the expected type of the argument true is \(\mathsf{int}\), so M fails at the literal true, column 18 — the subterm the programmer would change, where W blamed the whole application at column 16.
Try it
./course drill hm-trace --seed 5 --difficulty medium --solution prints W's unification table and the type of every subterm for a random program; --difficulty hard includes ill-typed programs and asks for W's error position.
4. Invariants and correctness¶
Let-polymorphism¶
Proposition 7.2.10 (λ-bound variables are monomorphic; let-bound ones are not)
\(e_{\mathrm{bad}} = \mathsf{fun}\ f \to (f\ 1, f\ \mathsf{true})\) has no type in any context, while \(\mathsf{let}\ f = \mathsf{fun}\ x \to x\ \mathsf{in}\ (f\ 1, f\ \mathsf{true})\) has type \(\mathsf{int} \times \mathsf{bool}\).
Proof
Suppose \(\Gamma \vdash e_{\mathrm{bad}} : \tau\). The only rule for fun is Abs, so \(\Gamma, f{:}\tau_1 \vdash (f\ 1, f\ \mathsf{true}) : \tau_2\) for a monotype \(\tau_1\); Pair and App then require \(\Gamma, f{:}\tau_1 \vdash f : \mathsf{int} \to \tau_3\) and \(\Gamma, f{:}\tau_1 \vdash f : \mathsf{bool} \to \tau_4\). By Var, both are instances of the scheme \(\tau_1\), which has no quantified variables, so \(\tau_1 = \mathsf{int} \to \tau_3 = \mathsf{bool} \to \tau_4\), hence \(\mathsf{int} = \mathsf{bool}\): contradiction. For the let form: \(\vdash \mathsf{fun}\ x \to x : \alpha \to \alpha\) by Abs and Var, \(\mathrm{gen}(\emptyset, \alpha \to \alpha) = \forall\alpha.\ \alpha \to \alpha\), and Var instantiates it at \(\alpha = \mathsf{int}\) and at \(\alpha = \mathsf{bool}\) in the two components; App and Pair conclude \(\mathsf{int} \times \mathsf{bool}\).
Algorithm W¶
Theorem 7.2.11 (Soundness and completeness of W)
Soundness: if \(W(\Gamma, e) = (\theta, \tau)\) then \(\theta\Gamma \vdash e : \tau\). Completeness (principality): if \(\theta'\Gamma \vdash e : \tau'\) for some \(\theta', \tau'\), then \(W(\Gamma, e)\) succeeds with some \((\theta, \tau)\) and there is \(\rho\) with \(\theta'\Gamma = \rho\theta\Gamma\) and \(\tau' = \rho\tau\). Consequently every typable \(e\) has a principal typing, and W computes it.
Proof sketch (full proofs: [DM82] states the theorems, Damas's thesis [Dam85] proves them; the monomorphic core in detail: [TAPL §22.3–22.5])
Soundness, by induction on \(e\), one case per clause, using two lemmas: typing is stable under substitution (\(\Gamma \vdash e : \tau\) implies \(\theta\Gamma \vdash e : \theta\tau\), by induction on derivations, with care at Let: \(\theta\) must avoid the generalized variables, which can be renamed apart) and Unify returns a unifier (Theorem 7.1.14). In the App case, the induction hypotheses give \(\theta_1\Gamma \vdash e_1 : \tau_1\) and \(\theta_2\theta_1\Gamma \vdash e_2 : \tau_2\); applying \(\theta_3\theta_2\) and \(\theta_3\) respectively and using \(\theta_3(\theta_2\tau_1) = \theta_3(\tau_2 \to \beta)\) gives the premises of App with the same context. In the Let case, the substitution lemma shows that generalizing in \(\theta_1\Gamma\) and then applying \(\theta_2\) is an instance of generalizing after — the step where the side condition \(\vec\alpha \cap \mathrm{ftv}(\theta_1\Gamma) = \emptyset\) matters.
Completeness, by induction on \(e\) with the hypothesis strengthened to all \(\theta'\): given a derivation for \(\theta'\Gamma\), the induction hypothesis on \(e_1\) yields \(\rho_1\) with \(\theta' = \rho_1\theta_1\) on \(\Gamma\); the derivation for \(e_2\) is then a derivation for \(\rho_1\theta_1\Gamma\), and so on; at App, the typing supplies a unifier \(\rho\) of \(\theta_2\tau_1\) and \(\tau_2 \to \beta\) (extended with \(\beta \mapsto \tau'\)), so Unify succeeds and its MGU \(\theta_3\) satisfies \(\rho = \rho_3\theta_3\) (Definition 7.1.3). At Let, the declarative rule's \(\mathrm{gen}(\theta'\Gamma, \tau_1')\) is an instance of W's \(\mathrm{gen}(\theta_1\Gamma, \tau_1)\) in the sense that every instance of the former is an instance of the latter — this is the lemma that fails without principality of \(e_1\), and the one Damas proves in detail.
Algorithm J¶
Theorem 7.2.12 (J computes W's result)
Run W and J on the same \((\Gamma, e)\) with the same order of fresh variables. Then J fails iff W fails, at the same subterm, and otherwise J's final \(\Theta\) and returned \(\tau_J\) satisfy \(\Theta\tau_J = \tau_W\) and \(\Theta = \theta_W\) on \(\mathrm{ftv}(\Gamma)\) and on every variable W created, up to the choice of representatives in each unification.
Proof sketch (J and W side by side: [Mil78, §4])
By induction on \(e\), with the invariant: at entry to \(J(\Gamma, e)\) the global \(\Theta\) equals the composition \(\theta_{\text{so far}}\) that W has applied to the \(\Gamma\) it passes to the corresponding call. The two algorithms make the same calls in the same order and create the same fresh variables. At each unification, W unifies \(\theta_{\text{so far}}\tau_1\) with \(\theta_{\text{so far}}\tau_2\) while J unifies \(\Theta\tau_1\) with \(\Theta\tau_2\) (dereferencing) — the same pair of terms, so both succeed or fail together; on success, W composes the MGU \(\theta\) onto its substitution and J extends \(\Theta\) by the same bindings (union-find computes an MGU equal up to representatives, Theorem 7.1.17), which re-establishes the invariant. Gen sees \(\Theta\Gamma = \theta_{\text{so far}}\Gamma\) in both, hence the same schemes.
Algorithm M¶
Theorem 7.2.13 (Algorithm M is sound, complete and fails no later than W)
If \(M(\Gamma, e, \rho) = \theta\) then \(\theta\Gamma \vdash e : \theta\rho\). If some \(\theta'\) satisfies \(\theta'\Gamma \vdash e : \theta'\rho\), then \(M(\Gamma, e, \rho)\) succeeds with a \(\theta\) more general than \(\theta'\) on \(\mathrm{ftv}(\Gamma) \cup \mathrm{ftv}(\rho)\). On an ill-typed \(e\), M stops after visiting no more subterms than W.
Proof sketch (full proof: [LY98, §3–4])
Soundness and completeness by induction on \(e\), as for W, with the extra parameter \(\rho\) threaded through the hypothesis: in the application case, the typing of \(e_1\, e_2\) at \(\theta'\rho\) provides a typing of \(e_1\) at \(\tau \to \theta'\rho\) for some \(\tau\), which instantiates the fresh \(\beta\) in \(M(\Gamma, e_1, \beta \to \rho)\). The "earlier" statement: M's unifications involve the expected type as soon as a subterm is entered, so every constraint W would check at an application node has, in M, already been imposed on the application's function or argument; Lee and Yi formalize this by comparing the sequences of visited subterms. The example \(e_{\mathrm{bad}}\) shows the difference is real: W fails after visiting the application f true, M at its argument.
5. Complexity¶
| Technique | Time (worst) | Time (typical) | Space | Variables |
|---|---|---|---|---|
| HM typability (the problem) | DEXPTIME-complete [Mai90, KTU90] | near-linear on real programs (Lesson 7.3) | exponential type size in the worst case | \(n\) program size |
| Algorithm W | exponential (inherent); \(\Theta(n^2)\) extra on nested lets |
quadratic factors show at thousands of bindings | substitutions and copied environments | \(n\) subterms, \(d\) let depth |
| Algorithm J | exponential (inherent); \(O(n \cdot \lvert\Gamma\rvert)\) for Gen without levels |
near-linear with union-find | one union-find over type nodes | as above |
| Algorithm M | as W | as W, slightly more unifications (one per leaf) | as W | as above |
Justification. All three solve the same problem, so the DEXPTIME lower bound of Lesson 7.3 applies to each; its pathological family (types doubling at every let) makes the output exponential. Beyond that: W applies its composed substitution to the whole environment at every App, Let and If (\(\Theta(\lvert\Gamma\rvert)\) each) and composes substitutions whose domains grow, so on a chain of \(n\) nested lets (the lab's letChain) it does \(\Theta(n)\) work per let, \(\Theta(n^2)\) in all. J never rewrites \(\Gamma\); with Lesson 7.3's levels even Gen is proportional to the size of the generalized type, giving the near-linear behavior. M does one unification per leaf in addition to W's, a constant factor.
Pathological family and measured scale. letChain(n) = let x1 = fun y -> y in let x2 = x1 in … xn. The lab's reference implementations (build/<preset>/bin/ch07-hm-bench, §8) take 58 ms (W) and 0.54 ms (J) at \(n = 1000\), and 286 ms and 0.87 ms at \(n = 2000\): W grows by \(4.9\times\) when \(n\) doubles, J by \(1.6\times\).
6. Variants and refinements¶
Let-polymorphism¶
- The value restriction (Lesson 7.3, [Wri95]): generalize only syntactic values, so that references stay monomorphic. Trade-off: sound with effects, rejects a few pure programs (fixed by η-expansion).
- No generalization of local
lets (GHC'sMonoLocalBinds, [VPJS10]): generalize only top-level and annotated bindings. Trade-off: simpler, more predictable inference with type classes and GADTs (Lesson 7.4); some local polymorphism needs an annotation.
Algorithm W¶
- Constraint-based W (TAPL Ch. 22 [TAPL]; HM(X), Lesson 7.4): first generate all equations, then solve them. Trade-off: cleaner separation and extensibility; the error location is no longer determined by the traversal (Lesson 7.9).
- W with explicit substitution application on demand (triangular substitutions, Lesson 7.1 §6): avoid applying \(\theta\) to \(\Gamma\) eagerly. Trade-off: this is most of the way to J.
Algorithm J¶
- J with levels (Lesson 7.3, [Rem92]; OCaml): replace \(\mathrm{ftv}(\Theta\Gamma)\) by a level comparison. Trade-off: one integer per variable; the fastest known practical generalization.
- J with undoable bindings (Swift, rustc probes): record links in a trail and roll back. Trade-off: needed when inference must try an alternative (overloads, Lesson 7.5); no path compression across checkpoints.
Algorithm M¶
- Bidirectional HM (Lesson 6.4, [DK21]; GHC's
tcExprwithExpRhoType[GHC-App]): switch between synthesis and checking instead of always pushing a type variable down. Trade-off: better annotation support (higher-rank, Lesson 7.8); more rules. - Folklore M in OCaml (
type_expectintyping/typecore.ml[OCAML-Typecore]): propagate the expected type where it is known and unify at the leaf. Trade-off: better error locations (§7), slightly more unification work.
7. In real compilers¶
Let-polymorphism¶
OCaml generalizes every let whose right-hand side is non-expansive (Typecore.type_let, using is_nonexpansive) and instantiates schemes at each use (Ctype.instance) [OCAML-Typecore, OCAML-Ctype]. GHC generalizes top-level bindings and, without MonoLocalBinds, local ones (GHC.Tc.Gen.Bind, tcPolyInfer calling simplifyInfer [GHC-Solver]). SML/NJ and F# follow the Definition of Standard ML.
Let-bound vs λ-bound polymorphism in OCaml 4.14
Reproduce (OCaml 4.14.1):
mkdir -p ml && cat > ml/poly.ml <<'EOF'
let pair_ids = let id = fun x -> x in (id 1, id true)
let compose = fun f -> fun g -> fun x -> f (g x)
let rec map = fun f -> fun l -> match l with [] -> [] | h :: t -> f h :: map f t
let escape = fun x -> let k = fun y -> (x, y) in (k 1, k true)
EOF
ocamlc -i ml/poly.ml
echo 'let bad = (fun id -> (id 1, id true)) (fun x -> x)' > ml/lambda.ml
ocamlc -i ml/lambda.ml
Output (complete):
val pair_ids : int * bool
val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
val map : ('a -> 'b) -> 'a list -> 'b list
val escape : 'a -> ('a * int) * ('a * bool)
File "ml/lambda.ml", line 1, characters 31-35:
1 | let bad = (fun id -> (id 1, id true)) (fun x -> x)
^^^^
Error: This expression has type bool but an expression was expected of type
int
What to notice: id bound by let is used at int and bool; the same function passed as a λ-argument is not (Proposition 7.2.10). In escape, k's own parameter is generalized but x's type is free in the context and stays one type 'a — \(\mathrm{gen}\) excludes \(\mathrm{ftv}(\Gamma)\). The printed types are the principal types of Theorem 7.2.11, identical to the lab corpus goldens 04-compose.mml and 09-escape.mml.
Algorithm W¶
W's substitution-passing form is what textbooks and proofs use; production compilers run J (next subsection). Its error behavior — blame the application whose two synthesized types clash — survives in compilers that infer bottom-up, such as SML/NJ, whose elaborator reports "operator and operand don't agree" with both types. The lab's W.cpp reference (solutions/labs/ch07-hm/src/W.cpp) is a direct transcription of Algorithm 7.2.7.
W-style blame in SML/NJ 110.79: the application, not the argument
Reproduce (SML/NJ 110.79):
mkdir -p sml && cat > sml/deep.sml <<'EOF'
val g = fn h => h 1
val r = g (fn b => if b then 0 else 1)
EOF
sml sml/deep.sml < /dev/null
Output (the banner and the final Uncaught exception lines removed):
[opening sml/deep.sml]
sml/deep.sml:2.5-2.39 Error: operator and operand don't agree [tycon mismatch]
operator domain: int -> 'Z
operand: bool -> [int ty]
in expression:
g (fn b => if b then 0 else 1)
What to notice: SML/NJ synthesizes the operator's type (int -> 'Z for g's parameter) and the operand's (bool -> int, because the if made b a bool) and fails when unifying them at the application g (…) — row "at e1 e2" of Algorithm 7.2.7. The lab corpus's 38-deep-mismatch.mml is the same program; its # error-wj header points at the application too.
Algorithm J¶
OCaml's type checker is Algorithm J with levels: type nodes are mutable (Types.type_expr), Ctype.unify links them in place, and generalization compares levels (Lesson 7.3) [OCAML-Ctype]. GHC fills mutable meta type variables (TcMType) as its solver discovers equalities [GHC-Solver]. rustc uses union-find tables with snapshots (InferCtxt in compiler/rustc_infer/src/infer/mod.rs) [RUSTC-Infer].
The principal types J computes, from OCaml 4.14 and from the lab
Reproduce (OCaml 4.14.1; the lab's reference build):
mkdir -p ml && cat > ml/fold.ml <<'EOF'
let rec fold = fun f -> fun acc -> fun l ->
match l with [] -> acc | h :: t -> fold f (f acc h) t
let church_two = fun f -> fun x -> f (f x)
let plus = fun m -> fun n -> fun f -> fun x -> m f (n f x)
let four = plus church_two church_two
EOF
ocamlc -i ml/fold.ml
Output (complete):
val fold : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
val church_two : ('a -> 'a) -> 'a -> 'a
val plus : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c
val four : ('_weak1 -> '_weak1) -> '_weak1 -> '_weak1
What to notice: fold and church_two are the lab corpus's 10-fold.mml and 16-church.mml goldens. four is an application, so the value restriction (Lesson 7.3) leaves its variable weak ('_weak1) where the lab's closed program 16-church.mml prints ('a -> 'a) -> 'a -> 'a for the whole program's type.
Algorithm M¶
OCaml checks many forms against an expected type: type_expect in typing/typecore.ml receives the type the context expects and unifies at the leaf, so its errors read "This expression has type … but an expression was expected of type …" [OCAML-Typecore]. GHC passes an expected type (ExpRhoType) into tcExpr and tcApp [GHC-App]. Both are M-like where the type is known and W/J-like elsewhere.
M-style blame in OCaml 4.14: the leaf that contradicts the expectation
Reproduce (OCaml 4.14.1):
mkdir -p ml && cat > ml/deep.ml <<'EOF'
let g = fun h -> h 1
let r = g (fun b -> if b then 0 else 1)
EOF
ocamlc -i ml/deep.ml
Output (complete):
File "ml/deep.ml", line 2, characters 23-24:
2 | let r = g (fun b -> if b then 0 else 1)
^
Error: This expression has type int but an expression was expected of type
bool
because it is in the condition of an if-statement
What to notice: OCaml pushed g's parameter type int -> 'a into the λ, so b : int, and the condition's expected type bool then clashes at b — exactly where the lab's Algorithm M reports 38-deep-mismatch.mml (# error-m: 6:16, the b in if b), while SML/NJ above (W-style) blamed the whole application.
8. Comparison¶
| Technique | Power / precision | Speed (asymptotic · practical) | Output / error quality | Implementation effort | Typical use |
|---|---|---|---|---|---|
| Let-polymorphism (HM) | Principal types for every typable program (Theorem 7.2.11); rank-1 only, λ-bound variables monomorphic (Proposition 7.2.10) | DEXPTIME-complete · near-linear in practice (Lesson 7.3) | Types need no annotations; errors can be far from the mistake | The rules are small; generalization needs care | ML, OCaml, Haskell 98, F#, the lab's MiniML |
| Algorithm W | Sound and complete (Theorem 7.2.11) | \(\Theta(n^2)\) extra on nested lets · lab: 286 ms at \(n = 2000\) | Blames the application where two synthesized types clash | Low; purely functional | Proofs, teaching, reference implementations |
| Algorithm J | Same results as W (Theorem 7.2.12) | Near-linear with union-find and levels · lab: 0.87 ms at \(n = 2000\) | Same locations as W | Medium: mutable graph, dereferencing | OCaml, GHC, rustc, SML/NJ — every production HM |
| Algorithm M | Same types as W; fails no later (Theorem 7.2.13) | As W, one unification per leaf more · lab: 818 ms at \(n = 2000\) (substitution-based) | Blames the leaf that contradicts the expected type | Low; like bidirectional checking | OCaml's type_expect, GHC's expected types; error-reporting passes |
Comparison-lab results (reproduce with build/<preset>/bin/ch07-hm-bench; reference solutions, RelWithDebInfo, the course container): on letChain with \(n = 250, 500, 1000, 2000\), W takes 4.2, 13.8, 58.4, 286 ms, J 0.11, 0.20, 0.54, 0.87 ms and M 10.8, 39.1, 153, 818 ms; on nestedLets (a λ-bound variable in every scheme's environment) W takes 1036 ms and J 1.95 ms at \(n = 2000\); on pairTower all three are exponential (at \(n = 14\): W 672, J 470, M 742 ms for a 338 285-character type). All three agree on every corpus program's type (tests ch07.HM.L1_*–L3_*) and on 500 random programs.
Choose W to learn, to prove, and to cross-check. Choose J (with levels, Lesson 7.3) for any real implementation. Choose M — or bidirectional propagation where types are known — when error locations matter more than a few percent of speed; production checkers mix J's in-place unification with M's expected types.
9. Assessment¶
| Technique | Quiz ids | Drill | Flashcard tag | Exercises |
|---|---|---|---|---|
| Let-polymorphism | lambda-vs-let, principal-type |
generalization |
let-polymorphism |
lab L1 |
| Algorithm W | w-unifications, w-subterm-type |
hm-trace |
algorithm-w |
lab L1 |
| Algorithm J | j-links, w-vs-j-cost |
hm-trace (the J remark in --solution) |
algorithm-j |
lab L2 |
| Algorithm M | m-error-position, m-expected-type |
— (M's traces are in the quiz and the lab's L3 corpus; the drill traces W, whose error positions M improves on) | algorithm-m |
lab L3 |
References¶
See the chapter references.