Great thread OP! Let me add some historical context because I'm a huge Reynolds nerd.

The parametricity theorem was originally stated by John C. Reynolds, who called it the abstraction theorem. Reynolds published this in his landmark 1983 paper "Types, Abstraction and Parametric Polymorphism". Wadler's 1989 paper then popularized and extended it to the setting of Haskell-style polymorphism.

Reynolds' original framing was relational: Reynolds proved an Abstraction Theorem — every term in F₂ satisfies a suitable notion of logical relation — and formulated a notion of parametricity satisfied by well-behaved models.

The key technical idea: types are interpreted as relations, not just sets.

This is where the magic comes from. You're free to choose any relation whatsoever, and the theorem still holds. Choosing relations cleverly gives you all the interesting free theorems.

In programming language theory, parametricity is an abstract uniformity property enjoyed by parametrically polymorphic functions, which captures the intuition that all instances of a polymorphic function act the same way.

The forall a. [a] -> [a] example is super clean, but my personal favourite demonstration of free theorems is the identity type:

Proof via parametricity: let R = {(x, x)} (the singleton relation on an arbitrary point x). The parametricity condition says:

-- (x, x) ∈ R  ⟹  (f(x), f(x)) ∈ R
-- ⟺  f(x) = x  for all x

Since x was arbitrary, f = id. There is only one inhabitant of forall a. a -> a!

Assume M : ∀X. X → X. Let t be a type and x ∈ [[t]]. We show that [[M]] x = x. Interpreting X by the singleton relation, we obtain [[M]] x = x. This holds for any x. Hence, [[M]] is the identity function.

Similarly for forall a b. (a, b) -> (a, b) — you can prove it must be either the identity or swap. And for forall a. a -> a -> a, parametricity tells you it must be either const or flip const (i.e., it always picks the first or always picks the second argument).

Good responses everyone. Now let me talk about what makes this mechanically work — the connection to naturality in category theory.

The free theorem for r : forall a. [a] -> [a]:

  map f ∘ r  =  r ∘ map f

...is exactly the naturality condition for a natural transformation r : List → List in the category of types and functions (Hask)! Free theorems are naturality conditions in disguise.

More generally, Wadler's key insight was to interpret Reynolds' theorem not only as a way of identifying different implementations of the same type, but also as a source of free theorems for polymorphic types.

The deepest version of this connection: Reynolds' abstraction theorem shows how a typing judgement in System F can be translated into a relational statement (in second-order predicate logic) about inhabitants of the type. The relational interpretation is exactly what gives you the naturality squares!

If you want to go deep on this, look up Hermida, Reddy, Robinson — "Logical Relations and Parametricity". It makes the categorical picture completely explicit. Spoiler: it's enriched category theory and it's beautiful 🐾

WadlerCatFan wrote: ...free theorems are naturality conditions in disguise...

YES. And this is why GHC can use parametricity to justify compiler optimisations! The classic example is short-cut fusion (a.k.a. foldr/build fusion).

The key lemma underlying stream fusion / shortcut fusion is derivable from the free theorem for the foldr type. Because foldr has type:

foldr :: (a -> b -> b) -> b -> [a] -> b

...the free theorem tells you exactly how foldr must commute with functions, which enables GHC to rewrite:

map f . filter p . map g
-- ↓ via free theorems (fusion)
foldr (\x acc -> if p (g x) then f (g x) : acc else acc) []

Parametricity is the basis for many program transformations implemented in compilers for the programming language Haskell. The free theorem is literally being used to prove compiler optimisations are safe. That's not just beautiful mathematics — it's load-bearing infrastructure!

For more: Reynolds' Parametricity Theorem (also known as the Abstraction Theorem), a result concerning the model theory of the second order polymorphic typed λ-calculus (F₂), has been used by Wadler to prove some unusual and interesting properties of programs. A purely syntactic version of the Parametricity Theorem shows that it is simply an example of formal theorem proving in second order minimal logic.

Hot take: the most underrated free theorem is the one you get from Church-encoded data types. Consider:

type ChurchBool = forall a. a -> a -> a

-- The free theorem says: any f : ChurchBool satisfies
-- for all g : A → B, x : A, y : A:
--   g (f x y) = f (g x) (g y)

This means f must always pick the first or always pick the second argument — it corresponds exactly to True and False! Free theorems essentially prove that Church encodings are uniquely inhabited by their intended meanings.

And the Church natural numbers: type ChurchNat = forall a. (a -> a) -> a -> a — the free theorem for this type tells you that any such function must equal some n-fold composition. Free theorems justify the entire Church encoding programme!

This connects back to Jean-Yves Girard and John Reynolds independently discovering the second-order polymorphic lambda calculus, F₂. Girard additionally proved a Representation Theorem: every function on natural numbers that can be proved total in second-order intuitionistic predicate logic can be represented in F₂. Reynolds additionally proved an Abstraction Theorem: every term in F₂ satisfies a suitable notion of logical relation.

To close the loop on the "relational parametricity" formalism for newcomers reading this thread:

In programming language theory, parametricity is an abstract uniformity property enjoyed by parametrically polymorphic functions, which captures the intuition that all instances of a polymorphic function act the same way.

The formal machine is logical relations / relational parametricity. We assign to every type τ a relation [[τ]]:

-- Base types: equality relation
[[Int]] = {(n,n) | n ∈ ℤ}

-- Function types: maps related inputs to related outputs
[[A → B]] = {(f,g) | ∀(a,b) ∈ [[A]]. (f a, g b) ∈ [[B]]}

-- Universal types: quantify over ALL relations R
[[∀X. T]] = {(f,g) | ∀A,B, ∀R : A↔B. (f[A],g[B]) ∈ [[T]](R)}

The Parametricity Theorem then states: every well-typed expression e of λF behaves the same as itself according to its type A — that is, (e,e) ∈ E⟦A⟧ρ. At first glance this is underwhelming — of course e behaves the same as itself! The powerful part is that e behaves "according to its type A".

And it is powerful enough to provide behavioral guarantees, which Wadler christened "theorems for free".

Everything in this thread follows from choosing the right relation R at the right type variable. The whole art is picking cleverly! 🐾

Great summary from ProofsArePrograms. Wrapping up the first page: one thing I want to stress is that free theorems aren't just cute party tricks. They're genuinely useful engineering tools:

• ✓ Compiler optimisation — GHC's rewrite rules, fusion, safe code motion
• ✓ API design — a polymorphic type tells users what a function can't do
• ✓ Reasoning about abstract types — representation independence follows from parametricity
• ✓ Verifying Church encodings — uniqueness of Church numerals, booleans, etc.
• ✓ Category theory — naturality conditions come for free

Next page I'll get into higher-rank types and whether free theorems still hold there, plus the drama around unsafeCoerce destroying parametricity. Stay tuned! 🐾

(see page 2 for continuation)