Type Inference and Hindley-Milner

A type system assigns types to terms via a derivable judgment `Γ ⊢ e : τ`. In the Simply-Typed Lambda Calculus, the programmer supplies enough annotations (usually on lambda parameters) that type checking is a straightforward syntax-directed recursion. Type inference removes that requirement: given only `e`, find a type environment and a type such that the judgment is derivable — or report that none exists. HM works with two layers of type syntax. A monotype (or simple type) `τ` is built from type variables `α`, base types like `int` and `bool`, and function arrows: `τ ::= α | int | bool | τ₁ → τ₂`. A type scheme (polytype) `σ` adds universal quantification only at the outermost level: `σ ::= τ | ∀α. σ`. This "prenex, rank-1" restriction — quantifiers only at the top, never nested inside an arrow like `(∀α. α → α) → int` — is exactly what keeps inference decidable and syntax-directed. Full Parametric Polymorphism (System F) allows arbitrary quantifier nesting and famously has undecidable type inference; HM is the fragment where inference is tractable. Two operations connect monotypes and schemes. Instantiation takes a scheme `∀α₁...αₙ. τ` and produces a monotype by substituting fresh, unconstrained type variables for the bound ones — this is what happens every time a `let`-bound name is used. Generalization takes a monotype `τ` derived for a `let`-bound expression and quantifies over all type variables that are free in `τ` but not free in the ambient environment `Γ` — this is what happens once, when the name is defined. The interplay of these two operations, restricted to `let`, is called let-polymorphism: a function can be polymorphic where it is bound, but every individual use site sees one concrete instantiation. This is why `fun f -> (f 3, f true)` — a lambda-bound, not let-bound, parameter — is not typable in HM, while `let f = fun x -> x in (f 3, f true)` is. Underlying everything is unification: given two type expressions possibly containing variables, find the most general substitution that makes them syntactically identical. HM's correctness rests on the fact that unification, when it succeeds, produces a substitution that is most general — any other unifying substitution factors through it. This directly delivers principal types: HM's inference algorithm computes not just a type for `e`, but the single most general type from which every other valid typing of `e` can be obtained by substitution and instantiation.

The classical presentation is Algorithm W, due to Milner, which is syntax-directed on the term structure and threads a substitution through the recursion. An equivalent and often more implementation-friendly view (the one modern compilers actually use) is constraint generation followed by unification: walk the term once to collect a set of equality constraints between types, then solve them all at the end. Both compute the same principal type; we present the constraint-based view first because it separates concerns cleanly, then give Algorithm W's classical formulation.

Step 1 — Constraint generation. Walk the abstract syntax tree, assigning a fresh type variable to every unannotated subterm, and emit an equation each time the term structure demands two types be equal (e.g., a function's argument type must equal the type of the actual argument; both branches of an `if` must agree).

Step 2 — Unification. Solve the collected equations by finding a substitution `S` — a finite map from type variables to types — such that applying `S` to both sides of every equation makes them syntactically equal. Unification proceeds by structural recursion: ``` unify(τ1, τ2): τ1 := resolve(τ1) // follow current substitution τ2 := resolve(τ2) if τ1 == τ2 (same base type, or same variable): return {} // already equal, no new bindings else if τ1 is a variable α: if α occurs free in τ2: fail "occurs check: infinite type" else: return { α ↦ τ2 } else if τ2 is a variable β: return unify(τ2, τ1) // symmetric case else if τ1 = A → B and τ2 = C → D: S1 := unify(A, C) S2 := unify(apply(S1, B), apply(S1, D)) return compose(S2, S1) else if τ1 = base b1 and τ2 = base b2 and b1 == b2: return {} else: fail "type mismatch: cannot unify " + τ1 + " with " + τ2 ``` The occurs check is the safety valve: without it, unifying `α` with `α → int` would silently accept it, producing the "infinite type" `(...→int)→int)→int`, which corresponds to no finite simply-typed term and would make the algorithm loop or produce nonsense downstream. Rejecting it is what keeps unification's output a finite well-formed type.

Step 3 — Generalization and instantiation, at `let`. When inference reaches `let x = e₁ in e₂`, it infers a monotype `τ₁` for `e₁` under the current environment `Γ`, then generalizes: it computes `σ = ∀α₁...αₙ. τ₁` where `α₁,...,αₙ` are exactly the type variables free in `τ₁` (after applying the accumulated substitution) but not free in `Γ`. It binds `x : σ` in `Γ` for checking `e₂`. Every occurrence of `x` inside `e₂` is then instantiated: fresh copies of `α₁,...,αₙ` are substituted, so each use of `x` can pick a different concrete type. Putting this together, here is Algorithm W as a recursive function `W(Γ, e)` returning `(S, τ)` — a substitution and the inferred type of `e` under `Γ`: ``` W(Γ, e): match e: case x (variable): σ := lookup(Γ, x) // must exist, else "unbound variable" τ := instantiate(σ) // fresh vars for each ∀-bound var return (∅, τ) case fun x -> body: α := fresh type variable (S1, τ_body) := W(Γ ∪ {x : α}, body) return (S1, apply(S1, α) → τ_body) case e1 e2: // function application (S1, τ1) := W(Γ, e1) (S2, τ2) := W(apply(S1, Γ), e2) β := fresh type variable S3 := unify(apply(S2, τ1), τ2 → β) S := compose(S3, S2, S1) return (S, apply(S3, β)) case let x = e1 in e2: (S1, τ1) := W(Γ, e1) σ := generalize(apply(S1, Γ), apply(S1, τ1)) (S2, τ2) := W(apply(S1, Γ) ∪ {x : σ}, e2) return (compose(S2, S1), τ2) case literal n: return (∅, int) case true/false: return (∅, bool) instantiate(∀α1...αn. τ): fresh β1,...,βn return τ[α1↦β1, ..., αn↦βn] generalize(Γ, τ): freeVars := ftv(τ) \ ftv(Γ) return ∀freeVars. τ ``` The `let` case is the heart of the algorithm: it is the only place polymorphism is introduced (via `generalize`) and the only place it is exploited across multiple, differently-typed uses (via repeated `instantiate` at each occurrence of `x`).

Time complexity. Unification of two type terms of combined size `n` (as a DAG with sharing, using union-find for variable bindings) runs in O(n α(n)) — essentially linear, where `α` is the inverse Ackermann function from union-find path compression. Algorithm W performs one unification per application node and one substitution-application per recursive call. If substitutions are applied eagerly to the whole environment at every step (as the naive pseudocode above does), each application can cost time proportional to the size of `Γ`, and because types can grow, the overall worst case becomes exponential in the depth of nested `let`-expressions. The canonical pathological example: ``` let f1 = fun x -> (x, x) in let f2 = fun x -> f1 (f1 x) in let f3 = fun x -> f2 (f2 x) in ... let fn = fun x -> f_{n-1} (f_{n-1} x) in fn (fun x -> x) ``` Each `fᵢ` doubles the size of the type of the previous one (nested tuples), so the principal type has size `Θ(2ⁿ)`. Since the output itself is exponentially large, no algorithm computing it explicitly can beat exponential time on this input — the blowup is intrinsic to the specification, not a flaw in Algorithm W. Real implementations mitigate the everyday cost (not this pathological case) by representing types as mutable union-find graphs with sharing rather than copying trees, giving near-linear behavior on typical programs; this is why production compilers (OCaml, GHC, older ML implementations) still ship HM inference rather than something asymptotically "safer."

Space complexity mirrors time: `O(n)` for the constraint/substitution structures on ordinary programs, with the same exponential outlier for the pathological nested-`let` family.

Correctness — soundness. If `W(Γ, e) = (S, τ)` succeeds, then `apply(S, Γ) ⊢ e : τ` is derivable in the HM type system. The proof is by induction on the structure of `e`, mirroring the algorithm's recursion:

• Variable: instantiation of a valid scheme `σ` in `Γ` yields a valid monotype instance by the HM typing rule for variable use (`∀`-elimination).
• Abstraction: by the induction hypothesis, `Γ, x:α ⊢ body : τ_body` under `S1`; the arrow-introduction rule then gives `Γ ⊢ (fun x -> body) : α → τ_body` under the same substitution.
• Application: the induction hypothesis gives typings for `e1` and `e2`; unifying `τ1` with `τ2 → β` and applying the resulting substitution exactly reconciles the arrow-elimination rule's requirement that the argument type match the domain of the function type.
• Let: the induction hypothesis types `e1` as `τ1`; generalization produces a valid scheme because the quantified variables are, by construction, exactly those not constrained by the ambient environment, so instantiating them freely in `e2` cannot violate any assumption already recorded in `Γ`.

Correctness — completeness / principality. This is the deeper theorem: if any typing of `e` exists (i.e., some `Γ' ⊇ Γ` and `τ'` with `Γ' ⊢ e : τ'`), then `W` succeeds and produces `(S, τ)` such that `τ'` is an instance of `τ` under some further substitution and instantiation — `τ` is the most general (principal) type. This rests on the corresponding property of unification: whenever two terms are unifiable at all, the `unify` algorithm above returns a most general unifier (mgu) — any other unifier factors as (mgu) composed with something else. Proving unification finds an mgu is itself an induction on the structure of the two terms, checking each of the four cases (variable, matching heads, mismatched heads) preserves "most-generality," with the occurs check guaranteeing termination and well-formedness (no infinite type is ever silently accepted).

Decidability. Because monotypes are finite first-order terms and quantifiers are restricted to the prenex, top-level position, both unification and generalization terminate, and the whole inference procedure is decidable — a Type checking and inference problem in the full second-order System F setting, by contrast, is not.

Tradeoff to be honest about. HM's decidability and principal-types guarantee come at a real cost: it cannot type `fun f -> (f 3, f true)` because a lambda-bound parameter is never generalized, only `let`-bound names are. Extensions (higher-rank types, `let`-polymorphism escape hatches like explicit type annotations, or the impredicative extensions used in GHC) restore some of this expressive power at the price of losing full principal types or decidable inference.

Trace `let double = fun f -> fun x -> f (f x) in double (fun y -> y + 1) 5` through Algorithm W.

The final, principal type of the whole program is `int`. Notice the crucial moment is step 6: because `double` is bound by `let`, its type variable `δ` is generalized into `∀δ. (δ→δ)→(δ→δ)`, and step 7 creates a fresh instantiation `δ0` for this particular call site. Had `double` instead been a lambda parameter (e.g., inside `fun double -> double (fun y -> y+1) 5`), no generalization step would occur, `δ` would stay a single rigid variable across the whole scope, and — if `double` were then also applied to, say, a boolean-returning function elsewhere in the same scope — inference would fail with a unification conflict, exactly illustrating why let-polymorphism, not lambda-polymorphism, is what HM provides.

:::physicist[Robin Milner|1934–2010|Computer scientist, designer of ML and the LCF theorem prover, Turing Award 1991|Edinburgh} Milner independently rediscovered and operationalized the same idea for the ML programming language in 1978, giving Algorithm W and connecting it explicitly to the practical need for a statically-typed, annotation-free functional language usable inside a proof assistant.

HM inference is the type-checking core of Standard ML, OCaml, F#, Haskell, Elm, and PureScript — in each, the vast majority of function definitions carry no type annotation at all, and the compiler reconstructs everything via unification exactly as described above. Rust's type checker uses a close relative (extended with trait bounds, lifetimes, and no full let-polymorphism inside function bodies) to infer local variable types while still requiring function-signature annotations for modularity and error-message clarity. TypeScript and modern Swift use bidirectional, constraint-based inference engines that are direct intellectual descendants of the constraint-generation-then-unification architecture, adapted to structural and subtype-rich settings. Beyond mainstream languages, unification itself — the general technique of solving equality constraints over trees via substitution — is the same core machinery behind Prolog's resolution engine, term-rewriting systems, and many static analyses (alias analysis, some points-to analyses) that pose their problem as "solve this system of syntactic equations." Understanding HM is therefore not just about ML-family languages: it is the canonical, best-understood instance of constraint-based program analysis, and the natural stepping stone toward richer polymorphic type systems and Parametric Polymorphism such as System F.

Ask the tutor: Can you show me how Algorithm W would fail, step by step, on `fun f -> (f 3, f true)`, and what error message it produces at the point of unification failure?