# Why Reflexive Graphs for Parametricity?

Looking at models of parametric polymorphism, I am curious why are reflexive graph categories are used?

In particular, why do they not include relational composition? In looking at the models, they all seem to support a natural notion of relational composition:

$$x(R;S)z \iff \exists y. xRy \wedge y S z$$

Most recent papers that use reflexive graphs seem to take this for granted, and the only older paper I could find that discussed it was "Relational Parametricity and Local Variables" by O'Hearn and Tennent who say:

One reason for not requiring composability is that, as is well known, composition is not preserved by logical relations at higher types.

And I'm not quite sure what this means, so my first question is what is meant by this and hopefully a better reference on this question.

What I think this means is that for instance the exponential doesn't necessarily preserve relational composition on the nose. In particular we can't show $(R;R') \to (S;S') \equiv ((R \to S);(R' \to S'))$. This means that the exponential doesn't extend to a functor on a category of relations.

However, while I can't show the equivalence between the above relations, I can certainly prove an inclusion $((R \to S);(R' \to S')) \subset ((R;R') \to (S;S'))$, right?

Given $f((R \to S);(R' \to S')) h$, then there exists a $g$ of appropriate type with $f(R\to S)g(R'\to S')h$, so given an $xRyR'z$, I can show $f(x) S g(y) S' h(z)$. Doesn't this means that the exponential does give me a lax functor, which seems like a bad property to throw away? So my second question is are there examples where the inclusion in this direction is not provable, either?

• Relational composition does not seem to be useful for proving the parametricity theorem or for reasoning about parametricity properties. This is precisely because the relational composition is not compatible with the exponential. You are right about the inclusion property but it is not enough. The proof of the parametricity theorem requires handling the exponential types as one of the inductive cases. Commented Jan 6, 2023 at 10:21

Often, the type of relations considered do not compose. For instance, if your notion of a relation $R : D \to E$ between $\omega$CPOs is an $\omega$-chain complete subset of $|D|\times |E|$, then the relation $R : \omega + 1 \to \mathbb{N}$ between the ordered naturals plus infinity $\omega+1$ and the flat CPO of naturals $\mathbb{N}$ given by $R(n,n)$ holds and nothing else, then $R$ is admissible, as is its converse, but the composite $R;R^T : \omega+1 \to \omega + 1$ is not chain-complete, since $n R;R^T n$ for every natural, but we don't have $\omega R; R^T \omega$.