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: Continuations and polynomials

Keith Elliott Peterson (Mar 19 2023 at 05:57):

Can I not view a continuation as a polynomial $y^{y^X}$ (a monomial with a monomial as an exponent)?

I'm just checking to dot my i's and cross my t's.

Simon Burton (Mar 19 2023 at 13:34):

Looks good to me. Here's some more i's and t's for you: https://ncatlab.org/nlab/show/cartesian+closed+category

Ryan Wisnesky (Mar 19 2023 at 16:34):

Here's a direct link to ncatlab about the continuation monad that verifies your formula: https://ncatlab.org/nlab/show/continuation+monad

Keith Elliott Peterson (Mar 19 2023 at 20:24):

Ryan Wisnesky said:

Here's a direct link to ncatlab about the continuation monad that verifies your formula: https://ncatlab.org/nlab/show/continuation+monad

The page implies that a continuation as a monad is actually a Dirichlet functor, $S^{S^y}$, hence my apprehension.

Ryan Wisnesky (Mar 19 2023 at 21:12):

Perhaps the apprehension is because there's more to the continuation passing style transformation that just that monad? For example, in addition to the monad operations, there's the callCC operation and some others. You could check the implementation of the CPS monad in haskell at https://hackage.haskell.org/package/mtl-2.3.1/docs/Control-Monad-Cont.html and make all those operations are compatible with what you're doing.

Reid Barton (Mar 20 2023 at 03:18):

It's not a polynomial functor: in a polynomial functor the variable $X$ should appear in the base, like $X^S$.
(Just like in algebra, the function $f(x) = 2^{2^x}$, say, is not a polynomial.)

Spencer Breiner (Mar 20 2023 at 12:09):

Well, $\bf Poly$ has exponentials, so it does make sense to talk about $y^{y^X}$, but it is not the same as the exponential in $\bf Set^{Set}$.

Keith Elliott Peterson (Mar 21 2023 at 02:50):

I'm getting multiple differing answers. :face_with_raised_eyebrow:

Reid Barton (Mar 21 2023 at 04:08):

Maybe your original question was not quite precise enough.

Reid Barton (Mar 21 2023 at 05:12):

What do you mean by "a polynomial"?

Todd Trimble (Mar 21 2023 at 16:54):

Reid is right. It's not a polynomial functor according to the usual definitions. A polynomial functor on Set would be a coproduct of representables, $\sum_{i \in I} \hom(n_i, -)$ where $n_i$ is a set (not necessarily finite), which could also be written $X \mapsto \sum_{i \in I} \hom(n_i, X) = \sum_{i \in I} X^{n_i}$ where $X$ is a set that fits into the "blank" argument. The continuation functor/monad is not that.

Josselin Poiret (Mar 21 2023 at 16:59):

In general, polynomial functors represent "strictly positive" type formers, whose claim to fame includes being able to form inductive types. Here, X ↦ (X → Y → Y) is positive but not strictly positive. As a side note, in type theories with impredicative universes, adding merely positive inductive types has been shown to be inconsistent, but no one really knows if they're consistent when there is no impredicativity (eg. Agda). You might find https://dblp.org/rec/conf/types/0001MS18.html interesting, although I admit I haven't grasped what the inductive type represents, and how it directly relates to continuations.