THE PARAMETRIC POLYMORPHISM one function, every type — and the type tells you what it can't do
A parametrically polymorphic function works for all types uniformly, because it cannot inspect the values it holds — length : [a] → Int counts elements without ever looking at one. Strachey named this (against ad-hoc polymorphism, which behaves differently per type). Reynolds and Wadler found the deep consequence: a polymorphic type is so restrictive that it forces theorems for free — map must preserve length, any a→a that is polymorphic must be the identity. The type alone, before you see the code, tells you what the function must do.
THE TECHNIQUE uniform over all types → the type forces the behavior
A polymorphic map applies a function elementwise without inspecting types. The demo maps and checks the free theorem — length is preserved: live demo
HISTORY & CREDIT Strachey 1967 · Reynolds · Wadler 1989
“A generic function is just one that ignores its type.” — ignoring the type is exactly what makes it powerful: unable to look, it must treat every element the same, and that uniformity is a theorem you get without proof. Restriction buys knowledge. cited
1967 · Christopher Strachey — “Fundamental Concepts”: names parametric vs ad-hoc polymorphism. 1983 · John Reynolds — parametricity / the abstraction theorem: polymorphic functions respect relations. 1989 · Philip Wadler — “Theorems for Free!”: read the theorem straight off the type. now · generics in every typed language.
The less a function may know about its input, the more you may know about the function. A fully polymorphic a → a can only be the identity — the type has one honest inhabitant. Wadler 1989
RECOMMEND FOR I-13 mapped sum + length preserved, computed
On the canonical compiler, mapping double over [1,2,3,4] gives sum 20 and the free theorem holds — length stays 4:
$ i13 run t_parametric.i13 # map double, then check length
mapped_sum = 20
len_preserved = 4 -- map never changes the number of elements (free theorem)
Recommend: i13's functions are parametric in the strongest possible sense — they cannot inspect a type because there is only one type (f64). Its map/sum over an array treat every element identically by necessity, so the free theorems (length preservation) hold trivially. i13 reaches parametricity's uniformity not by a rich polymorphic type system but by having no types to be non-uniform over — the same austerity that put types: NOT COVERED in its ledger.