7 min read
On this page

System F and Beyond

System F (Polymorphic Lambda Calculus)

The Lambda Cube

Syntax and Typing

System F (Girard, 1972; Reynolds, 1974) extends the simply typed lambda calculus with universal type quantification:

Types: A, B ::= alpha | A -> B | forall alpha. A Terms: M, N ::= x | lambda x:A. M | M N | Lambda alpha. M | M [A]

New typing rules:

Gamma |- M : A          (alpha not free in Gamma)
------------------------------------------  (TAbs)
Gamma |- Lambda alpha. M : forall alpha. A

Gamma |- M : forall alpha. A
----------------------------  (TApp)
Gamma |- M [B] : A[alpha := B]

Expressivity

System F is dramatically more expressive than simply typed lambda calculus while retaining strong normalization. All functions provably total in second-order Peano arithmetic are representable -- this includes Ackermann's function and far beyond primitive recursive.

Church encodings in System F (types make encodings precise):

  • Booleans: Bool = forall alpha. alpha -> alpha -> alpha
  • Natural numbers: Nat = forall alpha. (alpha -> alpha) -> alpha -> alpha
  • Pairs: A x B = forall alpha. (A -> B -> alpha) -> alpha
  • Lists: List A = forall alpha. (A -> alpha -> alpha) -> alpha -> alpha
  • Existentials: exists alpha. A = forall beta. (forall alpha. A -> beta) -> beta

Impredicativity

System F is impredicative: the quantifier forall alpha. A ranges over ALL types, including forall-types themselves. For example, (forall alpha. alpha -> alpha) is a valid instantiation for alpha in forall alpha. A.

This creates a circularity: the type being defined is among the types quantified over. Impredicativity is essential for the expressivity of System F (Church encodings require instantiating forall-quantified types at their own type).

Consequences:

  • Type inference is undecidable (Wells, 1999)
  • Type checking is decidable (but only because terms carry explicit type annotations in Church-style)
  • Models are more complex than for predicative systems

Strong Normalization

Theorem (Girard, 1972): Every well-typed term in System F is strongly normalizing.

Proof: Girard's reducibility candidates method extends Tait's logical relations to handle type quantification. For each type A and interpretation xi mapping type variables to sets of terms, define RED_A^xi:

  • RED_alpha^xi = xi(alpha)
  • RED_{A -> B}^xi = {M : for all N in RED_A^xi, M N in RED_B^xi}
  • RED_{forall alpha. A}^xi = {M : for all candidates C, M in RED_{A}^{xi[alpha := C]}}

A "reducibility candidate" must satisfy closure conditions (closure under reduction, head expansion for neutrals). The proof shows that every well-typed term belongs to its type's reducibility set under all interpretations.

Girard's paradox: Extending System F with "Type : Type" (allowing types to classify themselves without restriction) makes the system inconsistent (all types become inhabited). This motivates the universe hierarchy in dependent type theories.

System F-omega

System F-omega adds type-level computation via a kind system:

Kinds: kappa ::= * | kappa -> kappa Type constructors: F ::= alpha | F G | lambda alpha:kappa. F | forall alpha:kappa. F

Kind * classifies proper types. Kind kappa -> kappa' classifies type-level functions (type operators).

Examples:

  • List : * -> * (takes a type, returns a type)
  • Pair : * -> * -> * (binary type constructor)
  • lambda alpha:*. alpha -> alpha : * -> * (type-level identity on function types)

System F-omega subsumes both System F (polymorphism) and the simply typed lambda-calculus at the type level. It is the core of GHC's intermediate language (System FC extends it with type equality coercions).

The Lambda Cube

Barendregt's lambda cube classifies eight type systems along three axes:

  1. Terms depending on types (polymorphism): lambda 2 / System F
  2. Types depending on types (type operators): lambda-omega
  3. Types depending on terms (dependent types): lambda-P

| System | Polymorphism | Type Operators | Dependent Types | |---|---|---|---| | lambda -> (STLC) | No | No | No | | System F | Yes | No | No | | lambda-omega | No | Yes | No | | System F-omega | Yes | Yes | No | | lambda-P (LF) | No | No | Yes | | lambda-P2 | Yes | No | Yes | | lambda-P-omega | No | Yes | Yes | | lambda-C (CoC) | Yes | Yes | Yes |

The Calculus of Constructions (lambda-C) sits at the apex, combining all three features.

Bounded Quantification: System F-sub

System F-sub (Cardelli-Wegner, 1985; Curien-Ghelli, 1992) adds subtyping and bounded polymorphism:

forall alpha <: A. B

The type variable alpha ranges over subtypes of A.

Subtyping rules include:

S <: Top                                    (S-Top)
S <: S                                      (S-Refl)
S <: U    U <: T  =>  S <: T               (S-Trans)
S1 <: T1 -> T2 <: S2  =>  S1 -> S2 <: T1 -> T2  (contravariant in domain)

Key result: Subtyping in full F-sub is undecidable (Pierce, 1994). The proof encodes the halting problem through a chain of subtyping queries. Restricted variants (kernel F-sub, where bounded quantification uses only the bound) are decidable.

F-sub is the theoretical foundation for understanding Java generics, Scala's type system, and bounded polymorphism in OO languages.

Existential Types

Existential types (exists alpha. A) model abstract data types:

pack [B, M] as exists alpha. A   -- introduction (hide implementation type B)
unpack (exists alpha. A) as (alpha, x) in N  -- elimination (use abstractly)

The unpacker cannot observe the hidden type -- it must work parametrically in alpha. This models information hiding: the module provides operations at type A[alpha := B], but clients only see exists alpha. A.

Encoding in System F: exists alpha. A = forall beta. (forall alpha. A -> beta) -> beta

This encoding uses the continuation-passing style: to use an existential, provide a continuation that works for any choice of alpha.

Parametricity and Free Theorems

Parametricity (Reynolds, 1983)

Parametricity formalizes the intuition that polymorphic functions cannot inspect their type arguments. Reynolds defined relational parametricity: a polymorphic function must map related inputs to related outputs, for any logical relation.

Abstraction theorem: If Gamma |- M : A in System F, then M satisfies the logical relation induced by A. For forall alpha. A, this means: for any relation R between types B and C, M[B] and M[C] are related by the lifting of R through A.

Free Theorems (Wadler, 1989)

From the type alone, one can derive free theorems -- equations that all inhabitants of a type must satisfy.

Examples:

  • f : forall a. a -> a: f must be the identity. (The only parametric function of this type.)
  • f : forall a. [a] -> [a]: For any g, map g . f = f . map g. (f commutes with mapping; it can only rearrange/drop/duplicate elements.)
  • f : forall a. [a] -> a: f must select an element at a fixed position (independent of the element type).
  • f : forall a b. (a -> b) -> [a] -> [b]: If f satisfies the free theorem, then f = map. (The type of map has a unique parametric inhabitant.)

Formal derivation: Given type A, construct the free theorem by:

  1. Replace each forall alpha with "for all relations R_alpha"
  2. Arrow types become: if inputs are related, outputs are related
  3. The resulting statement holds for all well-typed terms of type A

Limitations

Free theorems assume:

  • No side effects (seq, exceptions break parametricity in Haskell)
  • No general recursion (divergence complicates the relational interpretation)
  • No type-case or reflection (runtime type inspection violates parametricity)

Parametricity in practice: Haskell approximates parametricity well. Languages with reflection (Java, C#) or unsafe coercions do not guarantee parametricity.

Type Inference in Polymorphic Systems

| System | Type Inference | Type Checking | |---|---|---| | STLC | Decidable (Hindley-Milner) | Decidable | | ML (rank-1 polymorphism) | Decidable | Decidable | | System F (rank-omega) | Undecidable | Decidable | | Rank-2 polymorphism | Decidable | Decidable | | Rank-k (k >= 3) | Undecidable | Decidable | | F-sub | Undecidable | Undecidable (full); Decidable (kernel) |

Hindley-Milner (let-polymorphism) restricts polymorphism to let-bindings (rank-1), recovering decidable inference with principal types. This is the basis of ML and Haskell's type inference.

Practical Manifestations

  • Haskell: Based on System F-omega extended with type classes, GADTs, and type families (System FC)
  • ML/OCaml: Hindley-Milner (rank-1 fragment of System F) with module system providing existentials
  • Scala: Combines F-sub (bounded polymorphism) with path-dependent types
  • Rust: Parametric polymorphism (monomorphized) with trait bounds (bounded quantification)
  • Java/C#: Bounded wildcards approximate existential types; generics are rank-1 with bounds

Key Metatheoretic Properties

| Property | System F | System F-omega | F-sub | |---|---|---|---| | Strong normalization | Yes | Yes | Yes | | Confluence | Yes | Yes | Yes | | Decidable type checking | Yes | Yes | Kernel only | | Decidable type inference | No | No | No | | Subject reduction | Yes | Yes | Yes | | Canonical forms | Yes | Yes | Complex |