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.