Principal Types and Parametricity

Two of the deepest facts about Hindley–Milner polymorphism close this module. The first looks inward, at the inference algorithm: whatever type W hands back is not merely a type but the type — the single most general one, the principal type, from which every other valid typing is carved by substitution. The second looks outward, at the meaning of the type itself: a polymorphic type is so constraining that it dictates, for free, powerful theorems about every function that could ever have it — Reynolds' and Wadler's parametricity, the source of "theorems for free". One says inference is optimal; the other says the types you infer are astonishingly informative. Together they explain why HM types feel less like bookkeeping and more like specifications.

The principal-type property

Order types by generality. Say scheme \sigma_1 is more general than \sigma_2, written \sigma_1 \sqsubseteq \sigma_2, when \sigma_2 can be obtained from \sigma_1 by instantiating its quantified variables. Thus \forall\alpha.\,\alpha\to\alpha is more general than \mathsf{Int}\to\mathsf{Int}, which sits below it as a special case.

Every typable expression e has a principal type scheme \sigma^\ast: it is a valid type for e, and every valid type for e is an instance, \sigma^\ast \sqsubseteq \sigma for all derivable \sigma.
Algorithm W computes it. The principal type is not just an existence claim — W returns it, because unification returns most-general unifiers and generalisation quantifies maximally. Optimality of the local steps compounds into optimality of the whole.
The principal type is unique up to renaming of its bound type variables.

The reveal shows the lattice for the identity function: the principal \forall\alpha.\,\alpha\to\alpha at the top, with each concrete instance hanging beneath it as a substitution. Every legal type for id is somewhere in this cone; W finds the apex.

Principality is what makes separate compilation and clean module interfaces possible: a function can be given its principal type once, published, and every caller instantiates that one scheme to their needs. Without a most general type there would be no canonical signature to expose — you would have to guess how specifically to commit, and guess wrong.

What a polymorphic type forbids

Here is the pivot from inference to meaning. A parametric function, we said, cannot inspect the type it is handed. That negative — "it may not look" — has an astonishingly positive consequence: the type alone tells you almost everything the function can do. Consider the humblest signature:

f : \forall\alpha.\,\alpha \to \alpha.

What functions can have this type? The caller supplies \alpha and a value of type \alpha; f must return a value of type \alpha. But f knows nothing about \alpha — it cannot conjure an \alpha from thin air, cannot test it, cannot transform it, because it has no operation that works at an arbitrary type. The only value of type \alpha it can possibly return is the one it was given. So (ignoring nontermination and effects) the identity is the unique inhabitant of \forall\alpha.\,\alpha\to\alpha. The type is the specification. Compare \forall\alpha.\,\alpha\to\alpha\to\alpha: a function must return one of its two arguments, and by parametricity it can only ever return the first or (consistently) the second — exactly the two Booleans. The type pins the behaviour down to a finite menu.

Polymorphic type	What parametricity forces
\forall\alpha.\,\alpha\to\alpha	must be the identity
\forall\alpha.\,\alpha\to\alpha\to\alpha	returns 1st or 2nd arg (the two "Booleans")
\forall\alpha.\,\mathsf{List}\,\alpha\to\mathsf{List}\,\alpha	output is a rearrangement/selection of the input's elements — no new elements can appear
\forall\alpha.\,\alpha\to\mathsf{Int}	ignores its argument; returns a fixed integer

Parametricity: theorems for free

Reynolds (1983) made this precise with his abstraction theorem, and Wadler (1989) popularised its consequences under the irresistible title "Theorems for Free!". The core idea is relational: interpret each type not as a set of values but as a relation between two interpretations, and read a universally quantified type as "related inputs go to related outputs, for every choice of relation". A term's parametricity theorem then falls straight out of its type.

Any function m : \forall\alpha\,\forall\beta.\,(\alpha\to\beta)\to\mathsf{List}\,\alpha\to\mathsf{List}\,\beta satisfies, for all f and all element functions g:
m\,f \circ \mathsf{map}\,g \;=\; \mathsf{map}\,(f\circ g') \circ m\,g' — more usefully, the special case \mathsf{map}\,f \,(m\,\mathrm{id}\,xs) = m\,f\,(\mathsf{map}\,\mathrm{id}\,xs), i.e. m commutes with \mathsf{map}.
You proved a law about every such m — reverse, tail, take, filter-by-position — from its type alone, having read not one line of its code.

That is the "for free" part: the theorem is a gift attached to the signature. The intuition is the same each time — a parametric function treats the elements as opaque black boxes, so relabelling every element with f before it runs, or after, cannot change which positions survive or move; only the labels differ. Parametricity turns that "it can't peek" into a rigorous equation.

Checking a free theorem empirically

A free theorem is a proof, not a test — but seeing it hold is bracing. The naturality law for any position-based list function m says \mathsf{map}\,f \,(m\,xs) = m\,(\mathsf{map}\,f\,xs): mapping f then reshaping equals reshaping then mapping. Below we take several genuinely parametric m's (reverse, drop-first, every-other) and a non-trivial f, and check both sides agree — then show a non-parametric function (one that peeks at values) breaking the law. Press Run.

const map = <A, B>(f: (a: A) => B, xs: A[]): B[] => xs.map(f); const eq = (a: number[], b: number[]): boolean => a.length === b.length && a.every((x, i) => x === b[i]); // Parametric list-to-list functions: they only reorder/select by POSITION, // never inspecting the element values. Their free theorem: map f . m == m . map f const reverse = <A>(xs: A[]): A[] => [...xs].reverse(); const dropFirst = <A>(xs: A[]): A[] => xs.slice(1); const everyOther = <A>(xs: A[]): A[] => xs.filter((_, i) => i % 2 === 0); const f = (x: number): number => x * 10 + 1; // any element function const xs = [1, 2, 3, 4, 5]; for (const [name, m] of [["reverse", reverse], ["dropFirst", dropFirst], ["everyOther", everyOther]] as const) { const lhs = map(f, m(xs)); // map f then reshape const rhs = m(map(f, xs)); // reshape then map f console.log(name.padEnd(10), "map f ∘ m =", JSON.stringify(lhs), " m ∘ map f =", JSON.stringify(rhs), " →", eq(lhs, rhs) ? "FREE THEOREM HOLDS" : "FAILS"); } // A NON-parametric function that inspects values (keeps evens). It has type // (number[] -> number[]), NOT ∀α. [α] -> [α] — so parametricity does NOT apply, // and the naturality law can break: const keepEven = (xs: number[]): number[] => xs.filter((x) => x % 2 === 0); const lhs = map(f, keepEven(xs)); const rhs = keepEven(map(f, xs)); console.log("keepEven ", "map f ∘ m =", JSON.stringify(lhs), " m ∘ map f =", JSON.stringify(rhs), " →", eq(lhs, rhs) ? "holds" : "BREAKS (not parametric!)");

Every parametric reshaper obeys the law on the nose; keepEven breaks it, because it looks at the values — so it cannot have the polymorphic type \forall\alpha.\,\mathsf{List}\,\alpha\to\mathsf{List}\,\alpha, and forfeits the free theorem. Behaviour is dictated by type: earn the polymorphic signature and the law is yours; peek at the data and you lose both.

This is the philosophical shock of parametricity, and it is worth sitting with. In an ordinary language, a signature like int f(int) tells you almost nothing — f could square, negate, print to a file, or launch a missile. But \forall\alpha.\,\alpha\to\alpha tells you everything: it must be the identity. The generality of the type is not weakness but strength — the more polymorphic a type is, the fewer functions inhabit it, and so the more the type reveals. Philip Wadler's slogan captures it: the type of a polymorphic function is a theorem, and the function is its proof (the Curry–Howard correspondence made practical). This is why seasoned Haskell and ML programmers "type-driven develop": they write the most general type they can, and let parametricity shrink the space of possible implementations until, often, only the right one is left — sometimes uniquely, so the compiler could all but write the body itself.

Parametricity is a theorem about a pure, total, parametric calculus. Bolt on the features real languages have and the guarantees weaken or vanish. Nontermination: in a language with general recursion, \forall\alpha.\,\alpha\to\alpha is inhabited not only by the identity but by the everywhere-undefined function \bot — the "free" theorems must be restated "up to \bot", and some fail outright. Effects: a function that secretly logs, mutates, or throws is no longer parametric even if its type says \forall\alpha, because the effect can depend on or reveal the value. Haskell's seq is the notorious spoiler — it can observe whether an argument terminates, breaking parametricity and quietly invalidating certain free theorems, which is exactly why adding seq to the language was controversial. And reflection / type-case (Java's instanceof, run-time type information, typeof) destroys parametricity by construction, since the whole point is to inspect the type the theorem assumed opaque. The rule of thumb: a free theorem is only as trustworthy as the parametricity of the language you invoke it in — read the fine print before you bank on it.