What's the multiplication in the continuation monad?

Question

Given a set $S$, we get an endofunctor $X \mapsto [[X,S],S]$ on $\mathbf{Set}$. This is called the continuation monad for $S$, so I guess that means it's a monad. There's a natural map $$\eta_X : X \rightarrow [[X,S],S]$$ that assigns each $x \in X$ to the corresponding "evaluator" $\eta_X(x)$. Explicitly this is given by $$\eta_X(x) = (f \mapsto f(x)).$$

Okay, but what's the multiplication? $$\mu_X : [[[[X,S],S],S],S] \rightarrow [[X,S],S]$$

This seems very complicated; just saying the type of $\mu_X$ is difficult: "The function $\mu_X$ is a way of turning (ways of turning ways of turning ways of turning ways of turning elements of $X$ into elements of $S$ into elements of $S$ into elements of $S$ into elements of $S$) into (ways of turning elements ways of turning elements of $X$ into elements of $S$ into elements of $S$)."

Answer 1

Given $f\in [[[[X,S],S],S],S]$ and $g\in [X,S]$, define $\mu_X(f)(g) = f(\eta_{[X,S]}(g))$.

Why is this the right thing to do? Well, the functor $[-,S]$ is (contravariantly) self-adjoint, with the unit equal to the counit (in the opposite category), and the monad $[[-,S],S]$ arises from this adjunction. If you work out what the definition of the monad induced by an adjunction says in this case, you get the formula for the unit map given in your question and the formula for the multiplication given above.

A little searching on this subject led me to this question, where it's pointed out that Hayo Thielecke's PhD thesis "Categorical Structure of Continuation Passing Style" might a relevant reference.

Answer 2

I think it helps to think things through in programming terms first.

So we have $a$ of type $(((X\to S)\to S)\to S)\to S$ and we want to produce something of type $(X\to S)\to S$.

Very well, we start by assuming we have $b$ of type $X\to S$. Now we need to make $S$.

We can get an $S$ either by having an $X$ and applying $b$ or having an $((X\to S)\to S)\to S$ and applying $a$. The former seems to be hopeless, but the latter may be doable -- namely by applying an appropriate $\eta$ to the $b$ we have assumed.

This leads to exactly to the function Alex also quotes: $$ \mu_X(a)(b) = a(\eta_{X\to S}(b)) $$

More operationally, speaking $(X\to S)\to S$ is a sort of weak promise of an $X$: something that will give us an $S$ if we promise it that we can turn an $X$ into an $S$ for it. Computationally, we expect it is something that will either give us an $X$, turn it into an $S$ and return the $S$ it got, or chicken out and just hand us an $S$ that it got in some other sneaky way. (Though there's no guarantee that it will work that way).

$a$ is then a weak promise of a weak promise of an $X$. But we want to be a weak promise of an $X$. So we start running $a$ -- if it throws us an $S$ immediately, then fine; we'll return that too. If $a$ invokes its continuation, it's going to give it a weak promise $a'$, and we can then run $a'$ and get either an $S$ (which we return immediately) or an $X$, which we will feed into our continuation.

Answer 3

This construction should not just apply to the category of sets, but rather to any cartesian closed category. But this puts us in the realm of mathematical logic. We may interpret $X \to S$ as the type of implications from $X$ to $S$. In particular, if $S=0$ is the falsum, you get the negation type $\neg X$. Using this logical interpretation, it is perhaps more easy to motivate the monad structure. The unit is just the usual implication $X \to \neg \neg X$ to the double negation. Notice that we are in constructive logic here.

Now, we can apply $Y \to \neg \neg Y$ to the special case $Y=\neg X$ and obtain $\neg X \to \neg \neg \neg X$. And now we apply $\neg$ on both sides (which is contravariant) to get $\neg \neg \neg \neg X \to \neg \neg X$.

This was only the special case $S=0$, but you can easily write down the same construction for arbitrary $S$; also in a purely category theoretic fashion. This results in the formula given by Alex Kruckman.

Answer 4

A general formula for the continuation monad (C) multiplication natural transformation (mult):

Given a State object S and a result object R we want a map from (C comp C)S = C(C S) = R^(R^(R^(R^S))) to (C S) = R^(R^S), so construct

    u(at S): (R^S) * (R^(R^(R^(R^S)))) -> R = 
    (R^S) * (R^(R^(R^(R^S)))); unit(at R^S) * id; (R^(R^(R^S)) * (R^(R^(R^(R^S))));
    eval; R 

and take its (lambda) transform to get:

    mult(at (C C)S) = \u: R^(R^(R^(R^S))) -> R^(R^S)

Verify that the unit and mult natural transformations make C (like) a monoid:

    (C unit; mult) = (unit C; mult) = id.

Here semi-colon means map composition from left to right: a;b means a followed by b. It is perfectly reasonable to compose an object with a map (or a map with an object) since an object can be interpreted as its corresponding identity map.

A functor name juxtaposed with a natural transformation name is the standard notation for composition of a natural transformation and a functor. So (C unit) transforms C to (C comp C), as does (unit C); mult then transforms (C comp C) to C. Most writers use juxtaposition of functor names to denote functor compostion, thus (C C) = (C comp C) = $(C\circ C)$.

The lambda transform notation:

    given f: f: A*B -> C
    \f : B -> C^A 

The functors (A * - ) and (-^A) are adjoint.