Parametricity

Remarks

Example: let $p$ be a parametric value of type $\forall \alpha.\, \alpha \to \alpha$, let $A$ be a set and $a \in A$. Take $B = A$ and the relation $R = \set{(a, a)}$. Clause 3 gives that $p_A(a)$ and $p_A(a)$ are related by $R$, so $p_A(a) = a$, and $p_A$ is the identity on $A$.

Non-example: let $q_A$ be the swap of $\mathsf{true}$ and $\mathsf{false}$ when $A$ is the set of booleans, and the identity on every other set $A$. This is a family of maps $A \to A$, but it is not parametric. With $A = \set{0, 1}$, $B$ the booleans and $R = \set{(0, \mathsf{false}), (1, \mathsf{true})}$, clause 3 fails: $0$ and $\mathsf{false}$ are related, but $q_A(0) = 0$ and $q_B(\mathsf{false}) = \mathsf{true}$ are not. Such a family cannot be written as a term of System F, since a term cannot test which type it is applied to.

For a function $h \colon A \to B$, taking $R$ to be the graph of $h$ turns the relational statement into an equation, which is how the free theorems are read off. For all of System F, with nested quantifiers and several type variables, the relational interpretation has one more clause. Values of $\forall \beta.\, \tau_1$ are related if, for all $A$, $B$ and $S \subseteq A \times B$, their instances at $A$ and $B$ are related by the interpretation of $\tau_1$ at $S$. Reynolds showed that System F has no model in which types are plain sets and $\forall$ ranges over all sets. So this general form is used in other models, such as models built from partial equivalence relations, or in a syntactic form. Reynolds' abstraction theorem says that every closed term of System F is parametric in this sense.