Parametric Polymorphism and System F
The simply-typed lambda calculus can type λx:Int. x and it can type
λx:Bool. x, but it cannot type the one identity function that works for both.
Each concrete type demands its own copy of the code. That is a scandal: the term
λx. x does the same thing — return its argument untouched — whatever the type of that
argument. It uses no property of the value at all. A type discipline that forces us to write the
program again for every type has failed to capture the very thing that makes the program
abstract.
Parametric polymorphism is the fix. A parametrically polymorphic function is one
that behaves uniformly for all types — it may not inspect, branch on, or exploit the type of
the data it is handed; it must treat that type as an opaque parameter. Girard (1972) and Reynolds
(1974) independently discovered the calculus that makes this precise: the
polymorphic lambda calculus, or System F. Its move is audacious and
simple — if a function can be abstracted over a value, why not abstract it over a
type?
Two new syntactic forms: type abstraction and type application
System F extends the simply-typed lambda calculus with exactly two new term forms and one new type
form. Where ordinary abstraction \lambda x{:}\tau.\,t binds a
value variable, type abstraction \Lambda\alpha.\,t
binds a type variable \alpha that may appear inside
t. And where ordinary application t\;u feeds a
term a value, type application t\;[\tau] feeds it a type.
| Idea | Term | Type | Reads as |
|---|
| Value abstraction | \lambda x{:}\tau.\,t | \tau\to\sigma | "for any value x of type \tau…" |
| Type abstraction | \Lambda\alpha.\,t | \forall\alpha.\,\sigma | "for any type \alpha…" |
| Value application | t\;u | \sigma | "…applied to this value" |
| Type application | t\;[\tau] | \sigma[\alpha \mapsto \tau] | "…instantiated at this type" |
The universal quantifier \forall\alpha.\,\sigma is the type of a type
abstraction, exactly as \tau\to\sigma is the type of a value abstraction.
It is a genuine type in the object language — you may pass a value of type
\forall\alpha.\,\sigma to another function, store it, return it. This is
the feature that makes System F so much larger than Hindley–Milner, as we will see.
The typing and reduction rules
Two typing rules govern the new forms. Type abstraction introduces a \forall
by checking the body under a context enriched with a fresh type variable; type application eliminates
it by substituting a concrete type for the bound variable.
\dfrac{\Gamma,\ \alpha\ \vdash\ t : \sigma}{\Gamma\ \vdash\ \Lambda\alpha.\,t \;:\; \forall\alpha.\,\sigma}\ \textsf{(T-TAbs)}
\qquad\qquad
\dfrac{\Gamma\ \vdash\ t : \forall\alpha.\,\sigma}{\Gamma\ \vdash\ t\;[\tau] \;:\; \sigma[\alpha \mapsto \tau]}\ \textsf{(T-TApp)}
In T-TAbs the premise carries \alpha in the context to
record that \alpha is now a legal (but abstract) type; the usual
freshness side-condition — \alpha must not already occur free in
\Gamma — keeps the quantifier honest. Computation adds one new redex, the
type-beta rule, mirroring ordinary \beta-reduction:
(\Lambda\alpha.\,t)\;[\tau] \;\longrightarrow\; t[\alpha \mapsto \tau].
A type application against a type abstraction fires by substituting the type argument throughout the
body — types get plugged in wherever \alpha stood, precisely as values get
plugged in for x in (\lambda x.\,t)\,u \to t[x\mapsto u].
The polymorphic identity, built and used
Here is the canonical inhabitant of System F. We wrap the plain identity in a type abstraction, giving
it a universal type; each use site instantiates it at whatever type is needed. Reveal the derivation
step by step:
The term and its type are
\mathsf{id} \;\equiv\; \Lambda\alpha.\,\lambda x{:}\alpha.\,x \;:\; \forall\alpha.\,\alpha\to\alpha.
To use it on an integer we first instantiate, then apply:
\mathsf{id}\;[\mathsf{Int}] : \mathsf{Int}\to\mathsf{Int}, and
\mathsf{id}\;[\mathsf{Int}]\;5 \longrightarrow 5. The type application does
the specialisation the STLC could not: one term, reused at
\mathsf{Int}, at \mathsf{Bool}, even at
\forall\beta.\,\beta\to\beta itself — including instantiating
\mathsf{id} at its own type. That self-instantiation is the sign
of System F's real muscle: impredicativity, which we return to below.
What System F can express
Abstraction over types is not a cosmetic convenience; it is expressive to an almost alarming degree.
With nothing but \Lambda, \lambda,
\to and \forall you can encode the data
types you thought were primitive. The Church encodings become genuinely polymorphic:
\mathsf{Bool} \;\equiv\; \forall\alpha.\,\alpha\to\alpha\to\alpha, \qquad
\mathsf{Nat} \;\equiv\; \forall\alpha.\,(\alpha\to\alpha)\to\alpha\to\alpha.
A Church numeral n is a polymorphic function that, given any type
\alpha, a step \alpha\to\alpha and a start
\alpha, applies the step n times — the type
is "iterate my argument, at any type you like". Lists, pairs, sums, existentials and much of
the algebra of data all fall out as System F types. Girard's astonishing theorem is that this is not
a toy: every function you can prove total in second-order arithmetic is definable in System F,
which is very nearly every function a working mathematician will ever meet.
-
Every well-typed System F term is strongly normalising: every reduction
sequence, in any order, terminates in a unique normal form.
-
Consequently System F is logically consistent as a proof system (via
Curry–Howard, it is second-order intuitionistic propositional logic) and is not
Turing-complete — you cannot write a non-terminating loop in it.
-
The proof requires Girard's method of reducibility candidates; a naïve induction
provably cannot work, because the quantifier ranges over all types including the one being
defined.
Type erasure: polymorphism costs nothing at run time
Because a parametric function may not inspect the type it is passed, the type arguments carry no
information the computation could ever branch on. They are pure specification. This licenses
type erasure: strip every \Lambda\alpha and every
[\tau] and run the untyped lambda term that remains — the answer is the
same. The erasure map \lfloor\cdot\rfloor is
\lfloor \Lambda\alpha.\,t \rfloor = \lfloor t\rfloor, \qquad
\lfloor t\;[\tau] \rfloor = \lfloor t\rfloor, \qquad
\lfloor \lambda x{:}\tau.\,t \rfloor = \lambda x.\,\lfloor t\rfloor, \qquad
\lfloor t\;u \rfloor = \lfloor t\rfloor\,\lfloor u\rfloor.
The erased \mathsf{id} = \Lambda\alpha.\,\lambda x.\,x is just
\lambda x.\,x. This is why a compiler for ML, Haskell or Rust emits
one machine-code body for a generic function and lets every instantiation share it: parametric
polymorphism, unlike C++ templates or Java's reified generics, need not specialise, box, or dictionary-pass
for the type parameter itself. The types were a compile-time contract; at run time they evaporate.
(This is the operational shadow of parametricity, the deep uniformity theorem we meet in the last
lesson of this module.)
// System F terms, and an eraser to the untyped lambda calculus.
// Types: TVar | Arrow | Forall. Terms: Var | Lam | App | TLam | TApp.
type Ty =
| { k: "tvar"; name: string }
| { k: "arrow"; from: Ty; to: Ty }
| { k: "forall"; v: string; body: Ty };
type Term =
| { k: "var"; name: string }
| { k: "lam"; x: string; ty: Ty; body: Term }
| { k: "app"; fn: Term; arg: Term }
| { k: "tlam"; a: string; body: Term } // Λa. body
| { k: "tapp"; fn: Term; ty: Ty }; // fn [ty]
const showTy = (t: Ty): string =>
t.k === "tvar" ? t.name
: t.k === "arrow" ? "(" + showTy(t.from) + " -> " + showTy(t.to) + ")"
: "(forall " + t.v + ". " + showTy(t.body) + ")";
// Type substitution ty[a := s] (used by type-beta reduction).
function substTy(ty: Ty, a: string, s: Ty): Ty {
if (ty.k === "tvar") return ty.name === a ? s : ty;
if (ty.k === "arrow") return { k: "arrow", from: substTy(ty.from, a, s), to: substTy(ty.to, a, s) };
return ty.v === a ? ty : { k: "forall", v: ty.v, body: substTy(ty.body, a, s) };
}
// Erase all type machinery, leaving an untyped lambda term as a string.
function erase(t: Term): string {
switch (t.k) {
case "var": return t.name;
case "lam": return "(\\" + t.x + ". " + erase(t.body) + ")";
case "app": return "(" + erase(t.fn) + " " + erase(t.arg) + ")";
case "tlam": return erase(t.body); // drop Λa.
case "tapp": return erase(t.fn); // drop [ty]
}
}
const A: Ty = { k: "tvar", name: "a" };
// id = Λa. λx:a. x : forall a. a -> a
const id: Term = { k: "tlam", a: "a", body: { k: "lam", x: "x", ty: A, body: { k: "var", name: "x" } } };
const idType: Ty = { k: "forall", v: "a", body: { k: "arrow", from: A, to: A } };
console.log("id :", showTy(idType));
// Instantiate at Int: the type-beta result is Int -> Int
const IntTy: Ty = { k: "tvar", name: "Int" };
const inst = substTy({ k: "arrow", from: A, to: A }, "a", IntTy);
console.log("id [Int] :", showTy(inst));
console.log("erase(id) =", erase(id), " (just the untyped identity)");
A definition is impredicative when it quantifies over a collection that includes the
thing being defined. System F's \forall\alpha.\,\sigma ranges over
all types — and \forall\alpha.\,\sigma is itself a type, so the
quantifier ranges over itself. Concretely, you may write
\mathsf{id}\;[\forall\beta.\,\beta\to\beta]: instantiate the identity at
its own type. This circularity is exactly what makes System F so expressive — and exactly what makes
Girard's normalisation proof so hard, since you cannot define the "meaning" of a
\forall-type by simple induction on types when it may mention itself. The
predicative restriction, where \forall ranges only over
quantifier-free types, is weaker but tamer, and it is essentially the fragment Hindley–Milner lives in.
That single restriction is the border between "inference is decidable" and "inference is undecidable".
It is tempting to hope that if Hindley–Milner can infer types with no annotations, then System F —
being "just a bit more general" — can too. It cannot. Type inference for System F is
undecidable (Wells, 1994): there is no algorithm that, given a bare untyped term, decides
whether it can be decorated with type abstractions and applications to become a well-typed System F
term. The culprit is precisely the impredicative \forall: a variable may
need to be used at two incomparable polymorphic types inside one function body, and there is
no most-general choice to infer. This is why real languages do not offer full System F with
inference. ML and Haskell adopt the restricted Hindley–Milner fragment, where every quantifier sits at
the outermost prenex position and inference is decidable; GHC's higher-rank types recover
slices of System F only by demanding annotations at the polymorphic binders. Do not confuse
"System F is the elegant target calculus" with "System F is what the compiler infers" — it is the
former, never the latter.
Where this sits
System F is the reference calculus of parametric polymorphism: everything about "generics",
"type parameters" and "for-all types" in real languages is a negotiation with this calculus about how
much of it to keep while staying inferable and efficient. The next lesson carves out the exact
sublanguage that stays fully inferable — the prenex fragment at the heart of
Hindley–Milner, the largest slice of System F for which a compiler can recover every type with no help
from the programmer at all.