Posted on October 27, 2019

The previous post showed off the flexibility of the continuation monad to represent various effects. As it turns out, it has a deeper relationship with monads in general.

Disclaimer: this is not a monad tutorial. It will not be enlightening if you’re not already familiar with monads. Or even if you are, probably. That’s the joke.

The starting point is the remark that lift for the ContT monad transformer is (>>=), and ContT is really Cont.1 To make that identity most obvious, we define Cont as a type synonym here.

type Cont r a = (a -> r) -> r

lift :: Monad m => m a -> Cont (m r) a
-- Monad m => m a -> (a -> m r) -> m r
lift = (>>=)

As a monad transformer, it is certainly an odd one. On the one hand, Cont (m r) is a monad which doesn’t really care whether m is a monad, or anything at all. On the other hand, lift is (>>=): it directly depends on the full power of a Monad. That contrasts with StateT for example, whose Monad instance uses the transformed monad’s Monad instance, while lift only needs a Functor.

If lift is (>>=), we can also say that (>>=) is lift, suggesting an alternative definition of monads as types that can be “lifted” into Cont, and “unlifted” back, by passing pure as a continuation.

class Monad m where
lift :: m a -> Cont (m r) a
pure :: a -> m a

unlift :: Monad m => Cont (m a) a -> m a
unlift u = u pure

We simply renamed (>>=) in the Monad class, nothing changed otherwise.2 The new monad laws below are also simple reformulations of the usual monad laws in terms of lift and unlift primarily. There’s a bit of work to fix the third law, but no serious difficulties in the process.3

Nevertheless, such renaming opens the door to another point of view, where monads are merely “subsets” of the Cont monad, and we can reframe the monad laws accordingly. They are the same, and yet, they look completely different.

-- Laws for the lift-pure definition of Monad

unlift . lift = id
(lift . unlift) (pureCont x) = pureCont x
(lift . unlift) (lift u >>=? \x -> lift (k x))
= (lift u >>=? \x -> lift (k x))

where the pure and (>>=) of Cont are called pureCont and (>>=?), clarifying that they are defined once for all, independently of the Monad class. That is the key to resolve the apparent circularity in the title.

pureCont :: a -> Cont r a
pureCont a = (\k -> k a)

(>>=?) :: Cont r a -> (a -> Cont r b) -> Cont r b
c >>=? d = (\k -> c (\a -> d a k))

The second and third law have a common structure. An equation (lift . unlift) y = y expresses the fact that y is in the image of lift. If we also assume the first law unlift . lift = id, that says nothing more.

Another interpretation of the monad laws is now apparent: they say that a monad m is defined by an injection lift into a subset of Cont (m r) closed under pureCont and (>>=?). That’s why we can say that, by definition, m is a “submonad” of Cont (m r).4

But with that fact alone, it wouldn’t matter that the codomain of lift is Cont (m r); any monad n would do, as we could unlift the (>>=) of n down to a (>>=) for m. The special thing about Cont here is that (>>=) for m is literally lift.

### A symmetric presentation

To push that idea further, one might propose a more symmetric redefinition of Monad as a pair (lift, unlift):

class Monad m where
lift   :: m a -> Cont (m r) a
unlift :: Cont (m a) a -> m a

The remaining asymmetry in the first type parameter of Cont can also be removed by using the CodensityT monad transformer:

type CodensityT m a = forall r. Cont (m r) a

lift   :: m a -> CodensityT m a
unlift :: CodensityT m a -> m a

That’s certainly fine. I just prefer the simplicity of Cont over CodensityT where we can get away with it.5

In any case, we can then define pure by “unlifting” pureCont:

pure :: Monad m => a -> m a
pure = unlift . pureCont

A small wrinkle with taking unlift as a primitive is that the new laws don’t quite match up to the old laws anymore. For example, for these two laws to be equivalent (remember that lift is (>>=))…

unlift . lift = id

u >>= pure = u

… we really want an extra law to “unfold” unlift, which is its definition in the previous version of Monad.

unlift u = u pure

-- or, without pure
unlift u = u (unlift . pureCont)

It’s also the only sensible implementation: unlift has to apply its argument u, which is a function, to some continuation. The only good choice is pure, and we have to write it into law to prevent other not-so-good choices.6 pure is arguably still a simpler primitive than unlift in practice, because one has to implement pure explicitly anyway.

To sum up, the (lift, unlift) presentation of Monad comes with an extra fourth law to keep unlift in check.

unlift . lift = id
(lift . unlift) (pureCont x) = pureCont x
(lift . unlift) (lift u >>=? \x -> lift (k x))
= (lift u >>=? \x -> lift (k x))

unlift u = u (unlift . pureCont)

### What’s the problem?

The title seems to be making a circular claim, defining monads in terms of monads. But it can really be read backwards in a well-founded manner.

The “continuation monad” is a concrete thing, consisting of a function on types (_ -> m r) -> m r, and two operations pureCont and (>>=?) (which turn out to be essentially function application and function composition respectively).

A “submonad of the continuation monad” is a subset7 of the continuation monad closed under pureCont and (>>=?).

Although “monad” appears in those terms, we are defining them as individual concepts independently of the general notion of “monad”, which can in turn be defined in those terms. Although confusing, the naming is meant to make sense a posteriori, after everything is defined.

That is an example of a representation theorem, where some general structure is reduced to another seemingly more specific one.

Cayley’s theorem says that every group on a carrier a is a subgroup of the group of permutations (bijective functions) a -> a, and the associated injection a -> (a -> a) is exactly the binary operation of the group on a.

The Yoneda lemma says that fmap is an isomorphism between m a and forall r. (a -> r) -> m r for any functor m (into Set).

Here we said that (>>=) is a (split mono) morphism from m a to forall r. (a -> m r) -> m r for any monad m.

## Generalized Cayley representation theorem (Update from 2019-11-02)

As was pointed out to me on reddit, this is indeed an application of the generalized Cayley representation theorem. This connection is studied in detail in the paper Notions of Computations as Monoids, by Exequiel Rivas and Mauro Jaskelioff, JFP 2017. (PDF, extended version)

The paper shows how to view applicative functors, arrows and monads as monoids in different categories, and how useful constructions arise from common abstract concepts such as exponentials, Cayley’s theorem, free monoids. Below is the shortest summary I could make of Cayley’s theorem applied to monads.

Cayley’s theorem generalizes straightforwardly from groups to monoids, and then from monoids (in the category of sets) to monoids in any category with a tensor × (i.e., a monoidal category) and with exponentials8: a monoid m, given by a pair of morphisms mult : m × m -> m and one : 1 -> m, satisfying some conditions, injects into the exponential object (m -> m) by currying the morphism mult as m -> (m -> m).

Then consider that statement in the category of endofunctors on Set, where the tensor × is functor composition. In this category,

• a monoid is a monad, i.e., a pair join : m × m -> m and pure : 1 -> m (where 1 is the identity functor);

• the exponential object (m -> m) is the codensity monad on m (which we’ve been deliberately confusing with Cont throughout the post): CodensityT m a is the set of natural transformations9 between the functor a -> m _ and m.

type CodensityT m a = forall r. (a -> m r) -> m r

1. As before, there will be quite some blur on the distinction between Cont, ContT, and CodensityT.↩︎

2. Assuming we’ve already ditched return for pure.↩︎

3. A proof in Coq that these new laws imply the old ones, just to be sure.↩︎

4. You may be more familiar with notions of “substructure” being refinements of the notion of “subset”, and strictly speaking, m is not a subset of Cont (m r). But it is convenient to generalize “substructure” directly to “anything that injects into a structure”, especially for working in category theory or formalizing those ideas in proof assistants based on type theory, where the set-theoretic notion of “subset” is awkward to express literally.↩︎

5. By defining CodensityT as a type synonym instead of a newtype, we would also run into minor problems with impredicativity and type inference.↩︎

6. I’m not actually sure whether the other laws entail this one.↩︎

7. “Subset” is not defined but I hope you get the idea.↩︎

8. or rather, it is sufficient for m alone to be an exponent, so (m -> m) is defined as an object.↩︎

9. which is not always a set, but we care when it is.↩︎