Algorithm W
We now have every part on the bench: the \forall-schemes and monotypes of
Hindley–Milner, generalisation and instantiation, and a unification engine that computes most-general
unifiers. Algorithm W is the machine that bolts them together into a complete type
reconstruction procedure — Milner's 1978 original, tightened and proved correct by
Damas and Milner in 1982. Given a raw, un-annotated expression, W returns its
principal type or a definite failure. No hints from the programmer, no backtracking, one pass.
The name is a historical accident (Milner simply labelled his algorithms V and W), but it stuck, and
"Algorithm W" now means the canonical, syntax-directed presentation of Damas–Milner inference. Its
shape is elegant: a single recursive walk over the syntax tree that, at each node, invents fresh
variables for the unknowns, recursively types the sub-expressions, and calls
unification to reconcile them — accumulating a substitution as it climbs.
The signature, and the invariant
W is a function of two arguments — a typing environment
\Gamma (variables to schemes) and an expression
e — returning a pair: a substitution
S and a monotype \tau.
\mathcal{W}(\Gamma, e) \;=\; (S,\ \tau).
The invariant it maintains is exactly the statement of soundness: S is the
most general substitution such that, after applying it to the environment,
e has type \tau —
S\Gamma \vdash e : \tau. The substitution flows outward and
upward: every recursive call may learn more about the type variables, and those refinements
must be applied to everything discovered so far. Threading S correctly
through the recursion is the one place implementations trip.
The five cases
W is syntax-directed: one rule per form of expression. Let S\Gamma denote
applying substitution S to every scheme in
\Gamma, and let \mathrm{mgu} be unification.
-
Variable x: look up its scheme
\sigma = \Gamma(x) and instantiate it with fresh variables to a
monotype \tau. Return (\varnothing,\ \tau).
-
Abstraction \lambda x.\,e: pick a fresh
\beta for the parameter, run
\mathcal{W}(\Gamma\cup\{x{:}\beta\},\, e) = (S_1,\tau_1), and return
(S_1,\ S_1\beta \to \tau_1). Note x is added
as a monotype \beta — the monomorphic-λ rule in action.
-
Application e_1\,e_2: run
\mathcal{W}(\Gamma,e_1)=(S_1,\tau_1), then
\mathcal{W}(S_1\Gamma,e_2)=(S_2,\tau_2), pick fresh
\beta, and unify
S_2\tau_1 \doteq \tau_2 \to \beta, obtaining
S_3. Return (S_3 S_2 S_1,\ S_3\beta). This is
the step that forces "the function's type is an arrow whose domain matches the argument".
-
Let \mathsf{let}\ x=e_1\ \mathsf{in}\ e_2: run
\mathcal{W}(\Gamma,e_1)=(S_1,\tau_1),
generalise \tau_1 in the (substituted) environment to a
scheme \sigma = \mathrm{gen}(S_1\Gamma,\ \tau_1), then run
\mathcal{W}(S_1\Gamma\cup\{x{:}\sigma\},\, e_2)=(S_2,\tau_2). Return
(S_2 S_1,\ \tau_2). Generalisation happens here and only here.
-
Literal (a constant like 3 or
\mathsf{true}): return its base type,
(\varnothing,\ \mathsf{Int}) or
(\varnothing,\ \mathsf{Bool}).
A worked inference: λf. λx. f x
Let us reconstruct the type of λf. λx. f x — the application combinator — the way W does,
node by node. Reveal each constraint:
Assign f{:}\alpha and x{:}\beta (fresh, both
monomorphic since they are \lambda-bound). Typing the body
f x is an application: the function part f has type
\alpha, the argument x has type
\beta, and W invents a fresh result variable
\gamma and unifies
\alpha \;\doteq\; \beta \to \gamma.
That single unification forces \alpha \mapsto \beta\to\gamma. Rebuilding the
two enclosing abstractions, the whole term has type
\alpha \to \beta \to \gamma, and after applying the substitution:
\lambda f.\,\lambda x.\,f\,x \;:\; (\beta \to \gamma) \to \beta \to \gamma.
Renaming, this is the principal type
(a\to b)\to a\to b — nothing forced b or
a to any concrete type, so both stay free, and the type is as general as the
term allows. W never guessed; every commitment came from a unification, and each unification returned
the most general result.
A complete mini Algorithm W you can run
Here is Damas–Milner W over a tiny language — variables, \lambda,
application, \mathsf{let}, and integer/boolean literals — sharing the
unifier from the previous lesson. Watch it infer the identity, the application combinator, and
genuine let-polymorphism (a let-bound identity used at two types in one
expression). Press Run.
// ---------- Types ----------
type Ty =
| { k: "var"; name: string }
| { k: "con"; name: string; args: Ty[] };
const TV = (name: string): Ty => ({ k: "var", name });
const Con = (name: string, args: Ty[] = []): Ty => ({ k: "con", name, args });
const Int = Con("Int"), Bool = Con("Bool");
const Arrow = (a: Ty, b: Ty): Ty => Con("->", [a, b]);
type Scheme = { vars: string[]; body: Ty }; // ∀vars. body
type Env = Map<string, Scheme>;
type Sub = Map<string, Ty>;
let n = 0;
const fresh = (): Ty => TV("t" + n++);
// ---------- Substitutions ----------
function applyTy(s: Sub, t: Ty): Ty {
if (t.k === "var") { const u = s.get(t.name); return u ? applyTy(s, u) : t; }
return Con(t.name, t.args.map((a) => applyTy(s, a)));
}
const applyScheme = (s: Sub, sc: Scheme): Scheme => {
const s2 = new Map(s); sc.vars.forEach((v) => s2.delete(v)); // don't touch bound vars
return { vars: sc.vars, body: applyTy(s2, sc.body) };
};
const applyEnv = (s: Sub, env: Env): Env =>
new Map([...env].map(([k, sc]) => [k, applyScheme(s, sc)]));
const compose = (s2: Sub, s1: Sub): Sub => {
const out = new Map<string, Ty>();
for (const [k, v] of s1) out.set(k, applyTy(s2, v));
for (const [k, v] of s2) if (!out.has(k)) out.set(k, v);
return out;
};
// ---------- Free variables ----------
function ftvTy(t: Ty, acc = new Set<string>()): Set<string> {
if (t.k === "var") acc.add(t.name); else t.args.forEach((a) => ftvTy(a, acc));
return acc;
}
const ftvScheme = (sc: Scheme): Set<string> => {
const s = ftvTy(sc.body); sc.vars.forEach((v) => s.delete(v)); return s;
};
const ftvEnv = (env: Env): Set<string> => {
const s = new Set<string>(); for (const sc of env.values()) for (const v of ftvScheme(sc)) s.add(v); return s;
};
// ---------- Unification (MGU) ----------
function unify(a: Ty, b: Ty): Sub {
if (a.k === "var") return bindVar(a.name, b);
if (b.k === "var") return bindVar(b.name, a);
if (a.name !== b.name || a.args.length !== b.args.length)
throw new Error("cannot unify " + show(a) + " with " + show(b));
let s: Sub = new Map();
for (let i = 0; i < a.args.length; i++)
s = compose(unify(applyTy(s, a.args[i]), applyTy(s, b.args[i])), s);
return s;
}
function bindVar(name: string, t: Ty): Sub {
if (t.k === "var" && t.name === name) return new Map();
if (ftvTy(t).has(name)) throw new Error("occurs check: " + name + " in " + show(t));
return new Map([[name, t]]);
}
// ---------- Generalise / instantiate ----------
const generalise = (env: Env, t: Ty): Scheme => {
const envV = ftvEnv(env);
return { vars: [...ftvTy(t)].filter((v) => !envV.has(v)), body: t };
};
const instantiate = (sc: Scheme): Ty => {
const s: Sub = new Map(sc.vars.map((v) => [v, fresh()]));
return applyTy(s, sc.body);
};
// ---------- Expressions ----------
type Expr =
| { e: "var"; name: string }
| { e: "lam"; x: string; body: Expr }
| { e: "app"; fn: Expr; arg: Expr }
| { e: "let"; x: string; rhs: Expr; body: Expr }
| { e: "lit"; ty: "Int" | "Bool" };
// ---------- Algorithm W ----------
function W(env: Env, ex: Expr): [Sub, Ty] {
switch (ex.e) {
case "lit": return [new Map(), ex.ty === "Int" ? Int : Bool];
case "var": {
const sc = env.get(ex.name);
if (!sc) throw new Error("unbound: " + ex.name);
return [new Map(), instantiate(sc)];
}
case "lam": {
const b = fresh();
const env2 = new Map(env); env2.set(ex.x, { vars: [], body: b });
const [s1, t1] = W(env2, ex.body);
return [s1, Arrow(applyTy(s1, b), t1)];
}
case "app": {
const [s1, t1] = W(env, ex.fn);
const [s2, t2] = W(applyEnv(s1, env), ex.arg);
const b = fresh();
const s3 = unify(applyTy(s2, t1), Arrow(t2, b));
return [compose(s3, compose(s2, s1)), applyTy(s3, b)];
}
case "let": {
const [s1, t1] = W(env, ex.rhs);
const env1 = applyEnv(s1, env);
const scheme = generalise(env1, t1); // GENERALISE at let
const env2 = new Map(env1); env2.set(ex.x, scheme);
const [s2, t2] = W(env2, ex.body);
return [compose(s2, s1), t2];
}
}
}
function show(t: Ty): string {
if (t.k === "var") return t.name;
if (t.name === "->") return "(" + show(t.args[0]) + " -> " + show(t.args[1]) + ")";
return t.name + (t.args.length ? " " + t.args.map(show).join(" ") : "");
}
const infer = (ex: Expr): string => { n = 0; const [, t] = W(new Map(), ex); return show(t); };
// helpers to build expressions
const v = (name: string): Expr => ({ e: "var", name });
const lam = (x: string, body: Expr): Expr => ({ e: "lam", x, body });
const app = (fn: Expr, arg: Expr): Expr => ({ e: "app", fn, arg });
const lett = (x: string, rhs: Expr, body: Expr): Expr => ({ e: "let", x, rhs, body });
const int: Expr = { e: "lit", ty: "Int" };
const bool: Expr = { e: "lit", ty: "Bool" };
// id = λx. x
console.log("λx. x :", infer(lam("x", v("x"))));
// application combinator: λf. λx. f x
console.log("λf. λx. f x :", infer(lam("f", lam("x", app(v("f"), v("x"))))));
// K = λx. λy. x
console.log("λx. λy. x :", infer(lam("x", lam("y", v("x")))));
// let-polymorphism: let id = λx.x in (id applied at two shapes)
// let id = λx.x in λz. id z (id used, still general)
console.log("let id=λx.x in id:", infer(lett("id", lam("x", v("x")), v("id"))));
// let id = λx.x in id (id 3) → Int, using id at (Int->Int) and Int independently
console.log("let id in id(id 3):", infer(lett("id", lam("x", v("x")), app(v("id"), app(v("id"), int)))));
The last line is the payoff. id is generalised to
\forall\alpha.\,\alpha\to\alpha; the inner id 3 instantiates it
at \mathsf{Int}\to\mathsf{Int} to give an
\mathsf{Int}, and the outer id instantiates it
independently — two separate specialisations of one generalised binding, the very essence of
let-polymorphism, produced with no annotations at all.
Soundness, completeness, and complexity
-
Soundness. If \mathcal{W}(\Gamma,e)=(S,\tau) then
S\Gamma \vdash e : \tau is a valid typing derivation.
-
Completeness / principality. If e has any
typing under \Gamma, then W succeeds and the type it returns is
principal — every other valid typing is a substitution instance of it.
-
Failure is meaningful. If W fails (a clash or an occurs-check violation), then
e is genuinely untypable — the rejection is never a false
alarm.
A famous surprise lurks in the cost. HM inference is DEXPTIME-complete (Kfoury,
Tiuryn, Urzyczyn; Mairson, 1990): a chain of nested \mathsf{let}s can each
double the size of the inferred type, so principal types can grow exponentially in the size of
the program. The witness is a stack of \mathsf{let}-bound pairs, each
pairing the previous binding with itself. Yet on the programs humans actually write — where such
pathological nesting never occurs — W runs in practically linear time, which is exactly why ML
and Haskell compilers infer types faster than you can blink. The worst case is a theorem; the common
case is a joy.
Milner actually gave two algorithms. W is the one that threads an explicit
substitution through the recursion and is easy to prove correct — but is fiddly, because you must apply
S_1 to the environment before the second recursive call, apply
S_2 to \tau_1 before unifying, and compose in the
right order (S_3 S_2 S_1, newest on the left). Get the order wrong and you
"forget" a constraint discovered in a sibling and infer a type that is too general — a real, classic
bug. Algorithm J, Milner's other version, hides all this by using a single mutable
global substitution (in practice, mutable union–find nodes with in-place binding). J is what
every production compiler actually implements — faster, simpler code — while W is what the textbooks
prove theorems about. Same inference, two personalities: W the mathematician, J the engineer.
Two generalisation blunders are near-universal. First: generalising a
\lambda-parameter. W must add a
\lambda-bound variable as a bare monotype
x{:}\beta, never as a scheme — if you generalise there you will
"prove" that a function argument is polymorphic and blow a hole in soundness (this is precisely the
distinction the whole Hindley–Milner design turns on). Second, and subtler: at a
\mathsf{let} you must generalise against the
substituted environment S_1\Gamma, not the original
\Gamma. A type variable that looks free in \tau_1
may already be pinned down by an outer \lambda recorded in
\Gamma; generalising it anyway lets the inner
\mathsf{let} escape its enclosing binding and, again, breaks soundness. The
golden rule: quantify only the variables free in the type and not free in the (current) environment
— and remember the environment has been updated by every substitution so far.