Abstract
It is expected that an abstract type can be realized by different concrete types without the users of the abstract type observing any differences. This is the principle of representation independence enunciated by Reynolds in 1983. Symmetrically, a polymorphic function is expected to execute the same algorithm when applied to data of different types.
Parametricity theory gives mathematically precise meaning to these intuitions. It is based on the notion of logical relations: relations between terms, indexed by types, and compatible with the structure of types. In particular, two functions are related to type τ → σ if and only if they send arguments related to type τ on results related to type σ. These logical relations were introduced by Plotkin for the study of the simply typed lambda-calculus. Reynolds extended logical relations to the case of abstract types, enabling him to formalize and demonstrate the principle of independence from representations. The extension to the polymorphic lambda calculus is trickier, as it is easy to fall into circular definitions, but is finally solved around 1990 by Bruce, Meyer and Mitchell, inspired by Girard's reducibility candidate technique.
A spectacular application of parametricity is Theorems for free, the title of a famous paper by Wadler (1991). All functions in the system F with a certain polymorphic type verify equations that depend only on the type ; there's no need to re-demonstrate these equations for every function. Thus, any function f : ∀α. α → α verifies f x = x and is therefore the identity. Parametricity also makes it possible to demonstrate the isomorphism between an inductive type and its functional encoding mentioned in the3rd lecture.
Recent work by Bernardy and Lasson shows that parametricity not only extends to type theory, but can also be internalized within it. A type A translates mechanically into a relation RA which is the logical relation to the type A ; a closed term a : A translates into a proof that a is related to itself by RA. The approach naturally extends to type constructors and dependent types.
