Type Inference (Hindley–Milner)
Type checking assumed
the programmer wrote the types down. But in ML, Haskell, OCaml, Rust and modern TypeScript you can write
let twice = f => x => f(f(x)) with no annotation at all, and the compiler will calmly report
its type as (\alpha \to \alpha) \to \alpha \to \alpha. That feat is
type inference: reconstructing the most general type of every expression from its
use, with nothing declared. The Hindley–Milner (HM) system is the crown jewel
here — it infers a principal (most general) type for every well-typed program, and does so
completely automatically. It is one of the most beautiful results in all of programming languages.
The engine has three moving parts. Invent a fresh type variable for every unknown; walk
the AST generating constraints (equations between type expressions) that the code forces
to hold; then solve those equations by unification. The solution is a
substitution mapping type variables to types — and applying it to the program's top-level variable yields
its inferred type.
Type variables and constraints
Start ignorant. Give the unknown type of every leaf and every subexpression its own fresh variable
\alpha, \beta, \gamma, \dots. Then each construct constrains those
variables. Consider inferring the type of f in f(x) = x + 1. Let
x : \alpha. The subexpression x + 1 forces, by the
+ rule, \alpha = \texttt{int} and gives the body type
\texttt{int}. So f : \alpha \to \texttt{int} together
with \alpha = \texttt{int} — i.e.
f : \texttt{int} \to \texttt{int}. Each rule from type checking becomes, in
reverse, a generator of equations:
\text{application } f(e):\quad \tau_f \;=\; \tau_e \to \beta \quad(\beta \text{ fresh}),\qquad \text{result type} = \beta.
Inference is thus two clean phases: a downward/upward walk that emits a set of equations, and a
solver that makes them all true simultaneously. All the cleverness lives in the solver.
Unification: making two type terms equal
Type expressions are just trees (terms): a constructor with children. Unification —
Robinson's algorithm, 1965 — takes two such terms and finds the most general substitution that
makes them identical, or fails if none exists. The rules are exactly what you would guess: a variable
unifies with anything (bind it); two identical constructors unify by unifying their children pairwise; two
different constructors clash.
Unifying \alpha \to \beta with \texttt{int} \to \texttt{bool}
descends the two arrow-trees in lock-step: the argument sides give
\alpha = \texttt{int}, the result sides give
\beta = \texttt{bool}, and the substitution
\{\alpha \mapsto \texttt{int},\ \beta \mapsto \texttt{bool}\} falls out. That
substitution, applied everywhere, is the inferred type. This is the heart of Milner's Algorithm
W: infer a type for each subterm, and unify at every point the language demands two types agree.
The occurs check
One rule keeps unification honest. When you are about to bind a type variable
\alpha to a term \tau, you must first check that
\alpha does not itself occur inside \tau. This
is the occurs check. Try to unify \alpha with
\alpha \to \alpha: binding \alpha \mapsto \alpha \to \alpha
would demand a type equal to its own function type, an infinite type
((\dots \to \dots) \to \dots) with no finite tree. The occurs check spots
\alpha inside \alpha \to \alpha and fails the
unification — correctly reporting that no (finite) type exists. This is exactly the check that flags the
classic self-application f => f(f) as untypable in HM.
// Type terms: a variable, or a constructor (e.g. "int", "->", "list") with args.
type Ty =
| { kind: "var"; name: string }
| { kind: "con"; name: string; args: Ty[] };
const tv = (name: string): Ty => ({ kind: "var", name });
const con = (name: string, args: Ty[] = []): Ty => ({ kind: "con", name, args });
type Subst = Record<string, Ty>;
// Apply a substitution to a type (follow variable bindings, recursively).
function apply(s: Subst, t: Ty): Ty {
if (t.kind === "var") return s[t.name] ? apply(s, s[t.name]) : t;
return { kind: "con", name: t.name, args: t.args.map((a) => apply(s, a)) };
}
// Does variable `name` occur inside t? (after applying current substitution)
function occurs(name: string, t: Ty, s: Subst): boolean {
const r = apply(s, t);
if (r.kind === "var") return r.name === name;
return r.args.some((a) => occurs(name, a, s));
}
// Robinson unification. Returns an extended substitution or throws.
function unify(a: Ty, b: Ty, s: Subst): Subst {
a = apply(s, a); b = apply(s, b);
if (a.kind === "var") {
if (b.kind === "var" && b.name === a.name) return s;
if (occurs(a.name, b, s)) throw new Error(`occurs check: ${a.name} in ${show(b)} — infinite type`);
return { ...s, [a.name]: b }; // bind the variable
}
if (b.kind === "var") return unify(b, a, s);
if (a.name !== b.name || a.args.length !== b.args.length)
throw new Error(`cannot unify ${show(a)} with ${show(b)}`);
for (let i = 0; i < a.args.length; i++) s = unify(a.args[i], b.args[i], s); // children pairwise
return s;
}
function show(t: Ty): string {
if (t.kind === "var") return t.name;
if (t.name === "->") return `(${show(t.args[0])} -> ${show(t.args[1])})`;
return t.args.length ? `${t.name}(${t.args.map(show).join(",")})` : t.name;
}
// 1) Unify α -> β with int -> bool.
const arrow = (x: Ty, y: Ty) => con("->", [x, y]);
let s = unify(arrow(tv("a"), tv("b")), arrow(con("int"), con("bool")), {});
console.log("a =", show(apply(s, tv("a"))), " b =", show(apply(s, tv("b"))));
// 2) The occurs check: α with α -> α must FAIL.
try { unify(tv("a"), arrow(tv("a"), tv("a")), {}); }
catch (e) { console.log("caught:", (e as Error).message); }
The first unification prints a = int, b = bool; the second is caught by the occurs check. Those
twenty-odd lines are, essentially, the whole solver at the core of every ML-family type checker.
Let-polymorphism and generalization
Inference so far gives each variable one type. But the identity function
id = x => x should be usable at many types in the same program:
id(3) and id(true) both. HM achieves this with let-polymorphism.
When a let-bound value is inferred, any type variables left unconstrained by the
environment are generalized — universally quantified into a type scheme
\forall \alpha.\ \alpha \to \alpha. Each use then
instantiates the scheme with fresh variables, so id(3) and
id(true) get independent copies and neither pins the other.
The subtlety — and the reason it is let-polymorphism, not lambda-polymorphism — is that a
function's own parameter is not generalized while you are still inferring the
function body. Inside x => …, the parameter x has a single monomorphic type; it
would be unsound to let it shape-shift mid-inference. Generalization happens only at a
let boundary, once the value's type is fully known and its free variables are provably
independent of the surrounding context. This one rule is what makes HM both sound and wonderfully
expressive.
Everywhere the compiler "just knows" the types. ML and OCaml are HM's birthplace — full
inference, annotations optional. Haskell extends HM with type classes (the
Num a => you see in signatures is the constraint HM couldn't express alone).
Rust uses HM-style inference locally — inside a function body you rarely write types,
though Rust deliberately requires them at function boundaries for readability and better errors.
TypeScript and Swift lean on unification-based inference for local
variables and generics. The 1978 algorithm still runs, in spirit, in the editor autocompleting your code
right now — a rare case of a piece of deep theory that became invisible infrastructure.
The first thing beginners "optimise away" is the occurs check — it seems like a fussy edge case. It is not:
without it, unifying \alpha with \alpha \to \alpha
succeeds, builds a cyclic type term, and the inferencer either loops forever printing an infinite type or
silently accepts nonsense like f => f(f). The rule «never bind
\alpha to a term containing \alpha» is what keeps
every inferred type a finite tree. If your homemade inferencer hangs, suspect a missing occurs check first.
The second trap is over-generalizing. It is tempting to think "every type variable can be
\forall-quantified." No: a variable may be generalized only if it is
not free in the environment — a lambda parameter is monomorphic within its body,
and only a let-bound definition generalizes. Generalize a parameter too eagerly and you
"prove" unsound programs type-correct; this is exactly why HM restricts polymorphism to let,
and why let f = fun x -> … and fun x -> let f = … can infer different types.