$\def\infer#1#2{\frac{\matrix{#1}}{#2}}$

Xavier Pinho

Reynolds' relation-preserving operator on functions

$\def\ra{\rightarrow}$ $\def\la{\leftarrow}$ $\def\x{\times}$ $\def\comp{\mathbin{\cdot}}$ $\def\ccomp{\mathbin{\circ}}$ $\def\startCalc{\begin{eqnarray*}&&}$ $\def\endCalc{\end{eqnarray*}}$ $\def\fa{\forall}$ $\def\Int{\texttt{Int}}$ $\def\FF{\mathcal{F}}$ $\def\stepCalc#1#2{\\ & #1 & \{ \mbox{ #2 } \} \nonumber\\ &&}$

The whole idea behind the parametricity result is that parametrically polymorphic functions preserve relations, an insight dating back at least to Reynolds’ abstraction theorem.

Example. Let $h:\alpha\ra\alpha$ be a parametrically polymorphic function. Let $R:A\ra B$ be a relation on two arbitrary types $A$ and $B$. The free theorem of $h$ applied to $R$ then reads $$\langle\fa a:A, b:B :: bRa \implies (h~b)R(h~a)\rangle$$

The key, as Wadler put it, is to read types as relations. Formally, suppose types are given by the following grammar $$t ::= c ~|~ \alpha ~|~ t_1 \ra t_2$$ in which $c$ denotes a concrete type (e.g. $\texttt{Bool}$), $\alpha$ a type variable, and $t_1\ra t_2$ a function from $t_1$ to $t_2$. For a type $t$ with type variables $\alpha_1,\dots,\alpha_n$, and relations $R_i:A_i\ra B_i$ associated with each $\alpha_i$, define the relation $$R_t:t[\alpha_1 := A_1,\dots,\alpha_n := A_n]\ra t[\alpha_1 := B_1,\dots,\alpha_n := B_n]$$ inductively as follows:

$$ \begin{eqnarray*} R_c &=& id\\
R_{\alpha_i} &=& R_i\\
R_{t_1\ra t_2} &=& R_{t_2}\la R_{t_1} \end{eqnarray*} $$

In the last equation, $R_{t_2}\la R_{t_1}$ is the relation on functions, typed $(A\ra B)\ra(A’\ra B’)$ if $R_{t_1}: A\ra A'$ and $R_{t_2}:B\ra B'$, such that $$g(R_{t_2}\la R_{t_1})f \iff \langle\fa a:A,a’:A’ :: a’R_{t_1}a \implies (g~a’)R_{t_2}(f~a)\rangle$$ or, equivalently, $$g\comp R_{t_1}\subseteq R_{t_2}\comp f$$

In other words, $g(R_{t_2}\la R_{t_1})f$ holds if $f$ and $g$ map $R_{t_1}$-related inputs to $R_{t_2}$-related outputs. The parametricity result then reads as follows:

$h R_t h$, for any parametrically polymorphic function $h :t$.

Returning to our initial example, from the type of $h:\alpha\ra \alpha$ we extract that, for any relation $R:A\ra B$, $h_B(R\la R)h_A$, equivalently, $h_B\comp R \subseteq R\comp h_A$, equivalently, $\langle\fa a:A, b:B :: bRa \implies (h~b)R(h~a)\rangle$. One interesting case is when $R$ is actually a function (i.e. an entire and simple relation), say $f:A\ra B$. In such case, the free theorem of $h$ boils down to the natural property of identity, i.e. $$h_B \comp f = f \comp h_A$$ wherefrom we conclude that $h$ corresponds to the identity function, as it was obviously clear from the beginning.

This $\la$ operator, as we can appreciate, is the cornerstone in the construction of $R_t$ in the parametricity result. Backhouse named it the Reynolds’ arrow operator and studied it as a standalone operator for its calculational merits. Let us define it formally and see some examples of where it can be found. We conclude this presentation with a few lemmata that are particularly useful for calculations.

Definition. Let $R:A\ra B$ and $S:C\ra D$ denote two relations. Define the relation $$S\la R: (A\ra C) \ra (B\ra D)$$ on arbitrary functions $f:A\ra C$ and $g:B\ra D$ such that

$$ g(S\la R)f \iff g\comp R \subseteq S\comp f $$

i.e. makes the following diagram semi-commute:

$$ \require{AMScd} \begin{CD} A @>{f}>> C\\
@VRVV\subseteq @VVSV\\
B @>>{g}> D \end{CD} $$

Example. A homomorphism between groups $(G,\dagger)$ and $(H,\ddagger)$ is a function $f:G\ra H$ such that

$$ \langle\forall x,y\in G :: f(x\dagger y) = (f~x)\ddagger(f~y)\rangle $$

Or, in other words, such that $\ddagger(f\la f\times f)\dagger$, cf. the following commutative diagram:

$$ \require{AMScd} \begin{CD} G\times G @>{\dagger}>> G\\
@V{f\times f}VV @VVfV\\
H\times H @>>{\ddagger}> H \end{CD} $$

To wit,

$$ \startCalc \ddagger(f\la f\times f)\dagger \stepCalc{\iff}{$\la$} \ddagger\comp (f\times f)\subseteq f\comp\dagger \stepCalc{\iff}{Equality on functions} \ddagger\comp (f\times f) = f\comp\dagger \stepCalc{\iff}{Introducing variables} \langle\forall x,y\in G::\ddagger\comp(f\times f)(x,y) = f\comp\dagger (x,y)\rangle \stepCalc{\iff}{$\comp$ and $\times$} \langle\forall x,y\in G::(f~x)\ddagger(f~y) = f(x\dagger y)\rangle \endCalc $$

Example. The category Grp of groups and group homomorphisms can then be stated as follows:

Example. The category Rel found in The Joy of Cats (p. 22) is defined by:

Thus, an arrow $f:(X,\rho)\ra(Y,\sigma)$ in Rel is a function $f:X\ra Y$ such that

$$ f(\sigma\la\rho)f $$

i.e. makes the following diagram semi-commute:

$$ \require{AMScd} \begin{CD} X@>{f}>> Y\\
@V{\rho}VV\subseteq @VV\sigma V\qquad f\comp\rho\subseteq\sigma\comp f\\
X@>>{f}> Y \end{CD} $$

To wit,

$$ \startCalc f\comp\rho\subseteq\sigma\comp f \stepCalc{\iff}{Shunting} \rho\subseteq f^\circ\comp\sigma\comp f \stepCalc{\iff}{Introducing variables} \langle\forall x’,x\in X : x'~\rho~x : x’(f^\circ\comp\sigma\comp f)x\rangle \stepCalc{\iff}{$\comp$ and $^\circ$} \langle\forall x’,x\in X : x'~\rho~x : (f~x’)\sigma(f~x)\rangle \endCalc $$

Lemma. Let $R$, $S$, $U$ and $V$ denote relations. Then

  1. $id\la id = id$
  2. $(S\la R)^\circ = S^\circ \la R^\circ$
  3. $(S\la R)\comp(V\la U) \subseteq (S\comp V)\la(R\comp U)$

Lemma. Let $f$, $g$ and $k$ denote functions. Then

  1. $k(f\la g)h \iff k\comp g = f\comp h$
  2. $(f\la g^\circ)h = f\comp h\comp g$

Lemma. The $\la$ operator is order-preserving on the left hand side and order-reversing on the right hand side, i.e. for $R$, $S$, $U$ and $V$ relations, $$\infer{S\subseteq V & R\supseteq U}{(S\la R)\subseteq(V\la U)}$$

References