Parametric Polymorphism and the Theorems You Get Free
A genuinely parametric `identity<T>(x: T): T` can only return its argument. That is not a convention or a code review rule — it is a theorem about the type, provable because the function is forbidden from knowing anything about T.
What does <T> actually guarantee, beyond saving me from writing the function twice?
A *type scheme* rather than a type: ∀T. (T) → T. The quantifier is the content. It says the body must type-check for every instantiation of T using only operations available on *all* of them — which, with no constraints, is none. The question this form answers: what can this code possibly do, given that it is not permitted to know what it is holding?
A parametric function may not inspect T. Any operation used on a value of type T must be licensed by an explicit constraint — a bound, a trait, a type class, an interface — and the moment such a constraint appears, the function has left parametricity and entered [[ad-hoc-polymorphism]]. Where the language provides a runtime escape (instanceof, typeid, isinstance, reflect.TypeOf, C# typeof(T), C++ if constexpr), the theorems below do not hold and the generic is a code template rather than an abstraction.
Key points
∀T. T → Thas exactly one total implementation, and that is a theorem derived from the type, not a convention.- Parametricity works because the function is *forbidden* from knowing what T is, so it must behave identically for every T.
- A type variable narrows the space of implementations; a concrete type does not.
int → inttells you nothing. ∀T. List<T> → Thas zero total implementations, which is the type-level argument for option types.- Adding a constraint buys operations and spends the theorem. Constrained generics are useful and no longer parametric.
- C# and C++ generics are not parametric:
typeof(T)andif constexprinspect the type. Java, Haskell and Rust are, by default. - The three implementation strategies — erasure, monomorphization, dictionary passing — are cheaper the more parametric the function is.
The theorem is in the signature
any and by the ability to inspect values at runtime with typeof, so treat the signatures above as illustrating the principle rather than as guarantees TypeScript enforces.Write function identity<T>(x: T): T. How many total functions have that type? Exactly one. It must return something of type T; the only value of type T it has is x; it cannot construct one because it does not know what T is; so it returns x. There is nowhere else for the value to come from.
This is not an argument about what a reasonable programmer would write. It is Reynolds’ abstraction theorem, popularised by Wadler in 1989 as “theorems for free”: from a parametric type alone, without seeing the implementation, you can derive properties that every implementation must satisfy. The reason it works is that the function is *prevented* from branching on the type, so it must behave identically for all of them.
The consequences scale up. ∀T. (List<T>) → List<T> cannot invent an element, cannot inspect one, and cannot compare two — so any function of that type produces its result by selecting, duplicating and reordering the elements it was given. That constrains it enormously without constraining it to one implementation. ∀T. (List<T>) → int cannot depend on the elements at all, only on the length. And map obeys length(map(f, xs)) = length(xs) as a theorem, not as a property test that happened to pass.
1// Exactly one total implementation. It returns x.2function identity<T>(x: T): T3 4// Exactly one. It cannot construct a B, so it must call f on a.5function apply<A, B>(f: (a: A) => B, a: A): B6 7// Exactly one. It has no B, so it must return a.8function first<A, B>(a: A, b: B): A9 10// ZERO total implementations. An empty list has no element11// to return, and T cannot be constructed. This is why every12// safe language types head as List<T> => Option<T>.13function head<T>(xs: T[]): T14 15// Many implementations, but every one of them builds its16// result only by applying f to elements of xs. It cannot17// invent a B and it cannot look inside an A.18function map<A, B>(f: (a: A) => B, xs: A[]): B[]The head case is the one with practical consequences. Its emptiness as a type is the argument for [[nullability]] and for option types: the signature T[] => T is a lie in every language that offers it, and the lie is discharged at runtime by an exception, a null, or undefined behaviour depending on the language.
How much a signature narrows the space
The useful habit is to read a generic signature as a *constraint on implementations* before reading the body. The table below counts total inhabitants — implementations that always return — for a series of signatures, and the pattern is worth internalising: adding a type variable usually removes implementations rather than adding them.
| Signature | Total inhabitants | What that tells you |
|---|---|---|
∀T. T → T | 1 | Identity. Nothing else is constructible. |
∀T. T → T → T | 2 | Return the first or the second. There is no third option and no way to combine them. |
∀A B. (A, B) → A | 1 | fst. The B is unreachable as a result. |
∀T. List<T> → T | 0 | The empty list defeats every implementation. This is why head must return an option or be partial. |
∀T. List<T> → int | Many, all element-independent | The result may depend on the length and on nothing else — not on any element’s value. |
∀T. List<T> → List<T> | Many, all element-preserving | Reverse, tail, duplicate, drop, permute. Every element in the output came from the input; none were made. |
∀A B. (A → B, List<A>) → List<B> | Many, all built by applying f | Every B in the result is f of some A from the input. map, but also reverse ∘ map, filter-then-map, and so on. |
int → int | Infinitely many | A concrete type constrains nothing. This is the contrast that makes the point: the *variable* is what carries the information. |
∀T: Comparable. List<T> → List<T>typical | Many more than the unconstrained version | The constraint bought comparison and cost the theorem. Sorting became expressible and “elements are untouched” stopped being provable from the type. |
Where the guarantee leaks
Parametricity holds only if the language actually prevents inspection. Several popular languages do not, and it is worth knowing which, because the difference decides whether a generic signature is a promise or a suggestion.
Java erases type parameters, so a generic method genuinely cannot inspect T — there is nothing left to inspect. Parametricity largely survives, and the leaks are through raw types and unchecked casts, which the compiler warns about as “heap pollution”. C# reifies generics: typeof(T) works, and if (typeof(T) == typeof(int)) is a legal, common idiom. C# generics are therefore not parametric, and a C# generic method may behave differently per instantiation.
C++ templates are not parametric at all and were never meant to be. A template is a code generator: if constexpr (std::is_same_v<T, int>) selects different code per instantiation at compile time, and specialization replaces the body entirely. The parametric-looking syntax is the trap — template <typename T> T identity(T x) may be specialized for int to return 42, and nothing about the signature forbids it. Rust sits closer to Java: a generic function cannot inspect T without a bound, and TypeId/Any require an explicit 'static bound and a downcast, making the escape visible in the signature.
Go generics forbid reflection over the type parameter directly, but a value can be converted to any and reflected upon, which is an escape one line away. TypeScript erases at emit, so a generic cannot inspect T at runtime — but it can inspect the *value*, and typeof x === "string" inside a generic is legal and common, which achieves the same non-parametric effect through a different door.
| Language | Can the body inspect T? | Mechanism | Consequence |
|---|---|---|---|
| Javaspec | No — erased | [[type-erasure]]; new T[] is not expressible | Parametricity mostly holds; leaks via raw types and unchecked casts |
| Haskellspec | No, without a constraint | Constraints are visible in the type: Show a => a -> String | The strongest parametricity guarantee in common use; free theorems are usable |
| Rustspec | No, without a bound | Traits are bounds; Any requires 'static plus an explicit downcast | Parametric by default, with a visible opt-out in the signature |
| C#spec | Yes | Reified generics: typeof(T), is, default(T) | Not parametric. A generic method may branch per instantiation. |
| C++ templatesspec | Yes | if constexpr, traits, explicit and partial specialization | Not parametric at all — a template is a code generator with generic-looking syntax |
| Goimplementation | Not directly; one conversion away | Convert to any, then reflect | Parametric in practice unless someone reaches for reflection |
| TypeScriptimplementation | Not T, but yes the value | typeof x === "string" narrows inside a generic body | Non-parametric behaviour is reachable without any type-level escape |
What it costs at the implementation boundary
Parametricity is a frontend property with a back-end bill, and the bill has three well-known shapes covered in detail elsewhere in this domain.
Erasure compiles one body and represents every T uniformly — a pointer, usually. One copy of the code, no code-size cost, and everything must be boxed, so List<int> in Java holds Integer objects rather than machine integers. See [[type-erasure]].
Monomorphization compiles a separate specialized body per instantiation. Machine-integer representations, direct calls, full inlining, and code size proportional to the number of distinct instantiations — which is why a Rust or C++ binary using generics heavily is large and slow to build. See [[monomorphization]].
Dictionary passing compiles one body and passes a hidden record of the operations the constraints demanded. One copy, one indirect call per constrained operation, and specialization available as an opt-in optimization. This is Haskell’s default and one of the two strategies Rust uses (dyn Trait versus impl Trait).
The design point worth noticing: the *more* parametric the function, the cheaper every strategy becomes. A function that knows nothing about T needs no dictionary at all, and a function that must inspect T cannot be erased. Parametricity is not only a reasoning tool; it is what makes uniform representation possible in the first place.
fn max_i32(a: i32, b: i32) -> i32 { if a > b { a } else { b } }
fn max_f64(a: f64, b: f64) -> f64 { if a > b { a } else { b } }fn max<T: PartialOrd>(a: T, b: T) -> T { if a > b { a } else { b } }Only if the two bodies are identical modulo the type, every operation they perform is licensed by the stated bound, and no caller depended on an overload-resolution behaviour the generic does not reproduce. Here > comes from PartialOrd, both bodies are the same, and monomorphization regenerates exactly the two original functions — so the machine code is unchanged.
When the bodies differ in a way the bound cannot express. If max_f64 needed NaN-aware behaviour that max_i32 did not, PartialOrd does not distinguish them and the generic silently gives the integer semantics to floats. The same failure appears whenever the “identical” bodies differ in overflow handling, in a precision-sensitive comparison, or in which of two equal values is returned — details a bound is usually too coarse to capture.
How it works
The steps, in the order the compiler takes them.
- The checker generalizes the function’s type over its type parameters, producing a scheme
∀T. …— the same generalization step as in[[hindley-milner]], made explicit by syntax. - Inside the body, T is treated as an opaque, unknown type: no operations are available on it except those the declared bounds provide.
- At each call site the scheme is instantiated: T is replaced by a concrete type, either written explicitly or inferred by
[[unification]]from the argument types. - The checker verifies that the instantiating type satisfies every declared bound, and reports a bound violation if not.
- The back end then chooses a representation strategy: erase to a uniform representation, generate a specialized copy per instantiation, or pass a dictionary of the bound’s operations.
- Any language feature that lets the body observe T — reflection, reification, compile-time type predicates — bypasses this and turns the generic into a per-type code selector.
How it breaks
What the engineer observes when it goes wrong — not what goes wrong internally.
- A generic is written parametrically, someone adds a
typeof Tbranch to handle one case, and every downstream reasoning about that function silently becomes invalid — including the compiler’s freedom to erase it. - A
T[] => Thelper is written for “the first element”, an empty array reaches it in production, and the result isundefinedflowing three layers down before anything notices. - In C++, a template is specialized for one type in one translation unit and not in another; the program has two different meanings for the same call and the linker picks one — an ODR violation with no diagnostic required.
- A Java generic method casts internally to make something work, the unchecked-cast warning is suppressed, and a
ClassCastExceptionappears at a call site that contains no cast at all. - Monomorphization on a heavily generic codebase produces a binary that is several times larger than expected and a build that takes minutes; the observable symptom is compile time, not runtime.
- A generic is given a constraint to make one call site work, and every other call site now needs a type that satisfies it — the constraint propagated up through the API and became a breaking change.
When it helps
- Reviewing an unfamiliar API: reading the generic signature tells you what the function cannot do before you read a line of its body.
- Designing library interfaces, where keeping a function parametric keeps its guarantee and keeps every implementation strategy available.
- Deciding whether a helper needs a constraint. If it does not, leaving it unconstrained is free strength; adding one “just in case” spends a theorem for nothing.
- Explaining why an option type is not ceremony:
List<T> => Tis uninhabited, so the language is not being awkward, it is being honest.
When it hurts
- When the language is not actually parametric. Reasoning about C# or C++ generics with free theorems produces confident, wrong conclusions.
- When a function genuinely needs per-type behaviour. Forcing it to be parametric produces a constraint hierarchy that is worse than an honest overload — see
[[ad-hoc-polymorphism]]. - On performance-critical numeric code under erasure, where uniform representation means boxing and the abstraction has a measurable per-element cost.
- When generic parameters multiply. A signature with five type variables and four bounds has stopped communicating anything and is a design smell rather than a strong theorem.
What it costs
Every one of these is paid by something.
- Parametricity buys reasoning — free theorems, safe refactoring, uniform representation — and pays in expressiveness: the function cannot do anything type-specific, so anything type-specific must move into an explicit constraint that then propagates to every caller.
- Erasure buys one compiled body, small binaries and fast builds, and pays in boxing, in the impossibility of
new T[], and in reflection that cannot see the type argument. - Monomorphization buys unboxed representations and direct, inlinable calls, and pays in code size proportional to instantiations, in compile time, and in instruction-cache pressure that can make the “faster” version slower on a large working set.
- Reified generics buy runtime type inspection and better reflection, and pay by giving up parametricity entirely — the signature stops being a promise and every call site must consider that the body may branch on its type argument.
What else you could do
What a different compiler or language does instead, and when that is better.
- Ad-hoc polymorphism: one name, several bodies, chosen by operand type. Necessary whenever the behaviour genuinely differs per type — see
[[ad-hoc-polymorphism]]. - Subtype polymorphism: one body operating on a supertype, with dynamic dispatch selecting behaviour. Different tradeoff — runtime dispatch, no code duplication, and no parametricity guarantee — see
[[subtyping]]. - Dynamic typing, where a function is implicitly polymorphic in everything and there is no theorem to be had. Maximum flexibility, and the guarantee is replaced by tests.
- Code generation or macros, which is what C++ templates and Rust macros actually are for the non-parametric cases: generate a specialized body per type explicitly, and stop pretending the signature is an abstraction.
- Higher-kinded and higher-rank abstraction, where the parameter is a type constructor rather than a type. More expressive, requires annotations (
[[hindley-milner]]cannot infer it), and available in Haskell and Scala rather than in mainstream imperative languages.
See it for yourself
The flag, dump or tool that shows you this directly.
- Java:
javap -son a generic class shows the erased descriptors;javap -vshows theSignatureattribute where the generic information was retained for reflection but not for dispatch. - Rust:
cargo llvm-linesandcargo bloatreport which generic functions produced the most instantiated code — the monomorphization bill, itemised. - C++: Compiler Explorer with a template and one explicit specialization side by side shows that the “generic” function can have a completely unrelated body per type.
- C#:
typeof(T).Nameinside a generic method, printed at runtime, demonstrates in one line that C# generics are not parametric. - TypeScript:
tsc --declarationshows the generic signature that is published; the emitted JavaScript shows that nothing about T survives. - To test parametricity empirically: write the signature, ask a colleague to implement it without seeing your version, and compare. For
∀T. T → Tthe exercise is over immediately, which is the point.
Plausible wrong readings
Stated the way a confident engineer states them.
- “Generics are about avoiding code duplication.” That is the motivation. The guarantee is that a parametric function cannot depend on the type, and that guarantee is what erasure, refactoring safety and free theorems all rest on.
- “
identityreturns its argument by convention.” In a parametric language it is the only thing it can do. There is no other value of type T in scope. - “C++ templates are C++’s generics.” They are a code generation facility with similar syntax. Specialization and
if constexprmean a template’s signature constrains nothing about its body. - “Type erasure means generics are fake.” Erasure is what makes the guarantee enforceable at zero runtime cost. Reified generics are the ones that trade the guarantee away.
- “Adding a constraint makes the generic stronger.” It makes it more capable and strictly weaker as a theorem, and it pushes a requirement onto every caller.
Misconceptions
The claim, and what is actually true.
T[] => T is a perfectly good signature for head.Go deeper
The same idea at increasing depth. Stop wherever it stops being useful.
overview
Generics let one function work for many types. The less obvious part is what that *proves*. A function typed <T>(x: T) => T cannot make a T, cannot look inside a T, and cannot tell one T from another — so the only thing it can return is the T it was handed. You can read guarantees like this straight off a signature: a function returning a number from a list of unknowns can only be looking at the length; a function returning a list of the same unknowns can only be rearranging the ones it got. This works only in languages that genuinely stop the body from inspecting the type, which Java, Haskell and Rust do and C# and C++ do not.
practical
Two habits. First, read generic signatures as constraints before reading bodies — it tells you what a function cannot be doing, which is often more useful than knowing what it does. Second, be reluctant to add constraints. Every bound you attach to a type parameter buys the body an operation and charges every caller a requirement, and it also spends whatever reasoning the unconstrained version gave you. When you find yourself adding a bound to make one call site work, check whether the operation belongs in the caller instead. And if the language you are in reifies generics, remember that none of the reasoning above applies: a C# or C++ generic may do something completely different for one instantiation, and only reading the body will tell you.
advanced
Parametricity is not merely a reasoning aid; it is what licenses uniform representation. If a function cannot observe T, then every T can be represented identically — a pointer, a word — and one compiled body suffices. That is exactly why Java could erase and why Haskell can pass a dictionary and still compile one copy. Reification breaks this: if a body can ask what T is, the code must be able to answer, so either every instantiation gets its own copy or the runtime carries the type argument alongside the value. C# chose the latter and pays for it in the runtime’s complexity; C++ chose the former and pays in code size. The connection runs the other way too: [[monomorphization]] recovers unboxed representations precisely by giving up on having one body, and [[type-erasure]] recovers one body precisely by giving up on knowing the type. Parametricity is the property that lets a language have both at once — one body *and* the guarantee — at the cost of boxing. There is no arrangement in which all three are free, and every language’s generics story is a choice of which one to pay.
How much this depends on
Nothing in this domain is true of every compiler. These say how much.
seq, bottom and unsafeCoerce) and largely to Java generics because erasure removes the ability to inspect. They do not apply to C# or C++, whose generics can inspect the type argument, and they hold only for terminating, exception-free implementations.new T[] is not expressible, and instanceof List<String> is a compile error. C# specifies reified generics, where typeof(T), default(T) and runtime type tests on T all work. These are language-level guarantees on both sides, and code written assuming one will misbehave under the other.if constexpr selects code per instantiation at compile time. Nothing in a template’s declaration constrains its instantiations’ behaviour, which is why C++ concepts were added — to state requirements in the signature — and why concepts still do not make templates parametric.dyn Trait; Haskell passes dictionaries by default and specializes when told to with SPECIALIZE or -fspecialise-aggressively. Which strategy applies to a given call is an implementation decision that changes binary size and speed materially, and it is visible in the emitted code rather than in the source.If you were asked this in an interview
- How many total functions have the type
<T>(x: T) => T? Prove your answer. - What can a function of type
<T>(xs: T[]) => numberpossibly depend on? - Are C# generics parametric? What about Java’s? Explain the difference and what it costs each language.
- Why does
<T>(xs: T[]) => Thave no total implementation, and what should the signature be instead?
Connections
- Software Design — Designing for reuse: when a generic abstraction is worth its costWhether a function should be generic at all is a design judgment about coupling and anticipated variation. This lesson answers what genericity *proves*, not whether you should reach for it.
- Programming Languages & Runtime Internals — Boxing, uniform representation and the runtime cost of erased genericsErasure’s bill is paid in the object representation — an
Integerwhere anintwould have fitted in a register. What that costs in allocation and cache behaviour is the runtime’s subject.