freetheorem

Free theorems are theorems about polymorphic functions that can be derived from a function’s type signature alone, under the principle of relational parametricity. They describe how such functions must behave uniformly across all instantiations of their type variables, without relying on the concrete values they process. The concept, developed in the study of parametric polymorphism, was popularized by Philip Wadler in Theorems for Free, building on Reynolds’ work on relational parametricity. These theorems let programmers reason about generic functions and libraries without knowing their implementations, expressing laws that must hold for all possible definitions.

A classic example is a function f with the type forall a. a -> a. By parametricity, f cannot inspect the actual value of a, so the only fully general implementation is the identity function: f x = x for all x. Another standard example is a polymorphic function f with the type forall a. [a] -> [a]. For any function g :: a -> b and any list xs :: [a], the free theorem implies that map g (f xs) = f (map g xs); in other words, f must commute with the usual map operation on lists.

Free theorems are used to reason about abstract interfaces, verify simple properties of polymorphic code, and guide library design in pure functional languages such as Haskell. They assume pure, fully parametric polymorphism; in languages with effects, type classes, or runtime type representations, additional considerations or extensions are required.

For further reading, see Reynolds’ relational parametricity and Wadler’s Theorems for Free.