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\}$)

12more comments