Parametricity

Definition

Parametricity is the principle that a polymorphic term behaves uniformly in its type arguments. Formally, one assigns to every type $A$ a logical relation $A^R$, and proves an abstraction theorem of the form

$$\Gamma ⊢t:A⟹{\Gamma }^R⊢t^R:A^R(t_0,t_1).$$

Thus, related inputs are sent to related outputs.

Example

Parametricity strongly constrains a closed term of type

$$f:{\Pi }_{X:U}X\to X.$$

Since such a term has no type-specific way to manufacture or inspect an element of $X$, it must behave uniformly, and in many theories this forces it to act like the identity.

Variants

Parametricity may be:

• external, as a metatheorem proved about a type theory
• internal, where relations or bridges are primitives of the theory
• unary, using predicates $A\to U$
• binary, relating two interpretations of $A$

History

Reynolds introduced the relational account of polymorphism. Bernardy, Jansson, and Paterson extended the translation to dependent type theory.

Related Concepts

Dependent Type Theory
Logical Relation
Polymorphism
Type Theory