THE SYSTEM F abstract over types, not just values — polymorphism as a calculus
The simply-typed lambda calculus lets you abstract over values. System F adds abstraction over types: a function can take a type as an argument (Λa. λx:a. x is the polymorphic identity, usable at any type). Discovered twice — Girard for proof theory, Reynolds for programming — it is the theoretical core of parametric polymorphism. It is startlingly expressive: you can Church-encode every data structure (numbers, booleans, pairs, lists) using nothing but functions and type abstraction. Its terms are exactly the second-order intuitionistic proofs.
THE TECHNIQUE Λ-abstraction over types; Church-encode data as functions
A Church numeral encodes n as “apply f, n times.” The demo runs church3 = apply succ three times to 0: live demo
HISTORY & CREDIT Girard 1972 · Reynolds 1974
“Polymorphism is a convenience the compiler bolts on.” — it is a calculus in its own right, with a proof-theoretic soul. System F is what generics are underneath, and its terms are literally proofs. The convenience is the visible tip of a logic. cited
1972 · Jean-Yves Girard — System F (in his thesis), for the proof theory of second-order arithmetic. 1974 · John C. Reynolds — independently, “Towards a Theory of Type Structure,” for programming. now · the core of Haskell (System Fω), the target of GHC's internal language.
Two people found the same calculus from opposite ends — logic and programming — because it is the same object. Types are propositions; type abstraction is universal quantification. Girard-Reynolds
RECOMMEND FOR I-13 Church numeral evaluated, computed
On the canonical compiler, the Church numeral 3 — apply succ three times to 0 — evaluates to 3:
$ i13 run t_systemf.i13 # church3 = succ(succ(succ(0)))
three = 3 -- a numeral encoded as iterated application
Recommend: i13 lives in the value half of System F and skips the type half. It has functions and recursion (so Church encodings run — the numeral computes 3) but no type abstraction: you cannot write Λa, because i13 has one type. That is the deliberate floor of the language — it keeps the value model to f64 and the validator single-pass, at the cost of the polymorphism System F formalizes. The proofs-as-programs reading (a term is a proof) is exactly what a typed i13 would gain and an untyped one forgoes.