Let-Polymorphism and the Hindley–Milner System
We have just seen that full System F is gloriously expressive and hopelessly uninferable. The
Hindley–Milner type system (HM) is the engineering masterstroke that recovers
almost all of the practical value of polymorphism while keeping a compiler able to reconstruct
every type on its own — no annotations, ever. It is the type system underneath ML, OCaml, F#, Haskell
(at its core), Elm, and the local inference of Rust and TypeScript. The trick is not to add power but
to subtract it, in exactly the right place.
HM keeps two ideas from System F — universally quantified types, and instantiating them at each use —
but it disciplines where quantifiers may appear and when they may be introduced.
Those two disciplines, the prenex restriction and
let-generalisation, are the whole story of this lesson.
Types, and a level above them: type schemes
HM stratifies its type language into two layers. Monotypes
\tau are the ordinary types — variables, base types, and arrows — with
no quantifier inside them:
\tau \;::=\; \alpha \;\mid\; \mathsf{Int} \;\mid\; \mathsf{Bool} \;\mid\; \tau \to \tau.
Above them sit type schemes (also called polytypes)
\sigma, which are a monotype wrapped in zero or more universal quantifiers,
all at the very front:
\sigma \;::=\; \tau \;\mid\; \forall\alpha.\,\sigma.
A scheme like \forall\alpha.\,\alpha\to\alpha is legal; a monotype like
\alpha\to\alpha is legal. But there is no way to build a
type with a quantifier inside an arrow, such as
(\forall\alpha.\,\alpha\to\alpha)\to\mathsf{Int}. Every quantifier is forced
to the outermost prenex position. This is the single restriction that separates HM
from System F, and it is precisely what makes inference decidable: with quantifiers only at the top,
there is always a most general way to instantiate, and unification can find it.
Generalisation and instantiation: the two half-moves
Schemes and monotypes are related by two operations that are formal inverses of each other. They are
the load-bearing beams of the entire system.
-
Instantiation \sigma \sqsubseteq \tau: a scheme
\forall\alpha_1\dots\alpha_n.\,\tau' may be specialised by
replacing its bound variables with any monotypes,
\tau = \tau'[\alpha_i \mapsto \tau_i]. This happens at every
use of a variable.
-
Generalisation \mathsf{gen}(\Gamma,\tau) = \forall\bar{\alpha}.\,\tau:
close a monotype over exactly the type variables that are free in
\tau but not free in the context
\Gamma, i.e. \bar\alpha = \mathrm{ftv}(\tau) \setminus \mathrm{ftv}(\Gamma).
This happens only at a let.
The side-condition on generalisation — quantify only the variables not free in the context —
is subtle and essential. A type variable that also appears in \Gamma is
still tied to some enclosing binding (a \lambda-parameter, say); it is
not free to vary, so we must not quantify it. Get this wrong and you can "prove" that a
function argument has every type at once — an unsoundness. Get it right and generalisation captures
exactly the freedom the value genuinely has.
The rule that names the system: LET
Here is the crux. In HM, a \lambda-bound variable is
monomorphic — it has a plain monotype, fixed across the whole function body. A
\mathsf{let}-bound variable is polymorphic — its inferred
monotype is generalised into a scheme, and each use may instantiate it afresh. Contrast the two typing
rules:
\dfrac{\Gamma,\ x{:}\tau_1\ \vdash\ t : \tau_2}{\Gamma\ \vdash\ \lambda x.\,t \;:\; \tau_1 \to \tau_2}\ \textsf{(Abs — monomorphic }x\textsf{)}
\dfrac{\Gamma\ \vdash\ e_1 : \tau_1 \qquad \Gamma,\ x{:}\,\mathsf{gen}(\Gamma,\tau_1)\ \vdash\ e_2 : \tau_2}{\Gamma\ \vdash\ \mathsf{let}\ x = e_1\ \mathsf{in}\ e_2 \;:\; \tau_2}\ \textsf{(Let — polymorphic }x\textsf{)}
Look at what the Let rule does that Abs does not: it binds
x to the generalised scheme
\mathsf{gen}(\Gamma,\tau_1) before checking the body
e_2. Two uses of the same \mathsf{let} variable
then instantiate that scheme independently — this is let-polymorphism. A variable
introduces the corresponding scheme by instantiation:
\dfrac{x{:}\sigma \in \Gamma \qquad \sigma \sqsubseteq \tau}{\Gamma\ \vdash\ x : \tau}\ \textsf{(Var — instantiate)}
Why \lambda stays monomorphic — the classic contrast
The reveal below traces the decisive difference. The identity is used at two different types
in one body. Under a \mathsf{let} that is fine; under a
\lambda it is a type error.
With a let, let id = λx. x in (id 3, id true), the binder
id is generalised to \forall\alpha.\,\alpha\to\alpha; the first
use instantiates \alpha := \mathsf{Int}, the second
\alpha := \mathsf{Bool}, and the pair is well typed. Now try to pass the
same function as an argument: λid. (id 3, id true). Here id is
\lambda-bound, so it is monomorphic — it holds a single monotype
\alpha\to\beta. The first use forces
\alpha=\mathsf{Int}; the second forces
\alpha=\mathsf{Bool}; unification of
\mathsf{Int} with \mathsf{Bool}
fails. HM rejects it. To accept it you would need a
rank-2 type, (\forall\alpha.\,\alpha\to\alpha)\to(\mathsf{Int}\times\mathsf{Bool}),
with a quantifier to the left of an arrow — exactly the prenex-violating shape HM forbids. This is the
price of decidability, and it is a price the designers of ML judged well worth paying.
Why the restriction buys decidability
The payoff is a theorem of real weight. Because quantifiers live only at the prenex position, the
subsumption order \sigma \sqsubseteq \tau is generated entirely by
substitution, and unification computes the most general substitution. The two facts combine into the
property that makes HM usable:
-
Every typable HM expression has a principal type scheme — one most general scheme
of which every other derivable type is an instance.
-
Type inference is decidable, and Algorithm W computes the principal scheme (or
reports failure) with no annotations required.
-
By contrast, type inference for full System F — where quantifiers may sit anywhere — is
undecidable. The prenex restriction is exactly the line between the two.
The next lessons make the machine concrete: first unification as a general solver,
then Algorithm W, the recursive procedure that walks a term, generates constraints, solves them by
unification, and generalises exactly at the \mathsf{let}s.
Let-polymorphism, in code
You can watch the two half-moves happen. Below, a scheme is a list of quantified variable names plus a
body monotype. instantiate replaces every quantified variable with a fresh
variable (so two uses never clash); generalise quantifies the free variables of a monotype
that are not pinned down by the environment. Press Run.
type Mono =
| { k: "var"; name: string }
| { k: "arrow"; from: Mono; to: Mono }
| { k: "base"; name: string };
type Scheme = { quantified: string[]; body: Mono };
const V = (name: string): Mono => ({ k: "var", name });
const Arrow = (from: Mono, to: Mono): Mono => ({ k: "arrow", from, to });
const show = (t: Mono): string =>
t.k === "var" ? t.name
: t.k === "base" ? t.name
: "(" + show(t.from) + " -> " + show(t.to) + ")";
const showScheme = (s: Scheme): string =>
(s.quantified.length ? "forall " + s.quantified.join(" ") + ". " : "") + show(s.body);
// Free type variables of a monotype.
function ftv(t: Mono, acc = new Set<string>()): Set<string> {
if (t.k === "var") acc.add(t.name);
else if (t.k === "arrow") { ftv(t.from, acc); ftv(t.to, acc); }
return acc;
}
let counter = 0;
const fresh = (): Mono => V("t" + counter++);
// INSTANTIATION: replace each quantified var by a fresh one (each USE site is independent).
function instantiate(s: Scheme): Mono {
const sub = new Map<string, Mono>(s.quantified.map((q) => [q, fresh()]));
const go = (t: Mono): Mono =>
t.k === "var" ? (sub.get(t.name) ?? t)
: t.k === "arrow" ? Arrow(go(t.from), go(t.to))
: t;
return go(s.body);
}
// GENERALISATION: quantify vars free in `t` but NOT free in the environment.
function generalise(envFtv: Set<string>, t: Mono): Scheme {
const quantified = [...ftv(t)].filter((v) => !envFtv.has(v));
return { quantified, body: t };
}
// let id = λx. x in (id 3, id true)
// Inferred body of id is a -> a. The environment is empty, so generalise fully.
const idMono = Arrow(V("a"), V("a"));
const idScheme = generalise(new Set(), idMono);
console.log("id generalised to:", showScheme(idScheme)); // forall a. (a -> a)
// Two independent uses instantiate with fresh variables:
console.log("use at 3 :", show(instantiate(idScheme)), " then unify its arg with Int");
console.log("use at true :", show(instantiate(idScheme)), " then unify its arg with Bool");
// Contrast: a λ-bound id is monomorphic — NOT generalised, so both uses share one var.
const envFtv = ftv(idMono); // 'a' is in the environment now
const stuck = generalise(envFtv, idMono);
console.log("λ-bound id stays:", showScheme(stuck), " (no quantifier — monomorphic)");
Because the polymorphism is triggered by the \mathsf{let} construct, and
only by it. Milner's 1978 design made a deliberate, almost surgical choice: generalisation
happens at \mathsf{let} bindings and nowhere else. A
\lambda-parameter never gets a scheme. This is why in ML you can write
let id = fn x => x and use id at many types, but if you receive a function
as a parameter you get only one type for it. The name records the mechanism, not just the phenomenon —
it is polymorphism located at let. Fun corollary: desugaring
let x = e1 in e2 into the "equivalent" application
(λx. e2) e1 is not type-preserving in HM, because the
\lambda version makes x monomorphic. The two look
operationally identical but the type system treats them as worlds apart.
Generalising every \mathsf{let} is sound in a pure language, but
the moment you add mutable references it breaks — spectacularly. Consider
let r = ref (λx. x) in …. If HM generalises r to
\forall\alpha.\,\mathsf{ref}(\alpha\to\alpha), you could store an
\mathsf{Int}\to\mathsf{Int} function through one instantiation and read it
back as a \mathsf{Bool}\to\mathsf{Bool} function through another — a type
hole straight to a run-time crash, with no cast in sight. Standard ML's fix is the
value restriction: generalise a \mathsf{let} binding
only when its right-hand side is a syntactic value (a variable, constant, or
\lambda-abstraction) — never a computation that might allocate mutable
state. Function definitions are values, so ordinary polymorphism is untouched; but
ref (λx. x), being an application, is not generalised and stays monomorphic. If you have
ever met the mysterious OCaml error about a "weakly polymorphic" type variable named
'_weak1, this is exactly it: the value restriction refusing to generalise a non-value.
The lesson: let-polymorphism is a theorem about pure terms; real languages must fence it off from
effects.