Unification
Type inference keeps generating equations between types: "this argument's type must equal that
parameter's type", "the result here must equal the result there". Each equation is a demand that two
type expressions, possibly riddled with unknowns, be made identical. The engine that
satisfies such demands — that solves equations over symbolic terms — is unification,
and it is one of the genuinely great algorithms of computer science. It powers Hindley–Milner
inference, Prolog's resolution, higher-order theorem provers, and pattern matching in dozens of
systems. Master it once and you understand the beating heart of them all.
The problem, abstractly, is syntactic first-order unification: given two terms built from
function symbols and variables, find a substitution for the variables that makes the two terms
syntactically equal — and, crucially, find the most general such substitution,
committing to as little as the equations force and no more.
Terms, substitutions, unifiers
Fix the vocabulary precisely. A term is a variable
\alpha,\beta,\dots, or a function symbol applied to a fixed number
of argument terms, f(t_1,\dots,t_n). For type inference the function symbols
are the type constructors: {\to} with arity 2,
\mathsf{List} with arity 1, and base types like
\mathsf{Int} as nullary constructors. A substitution
\sigma is a finite map from variables to terms; applying it,
\sigma(t), replaces each variable in t by its
image.
-
A substitution \sigma unifies two terms
s,t when \sigma(s) = \sigma(t) syntactically.
-
\sigma is a most general unifier if every other unifier
\theta factors through it: there is some substitution
\rho with \theta = \rho \circ \sigma. The MGU
commits to the least it possibly can; every solution is one of its specialisations.
Composition is the natural algebra here: (\rho \circ \sigma)(t) = \rho(\sigma(t)),
apply \sigma first and then \rho. The MGU is the
join, the least element, of the ordered set of all unifiers — and Robinson's 1965 theorem is
that whenever a unifier exists, a most general one exists and can be computed.
Robinson's algorithm: recurse, bind, occurs-check
The algorithm compares two terms and dispatches on their shape. There are only three genuinely
different situations.
-
Variable meets anything. To unify a variable
\alpha with a term t: if
t is \alpha itself, do nothing. Otherwise, if
\alpha does not occur in t, extend the
substitution with \alpha \mapsto t. If it does occur — the
occurs check fails, and there is no finite unifier.
-
Constructor meets constructor. To unify
f(s_1,\dots,s_m) with g(t_1,\dots,t_n): if the
symbols differ (f\neq g) or the arities differ
(m\neq n), fail — a clash. Otherwise unify the
arguments pairwise, threading the growing substitution from each solved pair into the next.
-
Symmetry. Term-meets-variable is handled by flipping it to variable-meets-term.
Written as an equation-set transformation, Robinson's rules are:
\begin{aligned}
&\textbf{decompose:} &\; f(\bar s) \doteq f(\bar t) &\;\Rightarrow\; \{ s_i \doteq t_i \} \\
&\textbf{clash:} &\; f(\bar s) \doteq g(\bar t),\ f\neq g &\;\Rightarrow\; \bot \\
&\textbf{eliminate:} &\; \alpha \doteq t,\ \alpha\notin \mathrm{vars}(t) &\;\Rightarrow\; \text{apply } \{\alpha\mapsto t\} \\
&\textbf{occurs:} &\; \alpha \doteq t,\ \alpha\in \mathrm{vars}(t),\ t\neq\alpha &\;\Rightarrow\; \bot
\end{aligned}
A worked unification, as a tree
Unify \alpha \to \mathsf{Int} with
(\mathsf{Bool}\to\beta) \to \gamma. Both are arrows, so we decompose and
walk down both term-trees in lock-step, binding variables as the leaves demand. Reveal it:
The root symbols match ({\to} against {\to}), so
we decompose into two sub-problems: the arguments
\alpha \doteq \mathsf{Bool}\to\beta and the results
\mathsf{Int} \doteq \gamma. The first binds
\alpha \mapsto \mathsf{Bool}\to\beta (occurs check passes —
\alpha is nowhere inside \mathsf{Bool}\to\beta);
the second binds \gamma \mapsto \mathsf{Int}. The most general unifier is
\sigma = \{\,\alpha \mapsto \mathsf{Bool}\to\beta,\ \ \gamma \mapsto \mathsf{Int}\,\},
and \beta stays free — nothing forced it, so the MGU leaves it alone.
Applying \sigma to either side yields the same term,
(\mathsf{Bool}\to\beta)\to\mathsf{Int}: the equation is solved, and solved
as generally as possible.
The occurs check, and why it matters
Try to unify \alpha with \alpha \to \mathsf{Int}.
Binding \alpha \mapsto \alpha\to\mathsf{Int} would make
\alpha stand for a term containing \alpha, hence
for (\alpha\to\mathsf{Int})\to\mathsf{Int}, hence for an
infinite type (\dots\to\mathsf{Int})\to\mathsf{Int} that never
bottoms out. There is no finite term that unifies the pair, so the honest answer is
failure. The occurs check — "refuse to bind
\alpha to a term in which \alpha occurs" — is
precisely the guard that detects this, converting a would-be infinite loop into a clean type error.
-
If two terms are unifiable, a most general unifier exists, and Robinson's
algorithm computes it; if they are not, the algorithm reports failure (a clash or an occurs-check
violation).
-
The MGU is unique up to renaming of variables — any two most general unifiers of
the same problem differ only by a bijective renaming.
-
The algorithm always terminates: each elimination removes a variable from the
problem for good, and there are finitely many.
A wrinkle worth knowing: the naïve substitution-copying algorithm above can be
exponential in time and space, because a bound variable's term may be copied many times.
Practical implementations use a union–find structure over type nodes with in-place
binding and path compression, giving almost-linear behaviour — this is what real ML compilers do, and
it is why occurs-checking is sometimes deferred or amortised.
A complete unifier you can run
Here is Robinson's algorithm in full, over the type language
\alpha \mid \mathsf{Int} \mid \mathsf{Bool} \mid \tau\to\tau \mid \mathsf{List}\,\tau.
It threads an immutable-in-spirit substitution (a Map) and returns it, or null
on failure. Watch a decompose, a bind, and an occurs-check failure all fire. Press Run.
type Ty =
| { k: "var"; name: string }
| { k: "con"; name: string; args: Ty[] }; // Int/Bool = con with []; Arrow = con "->" [a,b]
const V = (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]);
const List = (a: Ty): Ty => Con("List", [a]);
type Sub = Map<string, Ty>;
// Resolve a type to its current representative (follow variable bindings).
function walk(t: Ty, s: Sub): Ty {
while (t.k === "var" && s.has(t.name)) t = s.get(t.name)!;
return t;
}
// OCCURS CHECK: does `name` appear inside `t` (after resolving)?
function occurs(name: string, t: Ty, s: Sub): boolean {
t = walk(t, s);
if (t.k === "var") return t.name === name;
return t.args.some((a) => occurs(name, a, s));
}
// Bind variable `name := t`, returning an extended substitution (or null if occurs-check fails).
function bind(name: string, t: Ty, s: Sub): Sub | null {
if (occurs(name, t, s)) return null; // would create an infinite type
const s2 = new Map(s);
s2.set(name, t);
return s2;
}
// UNIFY x and y under substitution s. Returns the extended MGU, or null on clash/occurs failure.
function unify(x: Ty, y: Ty, s: Sub): Sub | null {
x = walk(x, s);
y = walk(y, s);
if (x.k === "var" && y.k === "var" && x.name === y.name) return s;
if (x.k === "var") return bind(x.name, y, s);
if (y.k === "var") return bind(y.name, x, s);
// both constructors: names and arity must match, then unify args pairwise
if (x.name !== y.name || x.args.length !== y.args.length) return null; // CLASH
let cur: Sub | null = s;
for (let i = 0; i < x.args.length; i++) {
cur = unify(x.args[i], y.args[i], cur!);
if (cur === null) return null;
}
return cur;
}
const show = (t: Ty, s: Sub): string => {
t = walk(t, s);
if (t.k === "var") return t.name;
if (t.name === "->") return "(" + show(t.args[0], s) + " -> " + show(t.args[1], s) + ")";
return t.name + (t.args.length ? " " + t.args.map((a) => show(a, s)).join(" ") : "");
};
// (1) unify (a -> Int) with ((Bool -> b) -> g)
const r1 = unify(Arrow(V("a"), Int), Arrow(Arrow(Bool, V("b")), V("g")), new Map());
if (r1) console.log("MGU 1: a =", show(V("a"), r1), ", g =", show(V("g"), r1), ", b =", show(V("b"), r1), "(free)");
// (2) unify List a with List Bool → a = Bool
const r2 = unify(List(V("a")), List(Bool), new Map());
if (r2) console.log("MGU 2: a =", show(V("a"), r2));
// (3) CLASH: Int with Bool
console.log("clash Int/Bool unifies?:", unify(Int, Bool, new Map()) !== null);
// (4) OCCURS CHECK: a with (a -> Int)
console.log("occurs a/(a->Int) unifies?:", unify(V("a"), Arrow(V("a"), Int), new Map()) !== null);
J. Alan Robinson (1930–2016) published unification in 1965 as the computational core of
a single, mechanisable rule of logical inference he called the resolution principle. Before
Robinson, automated theorem provers drowned in a sea of instantiations — to use a universally
quantified fact you had to guess which specific instances would help. Robinson's insight was that
unification computes the single most general instance that lets two clauses cancel, so the
prover need never guess. Resolution + unification made mechanical theorem proving practical, and a
decade later it became the execution model of Prolog, where every function call is a
unification. The very same algorithm you use to infer that map has type
(\alpha\to\beta)\to\mathsf{List}\,\alpha\to\mathsf{List}\,\beta is the one a
logic engine uses to prove theorems. One idea, two enormous fields.
The occurs check is not an optional optimisation; it is what keeps the type system sound and
the algorithm terminating. Omit it and unifying \alpha with
\alpha\to\mathsf{Int} builds a cyclic term — a "rational tree" — and either
your show function loops forever printing it, or you have quietly admitted an infinite
type that no finite value can inhabit, punching a hole in soundness. Self-application
λf. f f is the canonical trigger: unifying f's type
\alpha with its own domain \alpha\to\beta demands
\alpha \doteq \alpha\to\beta, which the occurs check must reject — and this
is exactly why HM cannot type λf. f f. Curiosity for the brave: some languages
(Prolog by default, and OCaml under -rectypes) deliberately omit the check to
allow cyclic structures — but they know precisely what they are trading away, and you should too before
you copy their unifier.