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: learning: questions

Topic: Parametricity implies Naturality?

Ruby Khondaker (she/her) (Aug 26 2025 at 12:03):

I've recently come across the famous Theorems for Free paper, which outlines some conditions under which parametric polymorphism automatically guarantees a naturality condition. But I've also had a cursory look at #learning: questions > Continuations, parametricity, and polymorphism, and it seems that in some cases parametricity does not imply naturality? So I wanted to clarify - to what extent does parametricity imply naturality "for free"?

John Baez (Aug 26 2025 at 12:37):

I think there was a huge conversation about this here.

John Baez (Aug 26 2025 at 12:38):

Yes, for example here:

#learning: questions > Continuations, parametricity, and polymorphism @ 💬

though it started earlier.

Ruby Khondaker (she/her) (Aug 26 2025 at 12:46):

I see - so if I'm understanding correctly, the additional condition one needs is this "bridge-discreteness" or "identity extension lemma"? So if you're in a situation where your types are bridge-discrete, then parametricity genuinely will imply naturality!

And as far as I can tell, the identity extension lemma is a technical condition that is more relevant for things like "spatial" type theories - but if your types really do behave just like sets, then you'd expect it to hold?

Ruby Khondaker (she/her) (Aug 26 2025 at 12:57):

This was also partially inspired by one of Riehl's talks, Infinity-category theory for undergraduates, particularly the following slide:

image.png

During the talk, she made a remark about how she used the word "function" instead of "functor" because, as it turns out, any function between pre-infinity categories (as defined in the talk) is automatically a functor. The slide itself also remarks about how the naturality condition is dropped because it is automatically true.

So I was wondering whether the origin of this was a similar "theorems for free" result? That functions between infinity-categories in this type theory must necessarily be parametric, which implies you get things like functoriality or naturality for free.

Nathanael Arkor (Aug 26 2025 at 13:34):

Surely the reason you don't need to state naturality explicitly here is because it is implicit in the definition of the product type $\prod$ (which is not simply an indexed product of sets)? In which case, it's not that the naturality condition is "dropped" (which makes the wording in the slides feel misleading). Perhaps I'm misunderstanding something.

Patrick Nicodemus (Aug 26 2025 at 14:14):

Ruby Khondaker (she/her) said:

I see - so if I'm understanding correctly, the additional condition one needs is this "bridge-discreteness" or "identity extension lemma"? So if you're in a situation where your types are bridge-discrete, then parametricity genuinely will imply naturality!

And as far as I can tell, the identity extension lemma is a technical condition that is more relevant for things like "spatial" type theories - but if your types really do behave just like sets, then you'd expect it to hold?

Some of the discussion in that thread is a little sophisticated for me to follow, I don't really know what bridge-discreteness is, but I feel confident saying that if $F,G$ are parametrically definable functors $\mathbf{Set}^n\to\mathbf{Set}$ then any polymorphic function $\tau : \forall \alpha :F\alpha\to G\alpha$ is natural with respect to, for example, a set theoretic semantics, or with respect to System R1 that is mentioned in the last comment on the linked thread.

The identity extension lemma is indeed a technical condition and I don't personally have good intuition for it off the top of my head but it already appears in treatments of parametericity that have nothing to do with spatial interpretations.

Josselin Poiret (Aug 26 2025 at 14:23):

Patrick Nicodemus said:

are parametrically definable functors $\mathbf{Set}^n\to\mathbf{Set}$

what does this mean?

Ryan Wisnesky (Aug 26 2025 at 15:33):

I believe (and I could be wrong) that that thread came up with a counter-example to the claim that for any definable functors F and G all polymorphic functions forall x, F x -> G x are natural, because if you let F be the reader functor and G be the identity functor you end up needing the identity extension lemma to complete the proof of naturality (this was worked out in Coq and Narya). For sure R2 (not sure about R1) would entail this. FWIW, subsequent discussion on the types list seemed to indicate that the initial model of system F does not satisfy identity extension. (I'm also hesitant to talk about set theoretic models of F at all, since no such model can be full and classical at the same time.)

Mike Shulman (Aug 26 2025 at 16:19):

One possible meaning of "parametrically definable functor $\mathbf{Set}^n\to\mathbf{Set}$" is something arising from the set-theoretic semantics of an endofunctor of the smallest universe that's definable in predicative dependent type theory, and similarly for a "polymorphic function $\tau : \forall \alpha :F\alpha\to G\alpha$". In that case one would hope to be invoking external parametricity for DTT, but in that case the proof of naturality depends on the IEL for $F$ and $G$. I can't keep straight all the things we decided are true and aren't; do we know that IEL holds for such functors?

Mike Shulman (Aug 26 2025 at 16:23):

Ruby Khondaker (she/her) said:

So I was wondering whether the origin of this was a similar "theorems for free" result? That functions between infinity-categories in this type theory must necessarily be parametric, which implies you get things like functoriality or naturality for free.

It's not unrelated, but not exactly the same. Simplicial type theory could be said to include a sort of "internal parametricity" in the sense that every type comes with a binary relation and every function preserves those relations. However, unlike in the traditional proofs of naturality from parametricity, here we are talking about synthetic $\infty$-categories, and the relation associated to such a thing is its homs, rather than having to choose a specific relation in order to make the proof go through. So I'm hesitant to characterize it as a "theorems for free" result -- it's more like a "theorem by definition".

Mike Shulman (Aug 26 2025 at 16:28):

Nathanael Arkor said:

Surely the reason you don't need to state naturality explicitly here is because it is implicit in the definition of the product type $\prod$ (which is not simply an indexed product of sets)? In which case, it's not that the naturality condition is "dropped" (which makes the wording in the slides feel misleading). Perhaps I'm misunderstanding something.

Inside of the type theory, the rules satisfies by $\prod$ are exactly the same as those in any other dependent type theory, i.e. those of an indexed product of "sets" (i.e. types). So naturality is not "built into" it in that sense. One could argue that naturality is implicit in the construction of $\prod$-types in the standard semantics in bisimplicial sets, but that doesn't explain why naturality is automatic inside the theory.

Inside of the theory, the naturality condition is "dropped" in exactly the sense that Emily wrote:

the "naturality" condition is dropped because it is automatically true [emphasis added]

Namely, the definition of "adjunction" internal to simplicial type theory looks like the usual one, except that the word "natural" is omitted because in this context it can be proven.

Ruby Khondaker (she/her) (Aug 26 2025 at 16:52):

Mike Shulman said:

Ruby Khondaker (she/her) said:

So I was wondering whether the origin of this was a similar "theorems for free" result? That functions between infinity-categories in this type theory must necessarily be parametric, which implies you get things like functoriality or naturality for free.

It's not unrelated, but not exactly the same. Simplicial type theory could be said to include a sort of "internal parametricity" in the sense that every type comes with a binary relation and every function preserves those relations. However, unlike in the traditional proofs of naturality from parametricity, here we are talking about synthetic $\infty$-categories, and the relation associated to such a thing is its homs, rather than having to choose a specific relation in order to make the proof go through. So I'm hesitant to characterize it as a "theorems for free" result -- it's more like a "theorem by definition".

Interesting, thank you for the clarification! I might think of it intuitively as a "internal parametricity => naturality" result, in a way that the type theory forces you to talk about internal parametricity, so you have to have various maps being natural.

Patrick Nicodemus (Aug 26 2025 at 17:52):

Josselin Poiret said:

what does this mean?

I mean that if $\tau : \forall \alpha_1,\dots, \alpha_n. F(\alpha_1,\dots,\alpha_n)\to G(\alpha_1,\dots,\alpha_n)$ where $F$ is equipped with $fmap : \forall \vec{\alpha},\vec{\alpha}',\vec{\alpha}\to\vec{\alpha'}\to F(\vec{\alpha})\to F(\vec{\alpha}')$ and the set theoretic semantics of $F$ and $fmap$ define a functor, similarly with $G$

Patrick Nicodemus (Aug 26 2025 at 17:53):

Mike Shulman said:

One possible meaning of "parametrically definable functor $\mathbf{Set}^n\to\mathbf{Set}$" is something arising from the set-theoretic semantics of an endofunctor of the smallest universe that's definable in predicative dependent type theory, and similarly for a "polymorphic function $\tau : \forall \alpha :F\alpha\to G\alpha$". In that case one would hope to be invoking external parametricity for DTT, but in that case the proof of naturality depends on the IEL for $F$ and $G$. I can't keep straight all the things we decided are true and aren't; do we know that IEL holds for such functors?

I was thinking of predicative Hindley-Milner polymorphism which I think should have a more straightforward set theoretic semantics than System F

Josselin Poiret (Aug 27 2025 at 08:20):

Patrick Nicodemus said:

I mean that if $\tau : \forall \alpha_1,\dots, \alpha_n. F(\alpha_1,\dots,\alpha_n)\to G(\alpha_1,\dots,\alpha_n)$ where $F$ is equipped with $fmap : \forall \vec{\alpha},\vec{\alpha}',\vec{\alpha}\to\vec{\alpha'}\to F(\vec{\alpha})\to F(\vec{\alpha}')$

and the set theoretic semantics of $F$ and $fmap$ define a functor, similarly with $G$

In this case, i'm pretty sure this isn't true, as $F$ and $G$ themselves can mention$$ ∀ $$, and these would need to be interpreted parametrically for the result to hold. Here's an example I think:
$F(X) = ∀ Y, Y → X$, $G(X) = X$.
Then define $ΛX.λF.F\; (X → X)\;\mathrm{id} : ∀ X.\; F(X) → G(X)$

Josselin Poiret (Aug 27 2025 at 08:23):

what happens here is reminiscent of the example we talked about in the other thread: if $F(X)$ was interpreted parametrically, then all its inhabitants would be constant functions, and the end result would be natural. But if the interpretation does include non-parametric functions $∀ Y, Y → X$, then there is no reason for the term above to be natural

Mike Shulman (Aug 27 2025 at 15:47):

But a functor that mentions $\forall$ doesn't have a set-theoretic semantics.

Patrick Nicodemus (Aug 27 2025 at 18:34):

Josselin Poiret said:

Patrick Nicodemus said:

I mean that if $\tau : \forall \alpha_1,\dots, \alpha_n. F(\alpha_1,\dots,\alpha_n)\to G(\alpha_1,\dots,\alpha_n)$ where $F$ is equipped with $fmap : \forall \vec{\alpha},\vec{\alpha}',\vec{\alpha}\to\vec{\alpha'}\to F(\vec{\alpha})\to F(\vec{\alpha}')$

and the set theoretic semantics of $F$ and $fmap$ define a functor, similarly with $G$

In this case, i'm pretty sure this isn't true, as $F$ and $G$ themselves can mention$$ ∀ $$, and these would need to be interpreted parametrically for the result to hold. Here's an example I think:
$F(X) = ∀ Y, Y → X$, $G(X) = X$.
Then define $ΛX.λF.F\; (X → X)\;\mathrm{id} : ∀ X.\; F(X) → G(X)$

Yes, as I said in my message to Mike I was talking about ML-style polymorphism. I guess your F is definable in ML but I mean to consider only fully applied type operators as functors, not curried type operators

Mike Shulman (Aug 27 2025 at 18:43):

I don't know exactly what "Hindley-Milner" or "ML-style" means, but I assumed you meant a theory with type variables but not type quantification. So a polymorphic function is defined in the context of one or more type variables, and you can informally think of it as universally quantified over those variables, but there isn't actually a type constructor $\forall$. I don't immediately see how to go beyond that and still have a set-theoretic semantics.

Patrick Nicodemus (Aug 27 2025 at 18:47):

Mike Shulman said:

I don't know exactly what "Hindley-Milner" or "ML-style" means, but I assumed you meant a theory with type variables but not type quantification. So a polymorphic function is defined in the context of one or more type variables, and you can informally think of it as universally quantified over those variables, but there isn't actually a type constructor $\forall$. I don't immediately see how to go beyond that and still have a set-theoretic semantics.

Yes. Maybe there is some syntactic restriction we can impose such as only permitting universal quantification at the outermost level, or that a product of types is simply not a type but something else, but this is what i had in mind. I was thinking that I would consider $F (X,Y) := Y\to X$ to be a well defined type constructor in the ML type system and $F(X) = \forall Y, Y \to X$ its partial application

Patrick Nicodemus (Aug 27 2025 at 21:25):

Mike Shulman said:

I don't know exactly what "Hindley-Milner" or "ML-style" means, but I assumed you meant a theory with type variables but not type quantification. So a polymorphic function is defined in the context of one or more type variables, and you can informally think of it as universally quantified over those variables, but there isn't actually a type constructor $\forall$. I don't immediately see how to go beyond that and still have a set-theoretic semantics.

Just for the sake of a formal reference, Jacobs calls the type theory $\lambda^\to$ and introduces it in chapter 8; he calls it "first-order polymorphic type theory" and seems to identify it with the simplest system of the $\lambda$-cube.

Ruby Khondaker (she/her) (Aug 27 2025 at 21:26):

Ah, is that from “categorical logic and type theory”?

Patrick Nicodemus (Aug 27 2025 at 21:27):

Ruby Khondaker (she/her) said:

Ah, is that from “categorical logic and type theory”?

Yes.

Mike Shulman (Aug 28 2025 at 01:18):

Patrick Nicodemus said:

Jacobs calls the type theory $\lambda^\to$ and introduces it in chapter 8; he calls it "first-order polymorphic type theory" and seems to identify it with the simplest system of the $\lambda$-cube.

Hmm, I don't have Jacobs in front of me, but I'm pretty sure that the simplest system of the lambda cube is STLC.

Patrick Nicodemus (Aug 28 2025 at 03:23):

That also occurred to me but I suppose Barendregts original paper considers systems with two distinguished symbols, Type and Kind, and classifies various systems by what the permissible abstraction rules are and the associated typing rule for the product. From this perspective all the systems contain type variables, it's just that in $\lambda\to$ you cannot quantify over them.