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: synthetic algebraic geometry vs continuation passing style

Ryan Wisnesky (Jun 23 2025 at 21:08):

I've noticed an informal correspondence between the primary "SQC" axiom of synthetic algebraic geometry (at least as formalized in HoTT: https://arxiv.org/abs/2307.00073) and a theorem about type theory (that every type is isomorphic to its type of continuations: https://stackoverflow.com/questions/60239815/how-to-understand-that-the-types-a-and-forall-r-a-r-r-are-isomorphic). I was hoping people here could tell me if this is just a coincidence, or if there is some deeper analogy between continuation passing style and this synthetic geometry axiom.
Screenshot 2025-06-22 at 1.08.48 AM.png
Screenshot 2025-06-23 at 2.10.38 PM.png
Screenshot 2025-06-22 at 1.08.35 AM.png
Anyway, if you unroll the definition of the algebraic geometry "SQC" axiom and write "->" for every kind of hom-set around, then this axiom looks like "forall R, forall A_R, A_R ~ ((A_R->R)->R)" (where A_R indicates an R-Algebra called A). Whereas in type theory, the theorem looks like "forall A, A ~ forall R, ((A->R)->R)" (with A and R just types). So it both cases it seems like some "double negative" translation is happening (and one direction of each iso is defined the same in both cases), but I don't have the algebraic geometry background to really dig in, so I wanted to ask this list.

John Baez (Jun 23 2025 at 22:00):

What's this "algebraic geometry axiom"? I see in big letters the definition of the spectrum of an algebra A over a ring R, which is

Spec(A) = hom(A,R)

But that's not an axiom - at least for me, it's a definition. Can you write down the axiom?

Ryan Wisnesky (Jun 23 2025 at 22:05):

The axiom is "SQC" - it's the statement that A and (Spec A -> R) are equivalent (from the first image). The images are from the first two pages of the arxiv paper linked, and from the stack overflow post. I included the definition of Spec A to try to make the images self contained. Zulip expands small images, there's no meaning to its large size.

John Baez (Jun 23 2025 at 22:19):

Oh, okay.

Mike Shulman (Jun 23 2025 at 23:36):

Well, whenever you have an endofunctor like $[-,R]$ that's adjoint to itself on the right ($\hom(X,[Y,R]) \cong \hom(Y,[X,R])$), every object has a "double dualization" map $X \to [[X,R],R]$, and you can talk about whether it is a reflexive object meaning that that map is an isomorphism.

Mike Shulman (Jun 23 2025 at 23:38):

This is not exactly the case for SQC: there it's more general, you have a contravariant adjunction between non-endo functors $G$ and $H$ (there, between objects and R-algebras) and the map in question is the unit $X\to GHX$ of the adjunction on one side. Then asking that map to be an isomorphism is asking $X$ to be a [[fixed point of an adjunction]].

Mike Shulman (Jun 23 2025 at 23:39):

It's also not an axiom $\forall R$, only about one particular distinguished local ring $R$.

Mike Shulman (Jun 23 2025 at 23:40):

But if you do quantify over $R$ then you can define a map $A \to \forall R. ((A \to R) \to R)$, as in the type theory situation you mention, and ask whether it is an isomorphism. I don't think this is the unit of any adjunction, though.

Mike Shulman (Jun 23 2025 at 23:41):

I'm also dubious about the "theorem" that that map is an isomorphism. It certainly isn't an isomorphism in most models. (There are maps in both directions, but they aren't inverses.) Do you know what exactly is being claimed? Is it assuming internal parametricity?

Madeleine Birchfield (Jun 23 2025 at 23:43):

Ryan Wisnesky said:

Anyway, if you unroll the definition of the algebraic geometry "SQC" axiom and write "->" for every kind of hom-set around, then this axiom looks like "forall R, forall A_R, A_R ~ ((A_R->R)->R)" (where A_R indicates an R-Algebra called A).

The SQC axiom used in synthetic algebraic geometry only applies to the finitely presented $R$-algebras $A$, not all $R$-algebras. And SQC applies only to a specified local ring $R$ provided by a different axiom in synthetic algebraic geometry, not to all local rings. See section 2 of:

https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/foundation-for-synthetic-algebraic-geometry/166673A0C34C63B01F2337E252FE5177

Ryan Wisnesky (Jun 24 2025 at 01:15):

@Mike Shulman there are many claims of isomorphism between a type and its type of continuations floating around the internet, for example https://www.williamyaoh.com/posts/2022-05-02-the-cont-monad.html . The book referenced in the stack overflow post is paywalled. But in trying to prove the isomorphism just now, I would agree that one direction is trivial and the other is not, and that parametricity does seem like something that might help. It does seem like the isomorphism claims may be wrong in general models.

Mike Shulman (Jun 24 2025 at 02:14):

I guess you can't even talk about models in Set, since you need an impredicative universe to even write $\forall R. ((X\to R) \to R)$. But I would be surprised if that were an isomorphism in, say, the effective topos, without any semantic parametricity.

Ryan Wisnesky (Jun 24 2025 at 03:26):

Here's a proof of isomorphism by Bartosz: https://bartoszmilewski.com/2015/09/01/the-yoneda-lemma/ (go to the middle) which uses the Yoneda lemma but I can't quite tell if it also requires parametricity.

Mike Shulman (Jun 24 2025 at 04:16):

Thanks. To use the Yoneda lemma there, you need $\forall R$ to refer to natural transformations. That's certainly not true in ordinary System F, for instance, although you can prove it from internal parametricity.

Ryan Wisnesky (Jun 24 2025 at 04:24):

can you elaborate? specifically, does that mean the Bartosz proof is incorrect without additional assumptions? If so I might leave a comment on his (and possibly other) sites about this "folk quasi theorem" (I certainly believed it for years without ever working through a proof).

Mike Shulman (Jun 24 2025 at 04:30):

Yes, I would say the proof is incorrect. It's a bit tricky because he isn't clear about what formal mathematical context he's working in: to talk about "isomorphism" in the first place, let alone Yoneda, you have to be in a category, and as we know Hask is not a category. But the closest thing there is to a category Hask is some denotational semantic category of domains, which doesn't in general satisfy internal parametricity unless you add it, and without that I don't think this proof works.

Mike Shulman (Jun 24 2025 at 04:32):

If this is the sort of elaboration you want: Yoneda says that $Fa$ is isomorphic to the set of natural transformations from $(a\to -)$ to $F$. Such a natural transformation consists of, for every $x$, a morphism $(a\to x) \to Fx$, plus a naturality condition. Whereas an element of $\forall x. ((a\to x)\to x)$ consists only of the morphisms $(a\to x) \to Fx$ for every $x$ without the naturality condition.

Mike Shulman (Jun 24 2025 at 04:34):

Since System F (and presumably Haskell) satisfies external parametricity as a metatheorem, it should be true that every closed term inhabiting $\forall x. ((a\to x)\to x)$ is natural, and therefore there is a bijection between closed terms of type $\forall x. ((a\to x)\to x)$ and closed terms of type $a$. But that's a weaker statement than saying that those two types are isomorphic in the category in question.

Ryan Wisnesky (Jun 24 2025 at 04:38):

Any intuition on if it would hold in Set? Does that question even make sense given how there are no (classical) set-theoretic models of polymorphism? Or is system F the simplest category within which to analyze the Bartosz argument?

Mike Shulman (Jun 24 2025 at 04:43):

I think that question doesn't even make sense, for the reason you give.

Mike Shulman (Jun 24 2025 at 04:47):

I should perhaps say that I'm less than 100% sure of my conclusion here about the incorrectness of the proof. I still don't feel like I completely understand models of polymorphism, and I don't have a concrete counterexample (e.g. a category of domains in which $\forall x. ((a\to x)\to x)$ is evidently not isomorphic to $a$).

Mike Shulman (Jun 24 2025 at 04:51):

One thing that occurs to me now is that there might be ways to make System F into a category in which this is true. For instance, maybe you can define two functions $f,g : a \to b$ to be equal if they behave the same "observationally" on closed terms. Then since there is a bijection between closed terms of $\forall x. ((a\to x)\to x)$ and $a$, and definable functions that implement that bijection, maybe those functions would be inverses in this "observational category".

I don't think that would be a very useful category, from a category-theorist's perspective, since this sort of "observational equality" doesn't seem like it would be preserved by interpretations, so for instance you wouldn't get a "semantics" functor from this category into domains. But maybe something like this is what people have in mind when they talk about such an isomorphism?

Is anyone around here more of an expert on this than me?

Josselin Poiret (Jun 24 2025 at 08:34):

the usual trick to contradict anything parametric is to rely on an operation like typecase in the model. a sketch counterexample would be to build an inhabitant of $∀ x. ((a → x) → x)$ in the model that inspects $x$ and does something weird depending on its shape. Fix $t : a$, then if $x$ is isomorphic to $\mathrm{bool}$, return $λ f. s(f(t))$ where $s$ is the non-identity automorphism, otherwise return $λ f. f(t)$

Josselin Poiret (Jun 24 2025 at 08:35):

then under the two maps, you get back a function that's observationally different from the one you started with

Mike Shulman (Jun 24 2025 at 15:04):

Right, but can you do that in a category that has an impredicative universe?

Josselin Poiret (Jun 25 2025 at 08:56):

i'd be very surprised if there isn't a model of system F + typecase

daniel gratzer (Jun 25 2025 at 11:04):

Josselin Poiret said:

i'd be very surprised if there isn't a model of system F + typecase

It's not so obvious to me. If your typecase allows for matching on a $\forall$, then one can construct an epimorphism $U \to (A \to U)$ for any $A$ and apply Lawvere's fixed point theorem to conclude that every map $U \to U$ has a fixed point. Taking, for instance, the map sending $A$ to $A \to \bot$ one can show that $\top = \bot$ in $U$, so the universe has to be trivial.

Josselin Poiret (Jun 25 2025 at 12:18):

you're right, it's probably not that simple: I also concomitantly found a couple pages describing inconsistencies of impredicativity + typecase + injectivity of type constructors

Josselin Poiret (Jun 25 2025 at 12:19):

(note although that there's no U in system F)

Kenji Maillard (Jun 25 2025 at 13:21):

Palmgren's On universe in type theory shows that Typecase on an impredicative universe goes boom (inconsistent).

But I'm missing a step in @daniel gratzer's argument to conclude that the universe is trivial. How is that a consequence of the fact that negation has a fixpoint ? (I'm vaguely thinking that there should be some kind of domain models that accomodate "infinite types" $(((\ldots \to \bot) \to \bot) \to \bot) \to \bot$ that could be such a fixpoint).

daniel gratzer (Jun 25 2025 at 13:32):

I suppose I was too hasty, if negation has a fixed point then one can show that $\bot$ is inhabited. This is not the same as $U$ being trivial I suppose, but it does mean the model is uninteresting from a logical perspective at least.

Mike Shulman (Jun 25 2025 at 14:27):

But of course $\bot$ is inhabited anyway in categories of domains that admit general recursion.

daniel gratzer (Jun 25 2025 at 14:33):

Mike Shulman said:

But of course $\bot$ is inhabited anyway in categories of domains that admit general recursion.

Indeed... I'd guess that System F + type case is actually inconsistent, but it's not exactly obvious. It's just that all the models of System F that I can think of seem sort of incapable of adaptation to handle type-case. And, of course, non-trivial domain models of PCF or whatever show that inconsistency is not the same thing as being uninteresting.

Mike Shulman (Jun 25 2025 at 14:34):

What do you think about the original question of a model of System F in which $a \not\cong \forall x. ((a\to x)\to x)$?

Mike Shulman (Jun 25 2025 at 14:34):

Typecase was just the most obvious way to violate such an isomorphism.

Madeleine Birchfield (Jun 25 2025 at 17:45):

Doesn't propositional extensionality imply that if $\bot$ is inhabited, then the universe is trivial?

Mike Shulman (Jun 25 2025 at 17:46):

Well, if $\bot$ is inhabited in a dependent type theory, you can prove anything, and therefore every type is trivial and every type is nontrivial, etc. But System F is not a dependent type theory, and doesn't have a "universe" as such, it only has impredicative quantification over types.

Madeleine Birchfield (Jun 25 2025 at 17:53):

So then the situation that Daniel Gratzer is talking about above wouldn't apply to System F because it doesn't have a universe $U$. (Edit: although I now see that Josselin Poiret made the exact same point above)

Mike Shulman (Jun 25 2025 at 17:55):

Right.

Evan Cavallo (Jun 28 2025 at 11:32):

From Hyland, Robinson, and Rosolini, "Algebraic Types in PER Models" (https://www.dpmms.cam.ac.uk/~jmeh1/Research/Pub81-90/hrr90.pdf):

Finally, we should return to the relationship between PER models and the free term model. We stated above that any PER model satisfies equations which are not provable in the calculus, and which therefore do not hold in the free term model. We can now give an example. If we let $P$ be the type $\Pi X.X \to X$, $Q = P \to P$ be the type of endomorphisms of $P$, and $S$ be the "double negation" $\Pi X.[[Q \to X] \to X]$ of $Q$, then it is well-known that there is a closed term of type $S$ which is not formally evaluation at any closed term of type $Q$ (the term $\Lambda X. \lambda f : Q \to X. f(\lambda a : P. (a[X \to P](\lambda x : X. \Lambda Y. \lambda y : Y. y)(f(\lambda p : P.p))))$ will do). It follows that in any extensional model, either we violate parametricity, in that $S$ is not isomorphic to $Q$, or there is a non-standard element of $Q$, or else some equation holds in the model which does not hold in the term model. In the particular case of PER models, we know that $P$ contains only the polymorphic identity. It follows that $Q$ and $S$ are also singletons, and that the term we have given is equated in the model to evaluation at the identity map on $P$.

Mike Shulman (Jun 28 2025 at 15:05):

Nice! This "well-known" (ugh) fact seems to be just what we need: it shows that in the ordinary term model of System F there is a type $a$ such that $\forall x. ((a\to x)\to x)$ is not isomorphic to $a$. So the "proof of isomorphism" that we were discussing above from here is incorrect if it's meant to be a proof in the ordinary syntax of System F or a related theory.

Mike Shulman (Jun 28 2025 at 15:08):

Of course there are some models in which the isomorphism holds, such as internal parametricity models (which I think I would say include PER models). The "contextual/observational equality" model I suggested previously, if it exists, would be another example. But if what's meant is to refer to one of these models, then I think it is at least highly misleading to assert "$\forall x.((a\to x)\to x)$ is isomorphic to $a$" without indicating that it's only a statement about a particular special model.

Ryan Wisnesky (Jun 28 2025 at 19:08):

I think my conclusion here is that working in Haskell, where "well typed programs cannot go wrong", makes it all too tempting to assume that "not going wrong" extends to having proofs of things like isomorphisms without bothering to check them. It's hard to imagine these same blog posts (or book!) in Coq would have made such expansive claims. (And this topic itself is probably worthy of a blog post). But FWIW, this is the first "organic" type I've seen behave this way; my original question was less about this particular type, than wondering if there's a deeper reason this kind of 'double negative' translation pops up so often, with one direction so often being stipulated axiomatically, such as apparently in synthetic algebraic geometry, which I think Mike answered earlier.

Mike Shulman (Jun 28 2025 at 21:21):

Yes, I was also thinking that someone should write a blog post about this. Any volunteers? (-:

Mike Shulman (Jun 28 2025 at 21:26):

I'm curious to know exactly what that book claims about it. The cited section on the continuation monad isn't part of the free preview. The preview does include a section that defines "isomorphism", and does it correctly, although it doesn't say precisely what the "=" sign means in to o from = id (that is, what category we're working in).

Ryan Wisnesky (Jun 28 2025 at 23:40):

I can write the post, if it can be hosted elsewhere (I have no blog). I, uh, just acquired a copy of the book in a game of chance and it had little to say (images attached):
Screenshot 2025-06-28 at 4.38.12 PM.png
Screenshot 2025-06-28 at 4.38.31 PM.png
Screenshot 2025-06-28 at 4.38.26 PM.png
Screenshot 2025-06-28 at 4.38.20 PM.png

Mike Shulman (Jun 28 2025 at 23:46):

Haha!

Spend a few minutes looking at cont and runContto convince yourself you know why these things form an isomorphism.

In other words, "reinvent parametricity and the Yoneda lemma on your own and give an [incorrect] proof that parametricity implies naturality".

Mike Shulman (Jun 28 2025 at 23:47):

I'd be happy to guest-post it for you at the n-Cafe.

Mike Shulman (Jun 28 2025 at 23:51):

I also realized that this "well-known" (sorry, I can't get over that) example also implies I was wrong when I said

Mike Shulman said:

there is a bijection between closed terms of $\forall x. ((a\to x)\to x)$ and $a$

In particular, therefore, it would be more complicated than I originally suggested to define an "observational/contextual equality" syntactic category in which these types are isomorphic. You couldn't just define two functions to be equal if they act the same, up to definitional equality, on closed terms; instead they would have to act the same up to the same sort of "contextual" equality.

Mike Shulman (Jun 28 2025 at 23:55):

I think this also means that the slogan "parametricity implies naturality" is not correct in general, because System F does satisfy external parametricity, but here we have a counterexample to naturality on closed terms. Thinking about the proof of naturality from parametricity, I think it only works for functors that are sort of "first-order" or "discrete" so that their parametricity transforms are equality. That's true, for instance, for datatype functors like $\mathsf{List}$, and also I think for representables $X\mapsto (A\to X)$ when $A$ is a discrete datatype like $\mathbb{N}$, but it fails for $X\mapsto (Q\to X)$ for this $Q = (\forall X.(X\to X)) \to (\forall X.(X\to X))$.

Ryan Wisnesky (Jun 28 2025 at 23:57):

just to double check my understanding, without a bijection in the term model, even the Bartosz proof (with its more limited claims) is incorrect?

Mike Shulman (Jun 29 2025 at 00:17):

Yes, I'm now willing to stand behind that claim. On his page about natural transformations he says

A natural transformation is a polymorphic function that is defined for all types a:

alpha :: forall a . F a -> G a

...
Haskell’s parametric polymorphism has an unexpected consequence: any polymorphic function of the type:

alpha :: F a -> G a

where F and G are functors, automatically satisfies the naturality condition....

fmap f . alpha = alpha . fmap f

This is still not real Haskell — function equality is not expressible in code — but it’s an identity that can be used by the programmer in equational reasoning; or by the compiler, to implement optimizations.

And on his previous page about functors, he said that by "equational reasoning" he means definitional equality:

equational reasoning... takes advantage of the fact that Haskell functions are defined as equalities: the left hand side equals the right hand side. You can always substitute one for another, possibly renaming variables to avoid name conflicts.

So he really does seem to be claiming that every function of type forall a . F a -> G a is natural in the term model, and that forall r . (a -> r) -> r is isomorphic to a in the term model. Which this example shows is false.

Ryan Wisnesky (Jun 29 2025 at 03:23):

the claim that any polymorphic function forall x, F x -> G x in Haskell must be natural isn't just in Bartosz's post, it is in course notes, for example: https://pages.cs.wisc.edu/~jcyphert/categoryTheoryNotes/basics/3_NaturalTransformations.pdf
Screenshot 2025-06-28 at 8.20.20 PM.png
Could these various notes etc mean that when F and G are functors in the sense of Haskell's type class (internal functors), then you have naturality, which would imply that Continuations are not a monad? Or is this incorrect folklore just widespread?

Mike Shulman (Jun 29 2025 at 03:50):

The reader monad (i.e. covariant representable) is certainly an internal functor, so I don't think that matters. My guess is that it's just widespread incorrect folklore.

Ryan Wisnesky (Jun 29 2025 at 04:23):

In googling around my guess is "every natural transformation turns into a polymorphic function" (which seems unobjectionable to me) gets conflated with its converse, "every polymorphic function turns into a natural transformation", in a lot of places. We'll have to add this bit of incorrect folklore to blog post too!

Mike Shulman (Jun 29 2025 at 04:59):

In connection with Haskell specifically, one thing that occurs to me is that the counterexample uses what Haskell calls a "rank 2 type" $(\forall X. X\to X) \to (\forall X. X\to X)$, which are officially a "language extension" (although System F has arbitrary-rank types, as does OCaml without being "extended" (although there you have to wrap them in a record)). I wonder whether this is necessary.

Ryan Wisnesky (Jun 29 2025 at 07:48):

aight, I have a Coq proof that if you assume Reader -> Id is a natural transformation, then you have an iso between a and forall x, (a->x)->x. (And assume dependent fun ext). Now I'll try to see what goes wrong proving that Reader -> Id is natural in Coq.

Mike Shulman (Jun 29 2025 at 16:06):

Do you mean if you assume that every function of type forall x, (a -> x) -> x is natural?

Ryan Wisnesky (Jun 29 2025 at 17:29):

That is how I phrased the axiom, but then the proof of isomorphism only instantiated that axiom with a single choice of function of that type, so maybe naturality is too strong. As a next step, I got the 'free theorem' for that type from a programatic generator, so next I'll check that the free theorem doesn't imply naturality
cont.v

Mike Shulman (Jun 29 2025 at 18:45):

Axiom natural: forall (F G : Type->Type)
  (fmap : forall {a b}, (a->b)->F a -> F b) (gmap : forall {a b}, (a->b) -> G a -> G b)
  (alpha : forall a, F a -> G a) a b (h:a->b)  ,
  o (fmap h) (alpha _) = o  (alpha _) (gmap h).

Lemma l2 : forall a (f:forall r, (a -> r) -> r), cont _ (unCont _ (f )) = f .
Proof.
intros a f; apply  functional_extensionality_dep;
intros t; apply  functional_extensionality_dep; intros g.
pose (natural (fun z => a -> z) (fun z=>z) (fun b f g h w => g (h w)) (fun a b f x => f x) f a t g) as ax.
apply (fapp (a->a) _ _ _ (fun z=>z)) in ax.
assert (g = fun w : a => g w) as H; auto; rewrite H .
Qed.

It looks to me like you instantiated the axiom natural with an arbitrary function f of that type, so you are by definition using the full strength of that axiom (for these specific choices of functors F and G).

Mike Shulman (Jun 29 2025 at 18:45):

What is the "free theorem" for that type?

Ryan Wisnesky (Jun 29 2025 at 18:48):

ah, touche. I grabbed the free theorem from here: https://www.mercerenies.com/projects/lambda-games?free-theorem=∀+r.+%28a-%3Er%29+-%3E+r
Screenshot 2025-06-29 at 11.48.19 AM.png

Mike Shulman (Jun 29 2025 at 19:01):

That looks like it would imply naturality, but I don't think it's what you want to start from. That's a free theorem for something of type $\forall a. \forall r. ((a\to r) \to r)$, but what we have is something of type $\forall r. ((a\to r) \to r)$ where $a$ is some fixed type.

Mike Shulman (Jun 29 2025 at 19:03):

Specifically, in the counterexample $a$ is $(\forall x. x\to x) \to (\forall x. x\to x)$. What does the free theorem generator give you for the type

$$\forall r. (((\forall x. x\to x) \to (\forall x. x\to x)) \to r) \to r$$

?

Ryan Wisnesky (Jun 29 2025 at 19:10):

if that free theorem (for forall r, (a->r)->r) implied naturality, then wouldn't external parametricity of system F imply that free theorem holds for system F, contradicting the 90s Hyland result? I was actually expecting the proof of naturality from paremetricity to fail in general. The free theorem for the bigger type is of course larger:
Screenshot 2025-06-29 at 12.07.47 PM.png

Mike Shulman (Jun 29 2025 at 22:02):

What is F?

Ryan Wisnesky (Jun 29 2025 at 22:17):

"that free theorem" refers to "forall r, (a->r)->r" and its free theorem. My confusion is whether external parametricity for system F should imply naturality for Reader->Id, because in my mind that would contradict Hyland's result (the term model being external parametric?).

Mike Shulman (Jun 29 2025 at 22:19):

Yes, but I asked what you meant by "F".

Ryan Wisnesky (Jun 29 2025 at 22:19):

oh, by F I meant system F

Mike Shulman (Jun 29 2025 at 22:23):

Ok, and what does "naturality for Reader->Id" mean? Reader and Id are, I presume, functors, so Reader->Id could mean the type of natural transformations, or it could mean the type of unnatural transformations, but neither one is a thing that can be natural; only an individual transformation can be natural.

Mike Shulman (Jun 29 2025 at 22:25):

Sorry if I'm being annoying, but I suspect sloppy use of language is one cause of this whole issue.

Ryan Wisnesky (Jun 29 2025 at 22:27):

"naturality for Reader->Id" is what i'm calling the (instantiation of the) axiom I assumed in the coq development, from which the isomorphism of a and forall r, (a->r)->r follow

Mike Shulman (Jun 29 2025 at 22:28):

An element of $\forall a.\forall x.(a\to x)\to x$ is not just one transformation but a family of them defined parametrically for all a. So its free theorem can say that all of its pieces are natural, without implying that all transformations for fixed a are natural.

Ryan Wisnesky (Jun 29 2025 at 22:31):

ok, I understand your response to mean that I should not be able to prove that axiom in the Coq development from the free theorem for "forall a, x, (a->x)->x", that makes sense to me... then I suppose the final question is if some other free theorem for a different type would allow to prove the axiom. In particular, would your proposed type from 12:03pm (CA time) work? (and is that why you proposed it?)

Mike Shulman (Jun 29 2025 at 23:05):

Well, if the counterexample is correct, then no (correct) free theorem can imply that all transformations $\mathrm{Reader}_a \to \mathrm{Id}$, for any fixed $a$, are natural. (-:

Mike Shulman (Jun 29 2025 at 23:06):

I proposed that type because that would at least be a free theorem that applies to the transformation in the counterexample -- the first one doesn't, because the counterexample isn't parametric over all $a$. So I thought that seeing why that free theorem also doesn't imply that the transformation is natural might be instructive.

Ryan Wisnesky (Jun 29 2025 at 23:14):

would it be fair to say we would need free theorems for open types (such as "forall r, (a->r)->r" for a type variable a) to be able to establish naturality? I'm trying to come up with some kind of short intuition for how parametricity can fail to yield naturality (besides having a counterexample) before starting writing the blog post.

Mike Shulman (Jun 30 2025 at 00:31):

Here's my intuition:

Mike Shulman said:

Thinking about the proof of naturality from parametricity, I think it only works for functors that are sort of "first-order" or "discrete" so that their parametricity transforms are equality. That's true, for instance, for datatype functors like $\mathsf{List}$, and also I think for representables $X\mapsto (A\to X)$ when $A$ is a discrete datatype like $\mathbb{N}$, but it fails for $X\mapsto (Q\to X)$ for this $Q = (\forall X.(X\to X)) \to (\forall X.(X\to X))$.

Mike Shulman (Jun 30 2025 at 00:36):

HRR describe $Q$ not being isomorphic to $\forall X. ((Q\to X)\to X)$ as a "failure of parametricity", but at the moment I'm not convinced that that's an accurate description, because I don't see how any kind of parametricity, even fully internal parametricity, would imply such an isomorphism for an arbitrary type $Q$. They do explain how the form of parametricity that holds in their PER model implies such an isomorphism for their particular type $Q$, and I expect the same would work in dependent type theory with internal parametricity. But the reason that works is different from the reason that it works when $Q$ is "rank-1", so I don't see a general argument.

Ryan Wisnesky (Jun 30 2025 at 01:00):

Any thoughts on where naturality comes from, when it can't come from parametricity (or a PER model)? That is, what is the most natural model for which all polymorphic functions are natural transformations? perhaps the "observational category"?

Mike Shulman (Jun 30 2025 at 01:03):

What makes you think such a model should exist?

Ryan Wisnesky (Jun 30 2025 at 01:25):

I heard a rumor once that there are models of system-F-like lambda calculi where "all functions are functors", and so have a naive hope that there might be a model where "all polymorphic functions are natural". I'm also trying to figure out when naturality implies parametricity; does one concept subsume the other or are they incomparable?

Mike Shulman (Jun 30 2025 at 01:27):

Well, I haven't heard that rumor, so I don't think I can help you. I would say they are incomparable in general; I don't know of any context in which naturality implies parametricity.

Patrick Nicodemus (Jun 30 2025 at 01:38):

I might have missed something in the thread so excuse me if I am repeating a misunderstanding which has already been cleared up.

But it should be the case that for closed definable functors $F, G :\prod_{\alpha:\mathsf{Type}}\mathsf{Type}$, and closed definable $\tau : \prod_\alpha : F(\alpha)\to G(\alpha)$, we have that $\tau$ is "natural" up to observability/contextual equivalence: for any ground types $a,b$ and any closed term $f : a\to b$, if $t[-]$ is a closed term of type $\mathsf{bool}$ with a hole of type $F(a)\to G(b)$, then $t[\tau_b\circ F(f)]=t[F(g)\circ \tau_a]$

Patrick Nicodemus (Jun 30 2025 at 01:45):

And the parametricity translation into dependent type theory given in the "Proofs for Free" paper maps an arbitrary type variable $\alpha$ to a pair of type variables and a binary relation $\alpha, \beta, R : \alpha\to\beta\to\mathsf{Type}$, and one then can freely specialize $R$ to whatever you like because it's just a variable in the context, so one could substitute $\beta$ for $\alpha$ and then substitute in equality for $R$ (either the Martin-Lof type or an extensional equality).

This is a bit handwavy as I don't know of a concrete dependent type theory with extensional equality which embeds System F.

Mike Shulman (Jun 30 2025 at 02:08):

Patrick Nicodemus said:

But it should be the case that for closed definable functors $F, G :\prod_{\alpha:\mathsf{Type}}\mathsf{Type}$, and closed definable $\tau : \prod_\alpha F(\alpha)\to G(\alpha)$, we have that $\tau$ is "natural" up to observability/contextual equivalence: for any ground types $a,b$ and any closed term $f : a\to b$, if $t[-]$ is a closed term of type $\mathsf{bool}$ with a hole of type $F(a)\to G(b)$, then $t[\tau_b\circ F(f)]=t[F(g)\circ \tau_a]$

That's good to have recorded, and maybe it answers Ryan's question about in what sense "all polymorphic functions are natural". Can you give a citation with a proof? (At this point I'm feeling extra-suspicious of all "parametricity implies naturality" claims.)

Mike Shulman (Jun 30 2025 at 02:14):

I think the point we're observing here is that to get a "CPS isomorphism" $X\cong \prod_\alpha ((X\to \alpha) \to \alpha)$, you would need a stronger sort of naturality: that even every variable $\tau : \prod_\alpha F(\alpha) \to G(\alpha)$ (for the case $F(\alpha) = X\to \alpha$ and $G(\alpha) =\alpha$) is natural for any variable types $\alpha,\beta$ and variable function $f:\alpha\to\beta$, and up to definitional equality rather than contextual equivalence.

Mike Shulman (Jun 30 2025 at 02:16):

And the counterexample in HPP seems to show that there is even a closed definable $\tau : \prod_\alpha ((X\to \alpha) \to \alpha)$ (for a particular closed definable $X$) that fails to be definitionally-natural on variable functions $f:\alpha \to \beta$.

Ryan Wisnesky (Jun 30 2025 at 02:20):

at this point, tbh, I can't even remember if there exists a model of the Coq axiom (Reader -> Id naturality), much less naturality for all polymorphic functions.

Ryan Wisnesky (Jun 30 2025 at 06:15):

here's a claimed agda proof that naturality follows from parametricity for internal functors: https://cs.stackexchange.com/questions/136359/rigorous-proof-that-parametric-polymorphism-implies-naturality-using-parametrici . if that can be translated into Coq to implement the Reader->Id axiom, then I'll be further confused, but I think it's my next step.

Ryan Wisnesky (Jun 30 2025 at 06:23):

And this post: https://cs.stackexchange.com/questions/9818/what-is-meant-by-category-theory-doesnt-yet-know-how-to-deal-with-higher-order gives a simple example of a polymorphic function that is not natural b/c its associated type constructor is not functorial (simpler than the 90s paper example)
Screenshot 2025-06-29 at 11.22.26 PM.png

Patrick Nicodemus (Jun 30 2025 at 06:55):

Mike Shulman said:

I think the point we're observing here is that to get a "CPS isomorphism" $X\cong \prod_\alpha ((X\to \alpha) \to \alpha)$, you would need a stronger sort of naturality: that even every variable $\tau : \prod_\alpha F(\alpha) \to G(\alpha)$ (for the case $F(\alpha) = X\to \alpha$ and $G(\alpha) =\alpha$) is natural for any variable types $\alpha,\beta$ and variable function $f:\alpha\to\beta$, and up to definitional equality rather than contextual equivalence.

I'm optimistic that this works for variable types, because in System F you can just erase the types and treat them as untyped lambda terms, the types don't play a computational role so they shouldn't matter. But my intuition here is depending on the fact that System F is strongly normalizing so every closed term of type $\mathsf{bool}$ should normalize to true or false, and if f is variable then the computation sticks and you might no longer get definitional equality of those terms? And certainly the definitional equality thing seems a much stricter requirement, that one doesn't even sound plausible to me, is that even true for functions List A -> List A in Coq?

Patrick Nicodemus (Jun 30 2025 at 07:06):

Here's a simple example, List.rev \circ map f is not definitionally equal to map f \circ List.rev. Not sure what the standard notion of definitional equality in System F works out to if you use various tricks to encode lists or add simple inductive types.

Definition id (A : Type) : A -> A := fun x => x.
Definition compose {A B C : Type} (f : A -> B) (g : B -> C) :=
  fun (x : A) => g (f x).

Goal forall (A B : Type) (f : A -> B), compose f (id _) = compose (id _) f.
Proof.
  intros A B f.
  reflexivity.
  (* This works. *)
Qed.

Definition revapp {A : Type} : list A -> list A -> list A :=
  fix revapp (l1 l2 : list A) {struct l1} :=
    match l1 with
    | nil => l2
    | cons hd tl => revapp tl (cons hd l2)
    end.

Definition rev (A : Type) : list A -> list A := fun l1 => revapp l1 nil.

Definition map {A B : Type} (f : A -> B) : list A -> list B :=
  fix map l1 :=
    match l1 with
    | nil => nil
    | cons hd tl => cons (f hd) (map tl)
    end.

Goal forall (A B : Type) (f : A -> B),
    compose (map f) (rev _) = compose (rev _) (map f).
Proof.
  intros A B f.
  Fail reflexivity.

Ryan Wisnesky (Jun 30 2025 at 07:41):

could the reason that parametricity "fails" on hyland et al's example be that the type constructor it corresponds to is not functorial? the image I linked says T(X):=X->X is not functorial, and that type appears in Hyland's example

Kenji Maillard (Jun 30 2025 at 08:10):

Ryan Wisnesky said:

could the reason that parametricity "fails" on hyland et al's example be that the type constructor it corresponds to is not functorial? the image I linked says T(X):=X->X is not functorial, and that type appears in Hyland's example

No, the type constructor in Hyland et al.'s example is the parametric continuation monad $\mathrm{Cont}(Y) := \forall X. (Y \to X) \to X$ which is functorial for the $\beta\eta$ equational theory of System F:

mapCont (f : A → B) (m : Cont A) : Cont B := Λ X. λ (k : B → X). m X (λ (a : A). k (f a))

mapCont (λ (x : A). x) m
= Λ X. λ (k : B → X). m X (λ (a : A). k ((λ x : A. x)  a))
= Λ X. λ (k : B → X). m X (λ (a : A). k a)
= Λ X. λ (k : B → X). m X k
= m

mapCont (g : B → C) (mapCont (f : A → B) m) =
= Λ X. λ (k : C → X). (Λ X. λ (k : B → X). m X (λ (a : A). k (f a))) X (λ (b : B). k (g b))
= Λ X. λ (k : C → X). m X (λ (a : A). (λ (b : B). k (g b)) (f a))
= Λ X. λ (k : C → X). m X (λ (a : A). k (g (f a)))
= mapCont (λ (x : A). g (f x)) m

Ryan Wisnesky (Jun 30 2025 at 08:22):

sure, but it's the continuation monad with the parameter chosen to be "(forall x, x->x)->(forall x, x->x)"; which the image notes isn't functorial. I'm really asking whether "naturality from parametricty" fails on hyland's example because he uses a non-functorial type ("(forall x, x->x)->(forall x, x->x)") as the parameter to the continuation monad and not a functorial type like "nat" or "list" as the parameter (as Mike was mentioning earlier)

Kenji Maillard (Jun 30 2025 at 08:27):

What do you mean by a functorial type like Nat ? That it is (at least isomorphic to) the initial algebra of some endofunctor ?

Ryan Wisnesky (Jun 30 2025 at 08:32):

by a functorial type, I mean a type constructor that corresponds to a functor, such as X |-> X but not X |-> X->X. I.e, if the type constructor is called T, then you can write down its corresponding "fmap : (a->b)->Ta->Tb"

Kenji Maillard (Jun 30 2025 at 08:35):

Ryan Wisnesky said:

by a functorial type, I mean a type constructor that corresponds to a functor, such as X |-> X but not X |-> X->X

How do you see nat or Q as type constructors here ? I'm having a hard time to follow precisely.

Kenji Maillard (Jun 30 2025 at 08:36):

Also, I would expect that "functoriality" is not the right keyword here, but as Mike mentionned it earlier in this discussion, the rank of the type to which we apply the continuation monad should matter. They are a few works from the 90s showing that CPS translations "work well" at low enough rank (I'm thinking of Girard's A new constructive logic: classical logic but there should be others that I don't remember immediately).

Ryan Wisnesky (Jun 30 2025 at 08:40):

nat would be a constant type constructor, X |-> nat. I'd read Hyland's S (instead of Q) as the type constructor X |-> (Q -> X) ->X

Kenji Maillard (Jun 30 2025 at 08:50):

I thought one of the point of this discussion was to compare the relationship between $\mathbb{N}$ and $\mathrm{Cont}~\mathbb{N}$ (I would expect the two types isomorphic on closed system F terms) with that of $Q$ and $\mathrm{Cont}~Q$ (for which Hyland et al show that the types are not isomorphic on closed system F terms). Did I misunderstand that part ?

Ryan Wisnesky (Jun 30 2025 at 08:56):

right- why are Q and Cont Q not isomorphic, whereas N and Cont N are isomorphic? Is it because of a naturality (or functoriality) property N has that Q doesn't? Or some other reason?

Mike Shulman (Jun 30 2025 at 14:20):

The point is that the variable $X$ is bound in $Q = (\forall X. X\to X) \to (\forall X. X\to X)$, so it doesn't even make sense to ask whether it's a functor: it's just a single type, not an operation mapping types to types. Similarly, the HPP $S$ is the constant type $\forall X. ((Q\to X) \to X)$ in which $X$ is bound. A single type cannot have a "naturality" or "functoriality" property.

Of course any single type can be regarded as a constant mapping all types to the same one, but that is a functor, a constant functor.

James Deikun (Jun 30 2025 at 14:52):

I think the relevant distinction probably is that $Q$ itself has nontrivial equations due to parametricity, that are not reflected by the definitional equality. I think, though, that internal parametricity is enough to prove as a theorem, and external parametricity as a metatheorem, that you have an isomorphism up to some appropriate extensional equality. The issue with the term model and its naive (definitional) equality that makes it possible to find these counterexamples with closed terms is that the equality doesn't obey functional extensionality for either $\to$ or $\forall$.

Mike Shulman (Jun 30 2025 at 15:05):

I agree that internal parametricity should imply that $\forall X. ((Q\to X)\to X)$ is isomorphic to $Q$ (extensionally) for the specific $Q = (\forall Y.Y\to Y) \to (\forall Y.Y\to Y)$, for the same reasons HPP gave that it holds in their PER model. However, I don't see how to prove even with internal parametricity that $\forall X. ((A\to X)\to X)$ is isomorphic to $A$ for a variable type $A$.

Mike Shulman (Jun 30 2025 at 16:50):

Ryan Wisnesky said:

here's a claimed agda proof that naturality follows from parametricity for internal functors: https://cs.stackexchange.com/questions/136359/rigorous-proof-that-parametric-polymorphism-implies-naturality-using-parametrici .

The "identity extension lemma" certainly is the key. I can never remember the name of that lemma for some reason, but it's basically what I meant by

Thinking about the proof of naturality from parametricity, I think it only works for functors that are sort of "first-order" or "discrete" so that their parametricity transforms are equality.

However, I don't believe this lemma is true in the generality that's needed. The Agda proof in that CS.SE answer simply assumes the lemma (the field idext), so that doesn't help. Reynolds' paper cited earlier in the answer states the lemma without proof, although it looks like he is not working in a type theory with $\forall$ so I could believe that it is true for him even though he doesn't prove it. The CS.SE answer claims "For System F, identity extension can be proven for types-in-contexts" but I don't see it; how do you deal with the case of $\forall$?

Mike Shulman (Jun 30 2025 at 17:36):

Patrick Nicodemus said:

And certainly the definitional equality thing seems a much stricter requirement, that one doesn't even sound plausible to me, is that even true for functions List A -> List A in Coq?

No, you're right, it's not. Your example shows that it doesn't work for actual inductive lists, but I checked and it also doesn't work for impredicatively defined System-F lists.

So there's no excuse for believing in a CPS isomorphism! (-:

Patrick Nicodemus (Jun 30 2025 at 17:58):

People in this thread are doing a lot of work to try and come up with proofs of these so-called "free theorems". I guess you get what you pay for. In this case the free theorems are false, which I'd say is a fair trade.

Mike Shulman (Jun 30 2025 at 18:02):

I was also tempted to make a comment like that, but I don't think I would go so far as to say that the free theorems are false, only that some of the conclusions people draw from them are. I think normally when people talk about a "free theorem" they mean the parametricity transform of a type, and that should always be true (for closed terms, at least, unless you assume internal parametricity). It just seems that people get overenthusiastic about what you can deduce from it.

Patrick Nicodemus (Jun 30 2025 at 18:04):

Yes, just having fun. Although this thread is reminding me that I don't understand how to interpret the identity extension lemma, does it follow directly from the parametricity transform or not?

Mike Shulman (Jun 30 2025 at 18:16):

I think it has to be proven by a separate induction over type-formers, referring to the definition of the parametricity transform.

Ryan Wisnesky (Jun 30 2025 at 19:41):

we have to do the hard work in this thread so eventual readers of the blog post don't have to :-). I think my next step is still to try to implement the naturality axiom from the Coq development using the argument from Agda, if only to see what goes wrong in the iso proof of a ~ forall x, (a->x)->x for variable a even when you do assume internal parametricity.

Mike Shulman (Jun 30 2025 at 20:04):

Here's the start of an attempted proof of naturality in Narya with its built-in internal parametricity:

{` -*- narya-prog-args: ("-proofgeneral" "-direction" "p,rel,Br") -*- `}

def eq (A : Type) (x : A) : A → Type ≔ data [ rfl. : eq A x x ]

def Gel (A B : Type) (R : A → B → Type) : Br Type A B ≔ sig x y ↦ (
  ungel : R x y )

axiom a : Type

def natural (α : (r : Type) → (a → r) → r) (r0 r1 : Type) (ρ : r0 → r1)
  (f : a → r0)
  : eq r1 (ρ (α r0 f)) (α r1 (x ↦ ρ (f x)))
  ≔ rel α {r0} {r1} (Gel r0 r1 (x y ↦ eq r1 (ρ x) y)) {f} {x ↦ ρ (f x)}
      (x ⤇ (ungel ≔ ?)) .ungel

The type of the hole is

α : (r : Type) → (a → r) → r
r0 : Type
r1 : Type
ρ : r0 → r1
f : a → r0
x.0 : a
x.1 : a
x.2 : Br a x.0 x.1
----------------------------------------------------------------------
eq r1 (ρ (f x.0)) (ρ (f x.1))

and in that context we have in particular

rel ρ (rel f x.2)
  : Br r1 (ρ (f x.0)) (ρ (f x.1))

So it would work if r1 were "discrete" in the sense that its parametricity bridges are just equality (is there a standard name for that property akin to "identity extension lemma"?).

Mike Shulman (Jun 30 2025 at 20:05):

Or if a were discrete, since then we could turn x.2 into an equality and apply ordinary ap.

Evan Cavallo (Jun 30 2025 at 20:39):

Mike Shulman said:

(is there a standard name for that property akin to "identity extension lemma"?

I always just called it being "bridge-discrete". By the way, what you wrote just now (with the a discrete assumption) is more or less what I do in Theorem 10.3.4 in http://reports-archive.adm.cs.cmu.edu/anon/2021/CMU-CS-21-100.pdf.

Mike Shulman (Jun 30 2025 at 21:45):

Ah, fantastic! I should have thought to look back at your thesis before this. If I may graciously quote the most relevant passages from your chapter 10:

In classical parametricity, the identity extension lemma is a key basic result: it says that the relational interpretation of an operator on types takes identity relations to identity relations. In particular, the interpretation of any closed type is the identity relation. In internal parametricity, the corresponding statement would be that any “homogeneous” bridge type Bridge(𝐴, 𝑀0, 𝑀1 )... is isomorphic to Path(𝐴, 𝑀0, 𝑀1 ), the relation Bridge(𝐴, −, −) being the analogue of the relational interpretation of 𝐴. We have just seen that this is false: we have $Bridge(U, 𝐴, 𝐵) \simeq (𝐴 × 𝐵 → U) \not\simeq (𝐴 \simeq 𝐵) \simeq Path(U, 𝐴, 𝐵)$. We can, however, identify the types that do satisfy this property, which we call the bridge-discrete types. We will see that the class of bridge-discrete types is closed under every type former we have introduced except the universe, and that assumptions of bridge-discreteness can effectively play the role of the identity extension lemma.
...
Whenever we want to prove a parametricity result about a type that involves an “external” type parameter, we likely need to assume that parameter is bridge-discrete.
Theorem 10.3.4. For any bridge-discrete 𝐴 type, we have an isomorphism of the follow-
ing type.
$((𝐵 : U) → (𝐴 → 𝐵) → 𝐵) \simeq 𝐴$

Ryan Wisnesky (Jun 30 2025 at 22:35):

so to summarize, "what goes wrong in the iso proof of a ~ forall x, (a->x)->x for variable a even when you do assume internal parametricity" is that you need a bridge discreteness proof (for variable a) too. So then I think my last question is whether or not the hyland type Q (or S etc) is bridge discrete

Mike Shulman (Jun 30 2025 at 22:59):

It better not be!

Ryan Wisnesky (Jul 01 2025 at 00:37):

on second thought, how does one formulate bridge discreteness outside of HoTT? as an axiom populating the hole in the narya development? Or as the identity extension lemma as in the agda development?

Mike Shulman (Jul 01 2025 at 01:11):

No matter what "Id" means, there is a map $\mathsf{Id}_A(x,y) \to \mathsf{Bridge}_A(x,y)$, and you would ask that to be an equivalence.

Mike Shulman (Jul 01 2025 at 01:12):

So that works in any dependent type theory with internal parametricity.

Mike Shulman (Jul 01 2025 at 01:15):

In a simple type theory like System F, internal parametricity doesn't really make sense, and, I guess it would have to be an analogous metatheoretic statement. E.g. for any type $A$ and closed terms $x,y:A$, the parametricity relation $A^P(x,y)$ is true iff $x=y$.

Madeleine Birchfield (Jul 01 2025 at 01:57):

Mike Shulman said:

No matter what "Id" means, there is a map $\mathsf{Id}_A(x,y) \to \mathsf{Bridge}_A(x,y)$, and you would ask that to be an equivalence.

So that works in any dependent type theory with internal parametricity.

Only works for binary internal parametricity.

But for $n$-ary internal parametricity one can instead consider the fibred version which says that the diagonal function $x \mapsto (x, \ldots, \mathrm{refl}_A(x))$ into the fibred bridge type $\sum_{x, \ldots:A} \mathrm{Bridge}_A(x, \ldots)$ is an equivalence of types, and works for arbitrary internal parametricity, even for nullary internal parametricity where the diagonal function is just a function $x \mapsto \mathrm{refl}_A(x):A \to \mathrm{Bridge}_A$.

Madeleine Birchfield (Jul 01 2025 at 02:07):

Alternatively, in $n$-ary internal parametricity, one can define a "walking bridge type" $\mathbb{I}$ as a higher inductive type generated by $n$ point constructors and a bridge constructor dependent on the $n$-point constructors, and say that every type $A$ is bridge-discrete in the sense of being $\mathbb{I}$-null, i.e. localization $L_\mathbb{I}(A)$ of $A$ at $\mathbb{I}$ is equivalent to $A$ itself.

Ryan Wisnesky (Jul 01 2025 at 03:08):

I'm still a little confused about what conclusions to draw about the hyland et al example from this discussion. I understand the system F term model to be externally parametric (right?), but the hyland result gives two closed types that it claims should be isomorphic according to parametricity and shows they are not isomorphic in the term model. So either the term model is not parametric, or a type and its double negation are not isomorphic via system F external parametricty alone (and so there is no failure of parametricity as they claim, we require an additional axiom a la the Narya development for parametricity to imply a type and its double negation are iso ). Am I missing something simple?

Mike Shulman (Jul 01 2025 at 05:57):

The conclusion is that there is a type $Q$ that is not isomorphic to $\forall X. ((Q\to X)\to X)$. (I would not call the latter "double-negation".)

Ryan Wisnesky (Jul 01 2025 at 06:03):

right, but I'm wondering why hyland et al call that a failure of parametricity, if the term model is parametric - were they wrong to think parametricity alone makes the types isomorphic?

James Deikun (Jul 01 2025 at 06:16):

Traditionally I don't know if a model would really be considered "parametric" if it didn't satisfy identity extension.

Evan Cavallo (Jul 01 2025 at 08:14):

From what I quoted before, I think we conclude that HRR would indeed not consider the term model parametric. The opening of the paper gives some indication of what they mean by "parametric" (but also that they are not completely sure what they mean!):

If you are given a model of the polymorphic lambda calculus (or of anything else for that matter), the first question you are likely to ask is "how good is it?" For many programming languages this might translate straight into a technical question about whether the model is fully abstract with respect to some operational semantics. For the strongly normalizing second-order lambda calculus, this particular question degenerates, and becomes simply the problem of characterizing the equational theory of the model. Seen from a slightly different point of view, it is also a question about how close the model you are given is to the term model for the theory. Specifically, how close it is to the term model for the bare theory, with no additional types, and no extra equations between terms. In this case there is, however, another important question that we can ask (even if we cannot yet precisely formulate it): "Are all the polymorphic values parametric?" (cf. [Ray83, Fre89b]).

One rather crude way of measuring this is by examining the interpretations of the polymorphic natural numbers

$\Pi X. [X \to X] \to [X \to X]$

and the polymorphic booleans

$\Pi X. [X \to [X \to X]].$

In a model close to the term model or in a parametric model, one might expect that these interpretations would contain, in some sense, only the closed terms of given type in the calculus. (Indeed Freyd, following Reynolds, has proposed this as part of a series of tests for the inherent parametricity of a model [Fre89b]).

The Freyd citation is to "Structural polymorphism. distributed notes, 1989" which presumably became the paper "Structural polymorphism" (https://www.sciencedirect.com/science/article/pii/030439759390057Z). It's not so easy for me to extract a clear/explicit criterion, but the "continuation" example does make an appearance:

Theorem 4.1. If $\mathbf{B}$ is a well-pointed CCC with pullbacks then, for any $A$ in $\mathbf{B}$, $\forall X.(A \Rightarrow X) \Rightarrow X$ exists and is isomorphic to $A$. As special cases, we obtain: ...

(Note that $\forall X.(A \Rightarrow X) \Rightarrow X$ has a non-obvious meaning here (it is the "binding" of a "structor"); indeed the point seems to be to give $\forall$ a meaning that makes these things true.)

Evan Cavallo (Jul 01 2025 at 08:35):

Ryan Wisnesky said:

so to summarize, "what goes wrong in the iso proof of a ~ forall x, (a->x)->x for variable a even when you do assume internal parametricity" is that you need a bridge discreteness proof (for variable a) too. So then I think my last question is whether or not the hyland type Q (or S etc) is bridge discrete

In internal parametricity, I believe $Q$ in particular is bridge-discrete, since we can show that $\Pi X. X \to X$ is equivalent to the unit type and thus $Q \simeq (1 \to 1) \simeq 1$. But there could be other non-bridge-discrete types.

Whether we can come up with an explicit example depends on the details of the theory and how we phrase things (there is a disconnect with the System F situation because the internally parametric TT's aren't generally impredicative), but we shouldn't be able to prove internally that all types are bridge-discrete unless this is forced by some axiom (such as there is in Nuyts--Vezzosi--Devriese's paper https://dl.acm.org/doi/10.1145/3110276 if I remember correctly).

Speaking for the theory that I worked on with Bob, it's consistent that the lowest universe $\mathcal{U}_0$ contains only bridge-discrete types, but $\mathcal{U}_1$ contains the non-bridge-discrete type $\mathcal{U}_0$. I don't know if say $(\Pi X:\mathcal{U}_1. (\mathcal{U}_0 \to X) \to X) \not\simeq \mathcal{U}_0$ though.

Evan Cavallo (Jul 01 2025 at 09:09):

Hm, actually I'm fairly confident that last inequivalence isn't provable. We can interpret the type theory in an extension with an extra level of parametricity, where for the new level $\mathcal{U}_0$ is bridge-discrete but $\mathcal{U}_1$ is still "bridge-univalent"/"relativistic", and in this theory the equivalence would hold.

That suggests to me that one can't come up with internal counterexamples to the "continuation" equivalence in internal parametricity (though externally we might be able to see they are unprovable).

Mike Shulman (Jul 01 2025 at 19:17):

Evan Cavallo said:

In internal parametricity, I believe $Q$ in particular is bridge-discrete, since we can show that $\Pi X. X \to X$ is equivalent to the unit type and thus $Q \simeq (1 \to 1) \simeq 1$.

Oops, right.

Mike Shulman (Jul 01 2025 at 19:43):

Evan Cavallo said:

Whether we can come up with an explicit example depends on the details of the theory and how we phrase things

Do you mean an explicit example in the lowest universe? Because of course any (relativistic) universe is not bridge-discrete.

Relatedly, is it possible to have "internal parametricity" in a simple type theory like System F? I'm not even sure what that would mean.

Ryan Wisnesky (Jul 01 2025 at 20:00):

so to be clear, the term model of system F does not satisfy identity extension, and so is not considered (fully) parametric by HRR? All this discussion of these subtle points will help write this up, so thanks everyone for continued participation.

Evan Cavallo (Jul 01 2025 at 20:33):

Mike Shulman said:

Do you mean an explicit example in the lowest universe? Because of course any (relativistic) universe is not bridge-discrete.

The choice of universe was part of what I meant by "how we phrase things", but I was also hedging because I don't have the details of every variant of internally parametric type theory in my head :innocent:

Mike Shulman said:

Relatedly, is it possible to have "internal parametricity" in a simple type theory like System F? I'm not even sure what that would mean.

I also don't know!

Ryan Wisnesky (Jul 01 2025 at 23:47):

I can't find many references on how much the term model of system F fails to be parametric. Even though HRR show that a type and its CPS transform type have different numbers of inhabitants in the term model, I can't see how to populate the polymorphic identity type with more than one term in the term model. This implies to me that the identity extension property can fail independently of other "free theorems"... and that the term model is partially parametric. Does that sound right?

Mike Shulman (Jul 02 2025 at 00:07):

I don't know what it means to ask whether a given model is externally parametric. I think of external parametricity as a construction on models, taking a given model to the corresponding relation model, and that works on any model as input.

Mike Shulman (Jul 02 2025 at 00:08):

The way we get free theorems is from initiality of the term model: the relation model of the term model is also a model, so its projection down to the term model has section, assigning to each term a proof of its free theorem.

Mike Shulman (Jul 02 2025 at 00:09):

So perhaps we ought to say that a model is externally parametric if the projection from its relation model has a section. If so, then the term model would always be parametric.

Ryan Wisnesky (Jul 02 2025 at 00:14):

I think there's a contradiction here, perhaps only in terminology, with two votes (HRR, Evan) saying the system F term model is not parametric, and one vote (Mike) saying it is, and I claim the term model is partially parametric, in that there's no extra term in the polymorphic identity type, but there is an extra term in the (HRR Q/S) continuation type... this blog post may have to turn into a research paper to clarify all this

Ryan Wisnesky (Jul 02 2025 at 01:19):

In reading Plotkin et al's classic https://homepages.inf.ed.ac.uk/gdp/publications/Par_Poly.pdf I'm wondering if part of the issue is that "Strachey polymorphism" is stronger than "Reynolds polymorphism" , and there are other definitions of parametricity as well (such as dinaturality), and so the statement that both identity and the HRR continuation of polymorphic identity should be isomorphic could be true in Strachey's sense but not Reynold's sense, and the term model could be Reynolds but not Strachey parametric (I haven't checked)

Mike Shulman (Jul 02 2025 at 01:23):

I'm not sure whether Evan was expressing his own opinion or just clarifying his reading of HRR.

Mike Shulman (Jul 02 2025 at 01:25):

It just seems wrong to me to call $Q\not\cong \forall X. ((Q\to X)\to X)$ a "failure of parametricity", since it seems that such an isomorphism isn't even provable in general from internal parametricity, which seems to me like it should be the strongest sort of parametricity there is.

Ryan Wisnesky (Jul 02 2025 at 01:30):

Indeed, I'd call it a failure of Strachey parametricity (b/c it is true in PER models), but not a failure of Reynolds parametricity (the strongest form of which should be internal parametricity). Although as a matter of good science, I suppose we should check if Q and its CPS are provably equal in Plotkin's logic, in case that logic differs from internal parametricity in a non-obvious way. The plotkin logic does have identity extension as a lemma, but nothing about bridge discreteness (that I can see). (And I'd also like to check that the term model is a model of plotkin's logic, I don't see that proved in their paper)

Ryan Wisnesky (Jul 02 2025 at 04:14):

another possible contradiction: "Q and CPS Q are not iso via internal parametricity" (mike), but also "Q is bridge discrete by internal parametricty" (Evan). I'm not sure how to resolve this

Mike Shulman (Jul 02 2025 at 04:16):

If I said that internal parametricity doesn't imply $Q \cong \mathrm{CPS}(Q)$, I was wrong, Evan corrected it. The point is that internal parametricity (seemingly) doesn't imply $A\cong \mathrm{CPS}(A)$ for all $A$.

Mike Shulman (Jul 02 2025 at 04:16):

The place $Q \cong \mathrm{CPS}(Q)$ fails is in the term model, by the HPP counterexample.

Mike Shulman (Jul 02 2025 at 04:30):

Ryan Wisnesky said:

I'd call it a failure of Strachey parametricity (b/c it is true in PER models)

It seems weird to me to introduce a fancy term like "Strachey parametricity" if it just means "is true in PER models". I don't see how a CPS isomorphism follows even intuitively from Strachey's supposed intuition that "a parametric polymorphic function behaves the same way for all types".

Ryan Wisnesky (Jul 02 2025 at 04:32):

the HRR paper uses a PER argument to show Q and CPS(Q) are iso (starting from P having one element), not a Reynolds argument. The distinction between Strachey and Reynolds comes from Plotkin

Mike Shulman (Jul 02 2025 at 04:34):

Ryan Wisnesky said:

The plotkin logic does have identity extension as a lemma

Without proof!! I really want to see a proof of this written out.

Maybe I'm confused, but I thought that identity extension was the only missing lemma to deduce naturality of all transformations between functors, and hence the CPS isomorphism, from parametricity. (Plotkin-Abadi seem to prove a similar naturality property on p8.) So if identity extension really is a theorem of their logic, it seems to me that the term model can't be a model of that logic, since by the HPP counterexample there is no CPS isomorphism in the term model.

Mike Shulman (Jul 02 2025 at 04:34):

Ryan Wisnesky said:

the HRR paper uses a PER argument to show Q and CPS(Q) are iso (starting from P having one element), not a Reynolds argument. The distinction between Strachey and Reynolds comes from Plotkin

Indeed. What's your point?

Ryan Wisnesky (Jul 02 2025 at 04:40):

I see the HRR counterexample as saying the term model can't be equivalent to a PER model, not that it can't be equivalent to a Reynolds parametric model, at least when I read the conclusion to their paper in isolation. (In which case, I would agree with HRR that parametricity somehow "fails" if we can have Reynolds parametric models where polymorphic identity has one element but Q and CPS(Q) are not iso)

Ryan Wisnesky (Jul 02 2025 at 04:43):

hyland et al

Ryan Wisnesky (Jul 02 2025 at 04:43):

oh, yeah typo

Mike Shulman (Jul 02 2025 at 04:44):

But if Reynolds parametricity implies that $Q\cong \mathrm{CPS}(Q)$, and that isomorphism fails in the term model, then the term model is not Reynolds polymorphic either.

Mike Shulman (Jul 02 2025 at 04:45):

Mike Shulman said:

it seems to me that the term model can't be a model of that logic

This is also intuitive to me, since their logic seems to be roughly the second-order fragment of internal parametricity, and the term model is not a model of internal parametricity either.

Ryan Wisnesky (Jul 02 2025 at 04:48):

heh, I'm still confused since it was also earlier claimed that "System F (and presumably Haskell) satisfies external parametricity as a metatheorem", which I take to mean the term model is reynolds-parametric - is that my misunderstanding?

Ryan Wisnesky (Jul 02 2025 at 04:50):

on a side note, I'm writing this all up as a giant list of "true/false" propositions

Mike Shulman (Jul 02 2025 at 05:34):

What I meant by "external parametricity" is that there's a section of the projection from the relation model. That's certainly true of the term model. But that's not, at least not a priori, the same as being a model of the Plotkin-Abadi logic, which is the notion of parametricity that I was suggesting a moment ago may imply $Q\cong \mathrm{CPS}(Q)$. They're both "Reynolds" in the sense that they refer to relations, but they're at least superficially distinct.

Mike Shulman (Jul 02 2025 at 05:36):

As I said, the Plotkin-Abadi logic looks to me more like a second-order fragment of internal parametricity. In particular, their parametricity schema on p5 quantifies internally over terms $u$, whereas external parametricity is only a statement about closed terms.

Mike Shulman (Jul 02 2025 at 05:44):

Ryan Wisnesky said:

The plotkin logic does have identity extension as a lemma, but nothing about bridge discreteness (that I can see).

Isn't bridge-discreteness the special case of identity extension for a constant type family?

Mike Shulman (Jul 02 2025 at 05:49):

Evan Cavallo said:

Speaking for the theory that I worked on with Bob, it's consistent that the lowest universe $\mathcal{U}_0$ contains only bridge-discrete types

Did you write out a proof of that? It sounds as if that might be a consequence of a metatheorem that any closed term in $\mathcal{U}_0$ is provably bridge-discrete (I guess you would only need "is not provably non-bridge-discrete", but that seems like it would be hard to prove any other way) -- is that what you proved? And if so, I would presume you'd have to prove something about open terms too for the induction to go through, in which case it might be essentially the same as the proof I really want to see of the identity extension lemma for the Plotkin-Abadi logic?

Ryan Wisnesky (Jul 02 2025 at 05:50):

this is helpful; throughout this discussion we've been using different meanings of external parametricity, which I'll try to take into account going forward. So now I would agree it's a mystery how plotkin proved the identity extension lemma if the term model doesn't satisfy it. As for bridge discreteness being a special case of identity extension, that actually answers a question I posed earlier about how to formulate it outside of HoTT (so I'll take your word for it)

Ryan Wisnesky (Jul 02 2025 at 06:01):

it is interesting to note that plotkin's lemma 2, the 'logical relations lemma', has a proof that mentions not using the axiom schema, whereas the identity extension lemma doesn't say that. I'm not sure what to make of that distinction in the current context

Mike Shulman (Jul 02 2025 at 06:16):

Is there a reason you are saying "Plotkin" instead of "Plotkin-Abadi"?

Mike Shulman (Jul 02 2025 at 06:19):

Ryan Wisnesky said:

it is interesting to note that plotkin's lemma 2, the 'logical relations lemma', has a proof that mentions not using the axiom schema, whereas the identity extension lemma doesn't say that. I'm not sure what to make of that distinction in the current context

I think surely the IEL must use the parametricity schema. For instance, we've seen that bridge-discreteness of the HRR type $Q$ depends on knowing that $\forall X. X\to X$ is a singleton, which depends on parametricity.

Ryan Wisnesky (Jul 02 2025 at 06:22):

I just say Plotkin or Hyland because it's shorter than Plotkin Abadi or Hyland et al in this unambiguous context. I liked HRR as an abbreviation because it is shorter still

Ryan Wisnesky (Jul 02 2025 at 06:24):

right, it's lemma 1, the IEL, that does use the axiom schema. But lemma 2, a different lemma, 'the logical relations lemma' notes that lemma 2 doesn't use the axiom schema

Evan Cavallo (Jul 02 2025 at 07:03):

Mike Shulman said:

Evan Cavallo said:

Speaking for the theory that I worked on with Bob, it's consistent that the lowest universe $\mathcal{U}_0$ contains only bridge-discrete types

Did you write out a proof of that? It sounds as if that might be a consequence of a metatheorem that any closed term in $\mathcal{U}_0$ is provably bridge-discrete (I guess you would only need "is not provably non-bridge-discrete", but that seems like it would be hard to prove any other way) -- is that what you proved?

More or less. What I proved (this is in section 10.3 of my thesis) is that the sub-universe of bridge-discrete types in a universe is closed under product, function, path, bridge, Bool, and Gel types. (I believe the Bool argument would work for some reasonable class of inductives.) So for internally parametric type theory with those types, there's an interpretation of the theory in itself that reinterprets the smallest universe as its sub-universe of bridge-discrete types.

Ryan Wisnesky (Jul 02 2025 at 07:14):

plotkin and abadi only mention one model of their calculus, a PER model. so I suppose their calculus may not be sound for the term model, although I thought in some sense a term model "has the most identifications" so this surprises me

Mike Shulman (Jul 02 2025 at 07:22):

A term model has the fewest identifications!

Mike Shulman (Jul 02 2025 at 07:24):

Ryan Wisnesky said:

I just say Plotkin or Hyland because it's shorter than Plotkin Abadi or Hyland et al in this unambiguous context. I liked HRR as an abbreviation because it is shorter still

I'm just uncomfortable with verbally discounting the contributions of all but one author, even if just for convenience. Perhaps PA similarly for Plotkin-Abadi?

Mike Shulman (Jul 02 2025 at 07:31):

@Evan Cavallo Ah, I see. But now I remember again that your theory is not impredicative, so your proof doesn't have to deal with a case corresponding to the $\forall$ of System F.

Ryan Wisnesky (Jul 02 2025 at 08:38):

I found a proposition (axiom C) here https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=ec150da2d4642c5a0eb05986132f725ff91837fe that is true in PERs and Reynolds models but not in the term model. So I think much of my confusion comes from the system F term model being so weak - and I'm not sure why it is so weak compared to term models of equational theories, or the term model of the STLC. (Is the term model for F initial in the category of models for F?) I think my conclusion is that the term model really does have only one term in the polymorphic identity type and also different cardinalities for Q and Cont Q, and this is a failure of the term model to be parametric (which goes against 'haskell is parametric' folklore')

Nathanael Arkor (Jul 02 2025 at 08:48):

So I think much of my confusion comes from the system F term model being so weak

I think this is a funny way of looking at it: given a calculus (such as System F), the term model precisely captures what is derivable in the calculus. If your models satisfy a stronger property than the term model, you have to decide whether you want that property as an axiom of the calculus, or whether the models are too strong. So it doesn't make sense to say that "the term model of System F is too weak". Either the calculus doesn't capture the intuition you desire, or the classical models are not faithful to the calculus.

Josselin Poiret (Jul 02 2025 at 08:50):

Ryan Wisnesky said:

right, it's lemma 1, the IEL, that does use the axiom schema. But lemma 2, a different lemma, 'the logical relations lemma' notes that lemma 2 doesn't use the axiom schema

iirc that lemma is basically just a binary parametricity translation

Josselin Poiret (Jul 02 2025 at 08:58):

Ryan Wisnesky said:

I found a proposition (axiom C) here https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=ec150da2d4642c5a0eb05986132f725ff91837fe

That link doesn't work for some reason

Ryan Wisnesky (Jul 02 2025 at 09:00):

hm, the paper is called "The Genericity Theorem
and the Notion of Parametricity *in the Polymorphic lambda-calculus", December 1992 , by Giuseppe Longo, Kathleen Milsted , Sergei Soloviev

Josselin Poiret (Jul 02 2025 at 09:01):

basically, IEL is a very strong requirement on a model: it needs to have extensional properties, which the term model of system F obviously doesn't have (because we want it to have decidable equality).

Josselin Poiret (Jul 02 2025 at 09:02):

it should be possible to make the notion of equality in the theory of system f extensional though

Ryan Wisnesky (Jul 02 2025 at 09:03):

I also found a paper by Hasegawa, Parametricity of extensionally collapsed term models of polymorphism and their categorical properties, https://link.springer.com/chapter/10.1007/3-540-54415-1_61, that says the closed terms of F are parametric but don't actually form a model; to get that requires "extensional collapse". And so the system F term model includes open terms (according to Hasegawa). As such the system F term model is very different than what I thought it was

Nathanael Arkor (Jul 02 2025 at 09:13):

Term models always include terms in context, rather than just closed terms.

Mike Shulman (Jul 02 2025 at 09:19):

Ryan Wisnesky said:

I think my conclusion is that the term model really does have only one term in the polymorphic identity type and also different cardinalities for Q and Cont Q, and this is a failure of the term model to be parametric

My conclusion is that the term model is externally parametric, but not internally parametric. External parametricity is a metatheoretic statement about syntax, and therefore equivalently about the term model. Internal parametricity is just defining a whole different theory that captures a different intuition, as Nathanael says. And external parametricity suffices to prove there is only one polymorphic identity, but not to prove that Q is isomorphic to Cont Q.

So possibly the central problem with the Haskell folklore is a failure to distinguish between external and internal parametricity. Haskell is externally parametric, but not internally parametric.

Ryan Wisnesky (Jul 02 2025 at 09:20):

Term models of equational theories are made of closed terms, like the term model for 0:nat and S:nat->nat being isomorphic to the natural numbers. but I'd agree that for the case of system f, the only term models that exist use open terms

Mike Shulman (Jul 02 2025 at 09:22):

That's a pretty impoverished term model. The good term model of an equational theory, the one that is initial among finite-product categories containing a model of that theory, has objects that are contexts and morphisms that are open terms, like any other term model.

Nathanael Arkor (Jul 02 2025 at 09:22):

In a model of an equational theory, you must interpret substitution of terms, which is based on terms in context.

Ryan Wisnesky (Jul 02 2025 at 09:34):

hm, both egglog (https://github.com/egraphs-good/egglog) and CQL take equational theories and enumerate the closed terms in order of size to build a model, potentially running forever if no such finite model exists. I was under the impression these were generating initial models? The way "term re-writing an all that" by Baader and nipkow defines things, the term model construction is parametrized by a possibly empty set of variables (which are (usually) taken as empty in egglog and cql). In logic these models of closed terms are called Herbrand models: https://en.wikipedia.org/wiki/Herbrand_structure . Section 8 of these excellent notes use a closed term model of simply typed lambda calculus for an internal language construction: https://www.cl.cam.ac.uk/teaching/1617/L108/catl-notes.pdf . Screenshot of Baader and nipkow:
Screenshot 2025-07-02 at 2.38.12 AM.png

Mike Shulman (Jul 02 2025 at 16:14):

That would be the initial model in a fixed category (like Set), but not initial among models in other categories.

Ryan Wisnesky (Jul 02 2025 at 18:30):

fair enough. I think I'm good; failure of closed terms of system F to form a model at all gives me a good intuition for these negative results about the open term model, and clarifying the difference in terminology re: internal vs external terminology helped a lot too. I'll be writing all this up now, updates to follow

Ryan Wisnesky (Jul 03 2025 at 01:28):

how have people on this thread been formalizing the open term model? hyper-doctrine? locally cartesian closed category? set-theoretically but intuitionistically? something else?

Mike Shulman (Jul 03 2025 at 02:03):

I think there is a fibrational formulation of models of polymorphic type theory in Jacobs' book. Something like that is what I've had in mind.

Ryan Wisnesky (Jul 03 2025 at 02:23):

I'm having trouble tracking down what may be inequivalent definitions of the system F open term model from the various papers mentioned on this thread (may just be an issue of computerized indexing of older papers; but I've never seen this written down), but I think I can proceed by ignoring term models and just focusing on provable equality using beta/eta only, since that seems to be equivalent in places like the HRR conclusion paragraph.

Nathanael Arkor (Jul 03 2025 at 05:33):

There is also a hyperdoctrinal model in Crole's "Categories for Types".