Parametricity: Theorems for Free

Symptom

Someone hands you a function and no source:

f :: forall a. [a] -> [a]

How much can you say about it? The instinct is nothing: any implementation is possible, that is what polymorphism means.

The opposite is true. You can say a great deal. f cannot inspect the elements, because it does not know their type and has no operations on them. It cannot manufacture new ones for the same reason. Every element in the output must have come from the input. So f can only select, duplicate, drop, and reorder, and whatever it does must depend solely on the length of the list — because length is the only thing about the list it can observe.

From this alone, without seeing a line of the implementation:

for every function g. That is a theorem about code you have never read, derived from its type. It holds for reverse, tail, init, take 3, cycle-and-truncate, and every other inhabitant of that type, including the ones nobody has written yet.

Statement

Parametricity (Reynolds’s abstraction theorem). Related inputs produce related outputs. A polymorphic function must behave uniformly at every type instantiation, because it has no way to observe which type it received.

The mechanical recipe: write the relational interpretation of the type, specialize every relation variable to a function’s graph, and read off the equation. That is it.

Argument

Derive the list theorem. For f :: forall a. [a] -> [a], the relational reading says: for any relation $R$ between $A$ and $A’$, if xs and xs' are related pointwise by $R$, then f xs and f xs' are related pointwise by $R$.

Take $R$ to be the graph of a function $g : A \to A’$, that is $R = {(x, g,x)}$. Then “related pointwise” means xs' = map g xs. The conclusion becomes f xs' = map g (f xs). Substituting gives f (map g xs) = map g (f xs). $\blacksquare$

More free theorems, read off directly:

The first row deserves emphasis. forall a. a -> a has exactly one total inhabitant. Not “usually the identity” — the type makes anything else impossible, because the function has a value of an unknown type and no operations on it, so the only thing it can return is the thing it was given.

Counting inhabitants is a useful habit. forall a. a -> a -> a has exactly two total inhabitants, returning the first or the second argument, which is why it is the boolean type in Church encoding (T041). forall a. [a] -> a has none that are total, since an empty list gives it nothing to return, which is exactly why head is partial and why safe APIs return Maybe a. The type is telling you the function must fail somewhere, before you have looked at it.

Where this becomes free performance. GHC’s most valuable rewrite rules rest on free theorems. foldr/build fusion eliminates intermediate lists:

foldr f z (build g) = g f z

build :: forall b. (forall a. (a -> b -> b) -> b -> b) -> [b] has a rank-2 type, and the inner forall a is what makes the rule sound. Because the producer is parametric in the list representation, it cannot inspect the list it is building, so replacing the constructors with f and z is guaranteed to preserve meaning. The compiler is applying a theorem it derived from a type in order to delete an allocation, and map f (map g xs) fusing to map (f . g) xs is licensed the same way.

Concretely: sum (map (*2) (filter even [1..n])) naively allocates two intermediate lists of size proportional to $n$; at $n = 10^6$ with filter even keeping half, that is 500,000 cons cells for the filtered list and 500,000 more for the mapped one, roughly a million heap allocations that fusion removes entirely, leaving a loop with no allocation at all.

Naturality is the categorical name. A free theorem of this shape is exactly a naturality condition on a natural transformation, and the polymorphic type is the transformation’s signature. This is not a coincidence or an analogy; it is the same statement in two vocabularies, and it is why the Haskell library ecosystem’s laws so often look like commuting squares.

Why the theorem holds: there is nothing to branch on. A parametric function receives a value of an abstract type with no operations attached. It cannot compare it, print it, check its size, or ask what it is. The only things it can do are pass it along, duplicate it, or discard it. Uniformity is not a convention the programmer follows; it is a consequence of having no primitive that could break it.

That is also precisely why the theorem dies the moment such a primitive exists. Java’s instanceof, C#’s reified generics, and Haskell’s Typeable all restore the ability to ask “what type is this really,” and with it, the ability to write a function that behaves differently at String than at Int.

Forbids

A total inhabitant of forall a. a. No value can be produced from nothing.

Anything but id at forall a. a -> a, among total functions.

Type-dependent behaviour in a parametric function. No branching on the instantiation, which is precisely the property that makes the free theorems free.

Fusion in a language with reflection over type parameters. GHC’s rewrite rules would be unsound if a producer could observe the representation it was producing into.

Does not forbid

It does not forbid ad-hoc polymorphism, and conflating the two is the usual confusion. Haskell’s type classes provide type-dependent behaviour legitimately, by passing a dictionary. show :: Show a => a -> String behaves differently at every type, and there is no contradiction: the constraint is a visible extra argument, so the function is parametric in everything it is parametric in and explicit about the rest. Rust traits, Scala implicits, and Swift protocols are the same mechanism.

It does not mean parametricity is a Haskell-only concern. Java’s generics are erased, so List<T> methods are parametric in T and the free theorems apply; this is why Collections.reverse cannot depend on element type. Rust’s generics are monomorphized but still parametric unless a trait bound says otherwise, and the bound is exactly the declaration that you are leaving the parametric world. OCaml’s functors are parametric over module types.

It does not require the language to be pure to be useful. It requires purity to be a theorem. In an impure language it remains a strong heuristic and a correct statement about the subset of functions that do not use the escape hatches, which is most of them.

It does not mean polymorphic code is slow. Rust and C++ monomorphize, so generic code compiles to the same machine code as the hand-specialized version. GHC specializes aggressively too. The uniformity is a source-level property with no necessary runtime cost.

It does not say the free theorem is the only theorem. It is the part you get without reading the code. reverse and tail share a type and share every free theorem, and they are different functions. Parametricity narrows the space; it does not pick a point in it.

Boundary

• Purity and totality. seq breaks parametricity in Haskell, which is why the free theorems come with side conditions about strictness and bottom, and why foldr/build fusion has documented corner cases.
• No type case. Reflection, instanceof, reified generics, and Typeable each void it for the code that uses them.
• Effects. A function that reads a global or performs IO is not determined by its argument, and the relational argument does not apply.
• Impredicativity and dependent types. The relational model becomes substantially harder; step-indexed logical relations were developed to handle recursive types and mutable state, and RustBelt’s proof is built on that machinery.
• The theorem constrains, it does not specify. It is an upper bound on what can vary, not a lower bound on what the function achieves.

The habit to acquire: read a type signature as a specification, and ask what it forbids before asking what it permits. Often the type has already ruled out every implementation but the one you wanted, and the remaining work is smaller than it looked.

Read next