21
$\begingroup$

In various places it is stated that the continuation monad can simulate all monads in some sense (see for example http://lambda1.jimpryor.net/manipulating_trees_with_monads/)) In particular, in http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.43.8213&rep=rep1&type=pdf it is claimed that

any monad whose unit and extension operations are expressible as purely functional terms can be embedded in a call-by-value language with “composable continuations”.

I was wondering what (Category-theoretic) mathematical content these claims of simulation have, and what precisely they show us about monads and categories in mathematical terms. In what ways is the continuation monad special, mathematically, compared to other monads, if at all? (I seem to remember some connection between the Yoneda embedding and continuations which might be relevant https://golem.ph.utexas.edu/category/2008/01/the_continuation_passing_trans.html, although I don't know)

One other relevant fact might be that the continuation monad is the monad which takes individuals $\alpha$ to the principal ultrafilters containing them (that is it provides the map $\alpha \mapsto (\alpha \rightarrow \omega) \rightarrow \omega$) )


Edit: I have been asked to explain what I mean by the continuation monad. Suppose we have a monad mapping types of the simply typed lambda calculus to types of the simply typed lambda calculus (the relevant types of this calculus are of two kinds: (1) the basic types, (I.e, the type $e$, consisting of individuals and belonging to domain $D_e$; and the type of truth values $\{ \top, \bot\}$ belonging to domain $D_t$) and, (2) for all basic types $\alpha, \beta$, the type of functions between objects of type $\alpha$ and objects of type $\beta$ belonging to domain $D_{\beta}^{D_{\alpha}}$). Let $\alpha, \beta$ denote types and $\rightarrow$ a mapping between types. Let $a : \alpha \hspace{0.2cm}$ (or $b: \beta)$ indicate that $a\hspace{0.2cm}$ (or $b$) is an expression of type $\alpha \hspace{0.2cm}$ (or $\beta)$. Let $\lambda x. t$ denote a function from objects of the type of the variable $x$, to objects of the type of $t$, as in the simply typed lambda calculus. Then a continuation monad is a structure $\thinspace(\mathbb{M}, \eta, ⋆)\thinspace$, with $\mathbb{M}$ an endofunctor on the category of types of the simply typed lambda calculus, $\eta$ the unit (a natural transformation) and ⋆ the binary operation of the monoid) such that:

$$\mathbb{M} \thinspace α = (α → ω) → ω, \hspace{1cm} ∀α$$ $$η(a) = λc. c(a) : \mathbb{M} \thinspace α \hspace{1cm} ∀a : α $$ $$m ⋆ k = λc. m (λa. k(a)(c)): \mathbb{M}\thinspace β \hspace{1cm} ∀m : \mathbb{M}\thinspace α, k : α → \mathbb{M}\thinspace β . $$

The continuation of an expression $a$ is $\eta(a) = (a \rightarrow \omega) \rightarrow \omega$.


Edit 2: let $ \omega$ denote some fixed type, such as the type of truth values (i.e, $\{ \top, \bot\}$)

$\endgroup$
  • 2
    $\begingroup$ This question is possibly more appropriate for cstheory.stackexchange.com $\endgroup$ – Gro-Tsen Apr 19 '18 at 12:08
  • 4
    $\begingroup$ I asked the question here since I thought mathematicians would be more capable of speaking about the relevant mathematical structures relevant to my question. $\endgroup$ – user65526 Apr 19 '18 at 12:49
  • 6
    $\begingroup$ @Gro-Tsen: Questions of the form “What precise mathematical statement lies behind this heuristic statement from computer science [or physics, etc.]?” seem reasonably on topic here — at least, I would expect answers here to be a bit different in outlook/emphasis from answers one would get at TCS. $\endgroup$ – Peter LeFanu Lumsdaine Apr 19 '18 at 13:17
  • 3
    $\begingroup$ "In a category with internal homs $[-,-]$, given an object $S$, the continuation monad is the endofunctor $X\mapsto[[X,S],S]$." ncatlab.org/nlab/show/continuation+monad $\endgroup$ – Oscar Cunningham Apr 19 '18 at 15:53
  • 3
    $\begingroup$ @user65526 That's true, but it might be helpful for mathematicians trying to answer your question (it was helpful for me). $\endgroup$ – Will Sawin Apr 20 '18 at 9:14
4
$\begingroup$

If I understand this paper correctly, the construction in full generality might not really involve the continuation passing monad as such.

It is easy to see that if $M$ is an internal monad and $\omega$ is any $M$-algebra, then there is a natural transformation from $M\alpha$ to $ (\alpha → \omega) → \omega$. Indeed, given an element of $(\alpha\to\omega)$, apply $M$ to obtain an element of $(M\alpha\to M\omega)$, plug in $M\alpha$, and compose with the $M\omega\to \omega$ from the algebra structure. (An internal monad is needed for this to make sense on objects, not just algebras).

However, there is no universal choice of an algebra. Let $U$ be the functor from the category of $M$-algebras to the base category. Hence for any $\alpha$ in the base category and $z$ a monad algebra, $\operatorname{Hom}(\alpha, Uz)$ is a set. Assume that the base category has arbitrary products, so that we can internally raise objects to the power of sets.

The first step is to replace $ (\alpha → Uz) → Uz$ with $Uz^{ \operatorname{Hom}(\alpha,Uz)}$. This is the same in the category of sets, and regardless is formally similar.

Next we want to consider elements of this that depend consistently on $z$. You might think this is impossible because one dependence on $z$ is covariant and the other is contravariant, but apparently this is the perfect situation to apply the categorical notion of an end, which gives the correct consistency condition.

The end of $Uz^{ \operatorname{Hom}(\alpha,Uz)}$ is naturally isomorphic to $M\alpha$.

So in the category of sets the statement is that any monad is isomorphic to the subset of a product of instances of the continuation passing monad consisting of those elements satisfying a certain compatibility condition.

$\endgroup$
  • $\begingroup$ @ Will Sawin Ok, and what about the Yoneda embedding? Does it render the continuation monad somehow more significant mathematically than other monads? $\endgroup$ – user65526 Apr 20 '18 at 23:11
  • $\begingroup$ @user65526 I don't know. I tried to use the Yoneda embedding to embed the category into some category of presheaves and then apply the continuation monad construction to a single universal object but I wasn't able to get it to work. $\endgroup$ – Will Sawin Apr 21 '18 at 5:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.