# Natural Transformations and Parametricity

In Theorems for Free!, Wadler says that the characterization of parametricity can be re-expressed in terms of lax natural transformations and this will be the subject of a further paper. Which paper is he referring to?

The categorical approach to paramtericty I know uses dinatural transformations as in Functorial Polymorphism by Bainbridge, Freyd, Scedrov and P.J. Scott. What is the connection between lax natural transformation and dinatural transformation formulations of parametricity?

• I am almost afraid to make this comment, but I will confess that I don't understand any technical word in this question. Might it be possible to add some links to definitions for this (horribly)-non expert ? Mar 13, 2014 at 19:09
• Looks like a job for @UdayReddy. Mar 13, 2014 at 19:38
• As far as I know, the paper referred to in Theorems for Free! was (sadly) never written. I'm pretty sure the current understanding of parametricity in terms of category theory is best captured by Scones and comma categories. See e.g. Mitchell & Scedrov and this n-Category Café post.
– cody
Mar 14, 2014 at 15:59
• Suresh, sorry for not providing the relevant links. Cody, thank you for editing the post and mentioning scones and comma categories. Mar 16, 2014 at 7:48
• Dinatural transformations are, in general, weaker than the relational laws that follow from the parametricity theorem. For a term of type $\forall a.\, F a$ where $F$ is some type constructor, you can write the dinaturality law (or the "wedge law"). That law will always hold due to the parametricity theorem. But when the type is sufficiently complicated and contains nested higher-order functions, e.g., $\forall a.\, (a \to a) \times a \to a$, the dinaturality law is too weak to prove the properties of such types. One needs to use the full power of the relational parametricity law. Jan 5, 2023 at 10:45

• @SonatSüer: The underlying 2-category is Rel. Recall that every poset can be regarded as a (degenerate) category with unique morphisms $x \to y$ whenever $x \leq y$. Similarly, every poset-enriched category can be regarded as a (degenerate) 2-category, with unique 2-cells $f \to g$ whenever $f \leq g$. Since Rel is a poset-enriched category with the inclusion order $R \subseteq S : \textbf{Rel}(A,B)$, it is a 2-category. Mar 17, 2014 at 12:39