12
$\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?

Improve this question
$\endgroup$
5
  • 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, 2014 at 19:09
  • 1
    $\begingroup$ Looks like a job for @UdayReddy. $\endgroup$
    – Dave Clarke
    Mar 13, 2014 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, 2014 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, 2014 at 7:48
  • $\begingroup$ 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. $\endgroup$
    – winitzki
    Jan 5 at 10:45

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
5
  • $\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, 2014 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, 2014 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, 2014 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, 2014 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, 2014 at 15:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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