The Polymorphic Lambda Calculus: System F

In the simply typed lambda calculus, types bought a guarantee: every well-typed term terminates. We paid with general recursion, but if it type checks, it halts. Something strange is sitting in that system, though, right in the identity function.

The same function, many types#

λx. x has type α -> α. It also has type Nat -> Nat, Bool -> Bool, any type you want: a separate derivation per choice of α, though the term never changes. The type system will not let you say that out loud; a library function needs a copy for every type it is called on. The limitation is not in the program. It is in the language we used to describe it.

A quantifier over types#

The fix is to let the type itself say "for any α": forall α. α -> α, one type holding at every α at once. That is polymorphism: one function, every type, no copies.

A polymorphic term has to accept a type as input, so the language gets two new operations. Type abstraction, written with a capital lambda: the polymorphic identity is Λα. λx:α. x. Read it: take a type, then take a value of that type, return the value. Type application plugs a specific type in: apply the polymorphic identity to Nat and you get λx:Nat. x. The typing rules mirror this: forall introduction captures the abstracted type variable, forall elimination substitutes a concrete type. Two new rules, parallel to the term level.

And at runtime, the capital lambdas and annotations have nothing left to do; the checker already used them. Erase them and λx. x is back. Type erasure is why polymorphic languages compile to fast code: a Haskell program carries no types at runtime.

Church encodings, now with types#

In the untyped calculus we built numbers as iterators: the Church numeral for $n$ applies a function $n$ times. The simply typed calculus could type these only at a fixed type (a function from what, to what?). System F answers: any type.

Nat is forall α. (α -> α) -> α -> α: take a function on α and a start, give back an α; a numeral iterates the function. Zero hands back the start, successor applies the function once more, addition threads it through both numerals, multiplication iterates one numeral's iteration inside the other.

Predecessor is the hard one: you cannot peel a layer off an opaque iterator, and Kleene's pair trick, walking a pair up from zero, needs polymorphism to instantiate the pair type at Nat. Exponentiation is the clever one: type-apply the base at α and the exponent at α -> α, and the iteration works out. From there one combinator, hyp-successor, iterates any binary operation on Nat: tetration, pentation, and on up, each rung one line of code. Three tetrated to three is already over seven trillion; three pentated to three is a tower of threes seven trillion high. The simply typed calculus could not type any of this uniformly. F types all of it.

Data from the same quantifier#

Booleans pick one of two options: forall α. α -> α -> α, true picks the first, false the second. A pair of A and B has type forall α. (A -> B -> α) -> α: you build a pair by saying how to use it. Sums are dual: two handlers, case analysis. Lists fold: hand me a combiner and a start; empty echoes zero, cons echoes successor. Even existentials, data with a hidden representation, are a dual trick: the consumer must work for every possible hidden type.

Every standard data structure from one quantifier. And the types count their own inhabitants: up to βη-equivalence, exactly two closed terms at Bool, one per natural number at Nat. The quantifier is doing the counting.

Parametricity#

So how many closed terms have type forall α. α -> α?

One. The identity.

Such a term receives a type it cannot inspect, because types are not values, then a value it cannot inspect either, having no operations on an arbitrary type. The only α it can return is the one it was given.

This is parametricity, proved by John Reynolds in 1983; Philip Wadler called the technique "theorems for free": facts read off a type alone. A function of type forall α. List α -> List α can only reorder, duplicate, or drop elements, having no way to produce an α; one of type forall α β. α -> β -> α must return its first argument.

In the simply typed calculus, a type was a contract on inputs. In F, it is a contract on behavior. And the encodings above were not workalikes: a Church numeral is extensionally indistinguishable from the number it stands for; impredicative polymorphism plus parametricity gives you inductive types for free.

Pause and try: count the closed terms of type forall α. α -> α -> α, and of type forall α β. α -> β -> β.

The first receives two values of an arbitrary type and must return one of that type; it cannot inspect them or build new ones, so it returns the first or the second. Two terms, which is exactly why this type is Bool. The second must produce a β, and the only β in scope is the second argument. One term. The type alone forces the behavior.

A logic in disguise#

System F is also a logic: the arrow is implication, the quantifier is the universal quantifier. A term of type forall α. α -> α is a proof that every proposition implies itself; the identity term is exactly that proof. This is Curry-Howard for second-order propositional intuitionistic logic: types are propositions, terms are proofs, beta reduction is cut elimination.

Now ask what has no inhabitants. forall α. α: you cannot fabricate a value of an arbitrary type. That is false, the proposition with no proof. Explosion still works: type-apply a term of forall α. α at any type and out comes a term of that type; false implies everything. What you cannot do is prove P or not P for an arbitrary P. System F is intuitionistic: to prove something, you have to build it.

Girard did not build System F to write programs. He built it to prove things about second-order arithmetic. John Reynolds, coming from the programming side, invented the same system independently in 1974.

Termination, the second time#

Does the more expressive system still terminate? Jean-Yves Girard proved it does, in a 1971 paper and his 1972 thesis: every well-typed term normalizes, which through Curry-Howard says every second-order proof has a normal form.

The proof is harder than Tait's. The difficulty is impredicativity: forall α ranges over all types, including types that contain forall α, so the naive induction on types defines a thing in terms of itself. Girard's fix, reducibility candidates, sets of terms with a closure property, stands in for the missing induction.

Push impredicativity one step further and it breaks: Girard also showed that a type of all types lets the system encode a Burali-Forti-style paradox, Girard's paradox, and prove false. System F stays safe because types are not themselves terms: there is no type of all types. Rocq (formerly Coq) and Lean want more power and pay with a universe hierarchy, Type zero in Type one in Type two, so nothing contains itself.

Still not Turing complete#

System F types far more: the Ackermann function, which outgrows every primitive recursive function, and in general anything provably total in second-order arithmetic. But not every total function: line up F's programs from Nat to Nat, apply each to its own index, add one, and that diagonal is total but computed by no F program. Every well-typed term still halts. F moved the boundary without erasing it.

The map, and the languages you use#

Henk Barendregt organized all of this into a cube. Terms depending on terms is the simply typed calculus; terms on types, System F; types on types, System F omega; types on terms, dependent types. Three axes, eight corners; the calculus of constructions, ancestor of Rocq and Lean, sits at the far corner, System F omega one corner over from it.

And you have been programming in it. Haskell's forall a., Rust's generics, Java generics all trace back here, with two compilation strategies: Haskell and ML erase types, one block of code for every instantiation; Rust monomorphizes, one specialized copy per type. One catch: type inference for full System F is undecidable (Joe Wells, 1994), so real languages restrict the fragment. ML allows quantifiers only at the outside of a type, the rank-one fragment with Hindley and Milner's decidable inference; Haskell asks for annotations where inference cannot keep up. Every statically typed language picks a point between expressiveness and inference.

The simply typed calculus asked you to pick a type and stick with it. System F lets the type itself say "for any," and the language finally fits the programs you were already writing.

If you remember three things#

1. One quantifier over types gives polymorphism and typed Church encodings of numbers, booleans, pairs, sums, and lists, all erasable at runtime.
2. Parametricity turns types into contracts on behavior: forall α. α -> α has exactly one inhabitant, and theorems read off a type, no code needed.
3. System F is second-order intuitionistic logic in disguise, Girard's reducibility candidates prove every term halts, and your language's generics are an inferable slice of it.