11
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ 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 ? $\endgroup$ – Suresh Venkat Mar 13 '14 at 19:09
  • 1
    $\begingroup$ Looks like a job for @UdayReddy. $\endgroup$ – Dave Clarke Mar 13 '14 at 19:38
  • 5
    $\begingroup$ 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. $\endgroup$ – cody Mar 14 '14 at 15:59
  • $\begingroup$ Suresh, sorry for not providing the relevant links. Cody, thank you for editing the post and mentioning scones and comma categories. $\endgroup$ – sonat Mar 16 '14 at 7:48
8
$\begingroup$

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. 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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – sonat Mar 17 '14 at 8:35
  • $\begingroup$ @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. $\endgroup$ – Uday Reddy Mar 17 '14 at 12:39
  • $\begingroup$ 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. $\endgroup$ – sonat Mar 17 '14 at 12:58
  • $\begingroup$ @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. $\endgroup$ – Uday Reddy Mar 17 '14 at 15:07
  • $\begingroup$ @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. $\endgroup$ – Uday Reddy Mar 17 '14 at 15:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.