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: algebras for the continuation monad

fosco (Dec 12 2021 at 15:32):

I was wondering what are the algebras for the continuation monad $X\mapsto B^{B^X}$. Google does not seem to help almost at all, apart from the cryptic sentence here

image.png

I am surprised that the algebras for such a well-known monad are so mysterious to find. Can you tell me more?

My motivation was: find a meaning for algebras, free algebras, and Kleisli composition in the Kleisli category. Understand better the relation between a continuation monad and a two-player game. In case you have information about this as well, feel free to answer!

Jules Hedges (Dec 12 2021 at 17:46):

I have a folklore-y belief from functional programming that virtually nothing is known about general algebras. And a distant memory of a conversation I had with Martín Escardó like 7 years ago when he told me the same, although don't take my word for that

Jules Hedges (Dec 12 2021 at 17:53):

Here https://twitter.com/johncarlosbaez/status/1113951766071074816?s=21 John claims that the EM category of $\mathcal K_2$ is exactly $\mathbf{Set}^{op}$

@CreeepyJoe ... and the Eilenberg-Moore category of the monad hom(hom(-,2),2)): Set -> Set is Set^op! BWAHAHAHA! :smiling_devil:

- John Carlos Baez (@johncarlosbaez)

fosco (Dec 12 2021 at 19:57):

Well, yes, I agree with that; but what is the category of algebras for a generic $B$?

Keith Elliott Peterson (Dec 15 2021 at 01:40):

Jules Hedges said:

Here https://twitter.com/johncarlosbaez/status/1113951766071074816?s=21 John claims that the EM category of $\mathcal K_2$ is exactly $\mathbf{Set}^{op}$

What is meant by 'is exactly' exactly?

Also, I'm having flashbacks from learning about the ultrafilter monad.

Jules Hedges (Dec 15 2021 at 11:30):

Keith Peterson said:

What is meant by 'is exactly' exactly?

By default (ie. when I haven't actually thought about it) I use "is" to mean equivalence of categories

Jules Hedges (Dec 15 2021 at 11:31):

I'd guess it's probably an isomorphism of categories

Nathaniel Virgo (Dec 15 2021 at 12:42):

What are the unit and multipilcation of this monad?

Jules Hedges (Dec 15 2021 at 13:14):

The unit $\eta : X \to (X \to R) \to R$ is $\eta (x) (k) = k (x)$, the multiplication is....... a bit complicated, but if you do type directed programming it's the thing that you find

Jules Hedges (Dec 15 2021 at 13:15):

Multiplication has type $\mu : ((((X \to R) \to R) \to R) \to R) \to (X \to R) \to R$

Jules Hedges (Dec 15 2021 at 13:18):

You get given $\phi : ((X \to R) \to R) \to R$ and $k : X \to R$. You want to get an $R$ which you can get by producing an input to $\phi$, of type $((X \to R) \to R) \to R$

Jules Hedges (Dec 15 2021 at 13:19):

We can build such a thing as the function that, given an input $f : (X \to R) \to R$, return $f (k)$

Jules Hedges (Dec 15 2021 at 13:20):

So in summary, $\mu (\phi) (k) = \phi (\lambda f . f (k))$

Jules Hedges (Dec 15 2021 at 13:23):

This is the goto tool (pun somewhat intended) in typed functional programming when you want to do evil control flow shenanigans and make people's brains explode

Nathaniel Virgo (Dec 15 2021 at 13:25):

Thanks!

Jules Hedges (Dec 15 2021 at 13:27):

Exercise for the reader with half an hour on their hands: it's much less well known that $\mathcal J_R : X \mapsto (X \to R) \to X$ is also a monad, called the selection monad (discovered by Martín Escardó). It's generally similar but its multiplication operator is much more complicated; derive it by the same method of type directed programming

Jules Hedges (Dec 15 2021 at 13:29):

(This is an example of an exercise that you could, in theory, give to 1st year students as soon as they learn the natural deduction calculus rules for purely implicational intuitionistic logic; but you shouldn't, because it's deceptively outrageously difficult)

fosco (Dec 16 2021 at 07:57):

Nathaniel Virgo said:

What are the unit and multipilcation of this monad?

Yet, proving that this is a monad in fact can be done the slick way: it's the monad induced by the adjunction

$[-,B] :{\cal C}^{op} \leftrightarrows {\cal C} : [-,B]$

;-)

Keith Elliott Peterson (Dec 17 2021 at 05:40):

Jules Hedges said:

I'd guess it's probably an isomorphism of categories

Why would you guess that?

Martti Karvonen (Dec 17 2021 at 09:36):

I'm not Jules, but let me take a stab: if "the category $C^T$ of algebras of $T$ is $D$" is taken to mean that $C^T$ and $D$ are equivalent, then "the category $C^T$ of algebras of $T$ is exactly $D$" should say something stronger (otherwise, why add the word "exactly"?). A reasonable reading then is that the statement asserts that $C^T$ and $D$ are isomorphic. Of course, one might interpret both statements in a stricter sense (so that these claims assert an isomorphism and an equality respectively) or something else (e.g. an equivalence and an equality), but these seem less likely.

Mike Shulman (Dec 17 2021 at 14:37):

I don't think "is exactly" necessarily implies anything stronger than "is". I would probably read it as just indicating some emphasis or surprise.

Plus, in this particular case, I think the categories are actually only equivalent.

Martti Karvonen (Dec 17 2021 at 15:40):

In retrospect, I agree that it's not a necessity: it's just _a_ reasonable interpretation

fosco (Dec 18 2021 at 09:59):

fwiw I think "exactly" in the sentence a is exactly b was meant to indicate the fact that we know a non-tautological description for a that makes use of b, and wow, they reduce into each other in some abstract rewriting system! In this sense, the category of sheaves on a space is exactly the category of certain continuous maps over said space, and 2+2 is exactly 4; exactness is contextual, to avoid going crazy in the rabbit-hle of when two things are the same.

But let's go back to the category theory now: a few thoughts

Maybe using the adjunction that generates the continuation monad one could argue that an algebra map $a : B^{B^A} \to A$ is an endomorphism of $B^A$ in the opposite category where the monad is defined, such that something happens. Can one extract some more information from this description, or it is bound to be tautological?

Also, another question: let $T_B$ be the continuation monad on $B$, $A\mapsto B^{B^A}$. Then, we all agree that the cat of $T_2$-algebras is the opposite of $\bf Set$. Is it true that if $H$ is an Heyting algebra, the category of $T_H$-algebras is the opposite of the topos of sheaves with $H$ as subobject classifier?

fosco (Dec 18 2021 at 10:00):

If true, this is certainly something more than we knew few days ago.

Todd Trimble (Dec 26 2021 at 20:24):

(Saw this while going through a huge pile of unread posts.)

In the case of $\mathsf{Set}$, taking $B$ to have cardinality greater than 1, in every case the category of algebras is equivalent to $\mathsf{Set}^{op}$, i.e., $[-, B]: \mathsf{Set}^{op} \to \mathsf{Set}$ is monadic.

It's already been pointed out that this has a left adjoint, namely $[-, B]^{op}: \mathsf{Set} \to \mathsf{Set}^{op}$. By the crude monadicity theorem, it suffices to check that $[-, B]$ reflects isomorphisms and preserves reflexive coequalizers.

We know $[-, 2]: \mathsf{Set}^{op} \to \mathsf{Set}$ preserves reflexive coequalizers -- that's a special case of how Paré proved his theorem that for a topos $E$, that $[-, \Omega]: E^{op} \to E$ preserves reflexive coequalizers. Also, for any set $P$, we know that $P \times -: \mathsf{Set} \to \mathsf{Set}$ preserves connected limits and in particular equalizers. Therefore, $[-, 2^P]: \mathsf{Set}^{op} \to \mathsf{Set}$, being isomorphic to a composite

$\mathsf{Set}^{op} \stackrel{(P \times -)^{op}}{\to} \mathsf{Set}^{op} \stackrel{[-, 2]}{\to} \mathsf{Set}$

of functors that preserve reflexive coequalizers, also preserves reflexive coequalizers. Then $[-, B]$, being a retract of a functor $[-, 2^B]$ that preserves reflexive coequalizers, must also preserve reflexive coequalizers.

Isomorphisms in $\mathsf{Set}$ are epi-monos, so to see that $[-, B]$ reflects isomorphisms, it suffices that it reflects epis and monos. For that, it suffices that $[-, B]$ is faithful, or in other words that $B$ is a cogenerator. But this in turn follows from the fact that $2$ is a cogenerator and there is a monomorphism $2 \to B$.

fosco (Dec 27 2021 at 09:17):

Todd, this is very neat, thanks for taking the time to share it from your email :-)
What surprised me the most about this is that the algebras are the same for every $B$ of cardinality $>2$.

Todd Trimble (Dec 27 2021 at 11:29):

You're welcome! Of course, one would also like a more intuitive understanding as well. That shouldn't be too hard to cook up.

Seemingly related is the fact that $[, V]: \mathsf{Vect}^{op} \to \mathsf{Vect}$ is also monadic for any non-zero vector space $V$. This fact came up around the time Tom Leinster was writing his series of articles about ultrafilters and measures. Again, what is crucial is the fact that such $V$ is an injective cogenerator; see here.

What this also reminds me of is the fact that there are many Lawvere theories whose models are Boolean algebras. The usual Lawvere theory is opposite to the category of finitely generated free Boolean algebras, which by a baby version of Stone duality may be identified with the category of finite sets of cardinality $2^n$. But now here comes a nice trick: if $T$ is any category with finite products, and $\bar{T}$ is its Cauchy completion, then $\bar{T}$ also has finite products, and moreover the category of product-preserving functors $T \to \mathsf{Set}$ is equivalent to the category of product-preserving functors $\bar{T} \to \mathsf{Set}$. For example, the Cauchy completion of finite sets of cardinality $2^n$ is the category $\mathrm{Fin}_+$ of nonempty finite sets. But then, the same is true if we start instead with finite sets of cardinality of $3^n$! It follows that if we take our Lawvere theory to be $\mathrm{Fin}_{3^\bullet}$, then we get the same category of algebras, i.e., Boolean algebras!

That may seem a little weird. It shows that there are many "underlying set" functors $U: \mathrm{Bool} \to \mathsf{Set}$. But it makes a little more sense if you consider that the number of chains $x \leq y$ in a Boolean algebra with $2^n$ elements is $3^n$. Circling back around then to the top of this post, I propose that if we think of $\mathsf{Set}^{op}$ as the category of complete atomic Boolean algebras, then the functor $[-, 3]: \mathsf{Set}^{op} \to \mathsf{Set}$ sends a CABA = power set $P(X)$ to the set of 2-fold chains $a \leq b$ in $P(X)$. (Well, that's one way of thinking about it; there are others.)

Jules Hedges (Dec 29 2021 at 15:51):

Wow!

Jules Hedges (Dec 29 2021 at 15:52):

I wonder, was this really an open question, or is it "known" but just not well known

Jules Hedges (Dec 29 2021 at 15:53):

May I propose that someone writes this down somewhere more permanent than here (for example an nCafe post)?

Todd Trimble (Dec 29 2021 at 15:55):

(Thanks!) I think it's known to certain people like Lawvere. Certainly a conversation he had with me exerted an influence. I'd bet @Tom Leinster knows it on some level as well, and he may have written something like this down himself.

Todd Trimble (Dec 29 2021 at 16:08):

For example, Tom wrote this Cafe post, linking to this section in an nLab article. And definitely check out this other Cafe post, as well as his paper.

Jules Hedges (Dec 29 2021 at 16:13):

I wonder, if you squint enough, if this (namely that $\mathbf{Set}^{op}$ is "backwards") "explains" why $K_R$ is the "monad for the side effect of really gnarly control flow shenanigans"