<p>Unfortunately, the remark of Wadler is too cryptic for me to tell what use he wanted to make of "lax natural transformations".  Here is a guess.  Relation-preservation squares can often be recast as lax commutative squares.  This is how they used to be written in old automata theory papers/books.  See paragraph 1.2 in my <a href="http://www.cs.bham.ac.uk/~udr/notes/semigroups.pdf">Notes on Semigroups</a>.  To do this kind of thing, you have to mix up relations and morphisms and pretend that they are the same.  I am also not sure that it buys you anything new.  It is just uglier notation for saying the same thing as relation-preservation.</p>

<p>Please feel free to explore the connection, but I am not confident that you will find anything new by doing it.</p>

CC BY-SA 3.0
2014-03-17T08:35:36.140Z
Thank you very much for the link. The formulation in paragraph 1.2 is still set theoretic to me. How do you talk about inclusion? Do you assume that the category is an allegory or has topos-like properties? If this is a reformualtion of lax natural transformations, what is the underlying 2-category? I also read the part "Categorification" but could not find anything about lax natural transformations.
sonat
CC BY-SA 3.0
2014-03-17T12:39:45.213Z
@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.
Uday Reddy
CC BY-SA 3.0
2014-03-17T12:58:44.583Z
Oh, so the category is fixed! I thought Wadler was referring to a more general and abstract formulation which makes sense in a certain class of categories containing **Rel** as a special (and somewhat trivial) case. If we are working only in **Rel** there is no point in introducing higher yet degenerate structure. Now I understand your original answer.
sonat
CC BY-SA 3.0
2014-03-17T15:07:39.830Z
@SonatSüer: If you are interested in generalizations, the standard way to generalize relations to categories other than **Set** is to treat them as "jointly monic spans".  You might get a preorder-enriched category instead of poset-enriched, but the 2-categorical structure is still the same.
Uday Reddy
CC BY-SA 3.0
2014-03-17T15:14:18.623Z
@SonatSüer: And, if you are really interested in a proper axiomatic theory that covers everything we know, I can refer you to our recent paper [Logical relations and Parametricity - A Reynolds Programme](http://www.cs.bham.ac.uk/~udr/#Recent).
Uday Reddy
CC BY-SA 3.0
2014-03-14T18:08:28.113Z
2014-03-14T18:08:28.113Z
Uday Reddy
<p>In <em><a href="http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf">Theorems for Free!</a></em>, Wadler says that the characterization of parametricity can be re-expressed in terms of <a href="http://ncatlab.org/nlab/show/lax+natural+transformation">lax natural transformations</a> and this will be the subject of a further paper. Which paper is he referring to?</p>

<p>The categorical approach to paramtericty I know uses <a href="http://en.wikipedia.org/wiki/Dinatural_transformation">dinatural transformations</a> as in <em><a href="http://citeseer.uark.edu:8080/citeseerx/showciting;jsessionid=8E22D04EC0AD799DCB3EC193F67AD728?cid=582306">Functorial Polymorphism</a></em> by Bainbridge, Freyd, Scedrov and P.J. Scott. What is the connection between lax natural transformation and dinatural transformation formulations of parametricity?</p>

CC BY-SA 3.0
2014-03-13T19:09:05.437Z
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 ?
Suresh Venkat
CC BY-SA 3.0
2014-03-13T19:38:35.150Z
Looks like a job for @UdayReddy.
Dave Clarke
CC BY-SA 3.0
2014-03-14T15:59:56.603Z
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](http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=971489E1F270E78C434728D8A8D6A06D?doi=10.1.1.26.4213&rep=rep1&type=pdf) and [this](https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html) n-Category Café post.
cody
CC BY-SA 3.0
2014-03-16T07:48:24.347Z
Suresh, sorry for not providing the relevant links. Cody, thank you for editing the post and mentioning scones and comma categories.
sonat
CC BY-SA 4.0
2023-01-05T10:45:18.367Z
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.
winitzki
<reference-request><ct.category-theory><parametricity>
Natural Transformations and Parametricity
sonat
# Natural Transformations and Parametricity

(Asked by: username_0 on 2014-03-13)

In *[Theorems for Free!](http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf)*, Wadler says that the characterization of parametricity can be re-expressed in terms of [lax natural transformations](http://ncatlab.org/nlab/show/lax+natural+transformation) 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](http://en.wikipedia.org/wiki/Dinatural_transformation) as in *[Functorial Polymorphism](http://citeseer.uark.edu:8080/citeseerx/showciting;jsessionid=8E22D04EC0AD799DCB3EC193F67AD728?cid=582306)* by Bainbridge, Freyd, Scedrov and P.J. Scott. What is the connection between lax natural transformation and dinatural transformation formulations of parametricity?

**Tags:** reference-request, ct.category-theory, parametricity

> **Comments:**
> **username_1**: 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 ?  
> **username_2**: Looks like a job for @UdayReddy.  
> **username_3**: 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](http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=971489E1F270E78C434728D8A8D6A06D?doi=10.1.1.26.4213&rep=rep1&type=pdf) and [this](https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html) n-Category Café post.  
> **username_0**: Suresh, sorry for not providing the relevant links. Cody, thank you for editing the post and mentioning scones and comma categories.  
> **username_4**: 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.  

---

## 1 answers

### Answer by username_5 on 2014-03-14. Score: 8 | Accepted answer

Unfortunately, the remark of Wadler is too cryptic for me to tell what use he wanted to make of "lax natural transformations". Here is a guess. Relation-preservation squares can often be recast as lax commutative squares. This is how they used to be written in old automata theory papers/books. See paragraph 1.2 in my [Notes on Semigroups](http://www.cs.bham.ac.uk/~udr/notes/semigroups.pdf). To do this kind of thing, you have to mix up relations and morphisms and pretend that they are the same. I am also not sure that it buys you anything new. It is just uglier notation for saying the same thing as relation-preservation.

Please feel free to explore the connection, but I am not confident that you will find anything new by doing it.

> **Comments:**
> **username_0**: Thank you very much for the link. The formulation in paragraph 1.2 is still set theoretic to me. How do you talk about inclusion? Do you assume that the category is an allegory or has topos-like properties? If this is a reformualtion of lax natural transformations, what is the underlying 2-category? I also read the part "Categorification" but could not find anything about lax natural transformations.  
> **username_5**: @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.  
> **username_0**: Oh, so the category is fixed! I thought Wadler was referring to a more general and abstract formulation which makes sense in a certain class of categories containing **Rel** as a special (and somewhat trivial) case. If we are working only in **Rel** there is no point in introducing higher yet degenerate structure. Now I understand your original answer.  
> **username_5**: @SonatSüer: If you are interested in generalizations, the standard way to generalize relations to categories other than **Set** is to treat them as "jointly monic spans".  You might get a preorder-enriched category instead of poset-enriched, but the 2-categorical structure is still the same.  
> **username_5**: @SonatSüer: And, if you are really interested in a proper axiomatic theory that covers everything we know, I can refer you to our recent paper [Logical relations and Parametricity - A Reynolds Programme](http://www.cs.bham.ac.uk/~udr/#Recent).  

---

