System F

System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is the simplest type system that supports parametric polymorphism — the ability to abstract functions not just over values but over types. Discovered independently by the logician Jean-Yves Girard and the computer scientist John C. Reynolds in the early 1970s, it is the type-theoretic core of modern functional programming languages and the direct ancestor of the polymorphic type systems of ML, Haskell, and the impredicative universe of the Coq proof assistant.

System F extends the simply typed lambda calculus with universal quantification over types: a term can have the type ∀α.α → α, meaning it is a function that works for any type α. This is not generics in the object-oriented sense — it is a foundational principle that the behavior of a polymorphic function is determined entirely by its type, a property known as parametricity that Reynolds formalized as the abstraction theorem. The expressive power of System F is remarkable: it can encode natural numbers, booleans, lists, and trees as pure lambda terms, without any primitive data types. Yet this power comes with a cost: type inference for System F is undecidable, which is why real programming languages restrict polymorphism to let-bound expressions.