Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Feel the Parametricity

Dan Doel (Apr 04 2020 at 02:29):

Although I guess some people are now pushing for the idea that naturality is a pale immitation of parametricity, and the latter should be more widely applied. :grinning:

Morgan Rogers (he/him) (Apr 04 2020 at 11:29):

What's parametricity, how does it relate to naturality, and what else do I need to know about it?

Dan Doel (Apr 04 2020 at 15:19):

Well, I don't know how historical you want to get. The oldest idea, I think, is that when you give a definition with a type like $a → a → a$, it is parametric if the definition is not necessary to be given by cases on what $a$ actually is. It must be a single, uniform definition that works for all choices of $a$. However, this is a very syntactic description, which is somewhat undesirable, so the challenge was to give a more semantic characterization of what it means.

Dan Doel (Apr 04 2020 at 15:20):

Apparently, this is also the oldest intuitive description of what it means for something to be "natural," but the way it was fleshed out ended up different. Naturality obviously involved categories.

Dan Doel (Apr 04 2020 at 15:36):

Parametricity instead uses relations. For type theory, this traditionally means that you can give types/terms an alternate semantics in relations. So, every type $A$ gives a relation $R_A : A \leftrightarrow A$, and every term $f : A$ is related to itself by $R_A$. For types with quantifiers, like $∀ A. A → A$, the relational interpretation is to quantify over relations between types, like $∀ A B (R : A \leftrightarrow B) (x : A) (y : B). R x y → R (f x) (f y)$.

Dan Doel (Apr 04 2020 at 15:40):

So, if you think of natural transformations as having these sort of quantified types, and the corresponding relations that we quantify over are required to be like 'structure respecting' relations, maybe that explains how this can fill a similar role to naturality.

Dan Doel (Apr 04 2020 at 15:45):

However, the original serious investigations into parametricity were conducted with System F, where the quantifiers range over all types, including ones with quantifiers. This is very powerful, and lets you encode all sorts of structures with very few primitives (just $∀$ and $→$). However, it is a different sort of impredicativity than is used in normal mathematics, and is incompatible with it. For instance, System F can define the booleans $2$, and also define the fixed point of $(- → 2) → 2$. So you can't interpret its types in classical set theory (because $- → 2$ is the power set there, and there is no fixed point of the double power-set).

Dan Doel (Apr 04 2020 at 15:48):

So, parametricity kind of got ignored in normal mathematics, because e.g. the title of the paper presenting the last message was "Polymorphism is not Set Theoretic." That is, "parametric polymorphism." However, I think parametricity is kind of irrelevant, the real problem is the mismatched sorts of impredicativity. But the two got conflated.

Dan Doel (Apr 04 2020 at 15:48):

This is the paper laying this out in more detail, and suggesting how parametricity could apply to wider mathematics: https://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf

Dan Doel (Apr 04 2020 at 16:09):

It's been recognized for a long time that parametric definitions in type theory automatically satisfy naturality conditions of the straight forward category built out of its types and terms, but usually naturality is kind of assumed to be 'better' by people investigating category theory for type theory applications.

Dan Doel (Apr 04 2020 at 16:10):

So, this is the first time I've seen it flipped around, that maybe parametricity is what should have been used more widely, and naturality is a bit weird.

Morgan Rogers (he/him) (Apr 04 2020 at 16:55):

Dan Doel said:

So, if you think of natural transformations as having these sort of quantified types, and the corresponding relations that we quantify over are required to be like 'structure respecting' relations, maybe that explains how this can fill a similar role to naturality.

This makes it sound like parametricity is "naturality where the components are relations instead of just morphisms", in which case I suppose it is more general as soon as you are working in a category with enough structure for relations to behave nicely.

Dan Doel (Apr 04 2020 at 17:08):

Maybe. But things are being restructured more fundamentally than that in the paper, I think.

Dan Doel (Apr 04 2020 at 17:13):

They do eventually construct something that looks a lot like a framed bicategory, or double category or something, where you have morphisms and relations and ways to lift morphisms to relations.

Verity Scheel (Apr 04 2020 at 17:21):

Most treatments of parametricity are type-directed in a sense: given a type of a (polymorphic) function, you can state the theorem it should satisfy to be parametric. Can naturality conditions be expressed in a similar way?

Dan Doel (Apr 04 2020 at 17:27):

The idea, I think, is that instead of objects and morphisms between them, you build objects with relations between them. Then the analogue of functors is required to carry a relational interpretation, and the analogue of naturality is also relation based.

Dan Doel (Apr 04 2020 at 17:29):

One of the stated advantages of this is that the functor analogue does not have an inherent variance, so you don't need to handle that by duplicating variables and worrying about dinaturality and such.

Dan Doel (Apr 04 2020 at 17:29):

Just like polymorphic types don't need their variables to have a particular variance.

Dan Doel (Apr 04 2020 at 17:31):

I'm not sure how much of a concern that really is, because I've seen it suggested that almost every use of dinaturality can instead be turned into extranaturality, which is much less of a problem.

Morgan Rogers (he/him) (Apr 04 2020 at 17:53):

I think I'll come back to this later. However, I would be remiss not to mention Freyd's allegories when discussing relational contexts. They never took off, but as a formal framework for talking about "categories like categories of relations" they're pretty robust. Maybe some computer scientist will get around to checking them out at some point :grinning_face_with_smiling_eyes:

Dan Doel (Apr 04 2020 at 17:58):

Well, one thing I haven't mentioned from the paper yet is that the relations in question do not compose. So it's not the same thing as a category of relations.

Dan Doel (Apr 04 2020 at 17:59):

I think they say the non-compositional nature is essential, too.

Dan Doel (Apr 04 2020 at 18:01):

Or rather, there is no assumption that you can take the composite of two relations, like the composite of morphisms.

Dan Doel (Apr 04 2020 at 18:01):

Only reflexivity.

Dan Doel (Apr 04 2020 at 18:17):

Basically, I think you should not be thinking of the suggestion as considering categories of relations instead of all categories, but as considering all reflexive graphs, instead of just categories.

Gershom (Apr 06 2020 at 08:44):

This paper and the subsequent paper by the same authors seem quite rich in terms of putting everything in a modern setting. I don't claim to really understand what's going on yet though https://arxiv.org/abs/1701.06244

Morgan Rogers (he/him) (Apr 06 2020 at 09:57):

I eventually understood this as the idea that one wants to look at $End(-)$ or $Aut(-)$ as being of a single variable rather than $Hom(-,-)$ which takes two, and I remember reading in a few places about how those things fail to be functorial; parametricity expresses the ways in which such constructions are universally defined. As someone who works with monoids a lot, this will eventually become interesting to me, but I'll leave it on the back burner for now. Thanks for the info!

Dan Doel (Apr 06 2020 at 14:33):

That's at least one aspect, yeah. They say that relations somehow capture abstraction (which is kind of what naturality is about) better than homomorphisms, but I'm not sure what the precise content of that is.

Dan Doel (Apr 06 2020 at 14:35):

There's also stuff in that paper I hadn't seen before, like the idea of having the reflexive relation on a poset be $\leq$, so that the equivalent of functors must preserve that. I'm not sure what consequences that has.