Sebastian Fischer sebf at informatik.uni-kiel.de
Thu Apr 9 05:22:54 EDT 2009

```Hi all,

thanks for pointing me at the Codensity monad and for mentioning the
lift operation! I'll try to sum up what I learned from this thread.

In short:

What I find interesting is

1. you can express the results of monadic computations using
functors that do not themselves support the `>>=` operation. You
only need an equivalent of `return`.

and

2. a variety of *non-*monadic effects (e.g., non-determinism) can be
non-determinism *monad* even if all you have is a non-determinism
*functor*.

Here is the long version:

Because `ContT` makes a monad out of anything with kind `* -> *`, we
`Control.Applicative.WrappedMonad` but defining them from scratch
might be insightful, so let's try.

We could define an instance of `Functor` for `ContT t` as follows.

instance Functor (ContT t)
where
fmap = liftM

But let's see what we get if we inline this definition:

fmap f a
= liftM f a
= a >>= return . f
= ContT (\k -> unContT a (\x -> unContT (return (f x)) k))
= ContT (\k -> unContT a (\x -> unContT (ContT (\$f x)) k))
= ContT (\k -> unContT a (\x -> k (f x)))

That leads to the `Functor` instance described in the first post on
Kan extensions by Edward Kmett.

> instance Functor (ContT t)
>  where
>   fmap f a = ContT (\k -> unContT a (k.f))

instance Applicative (ContT t)
where
pure  = return
(<*>) = ap

If we inline `ap` we get

f <*> a
= f `ap` a
= f >>= \g -> a >>= \x -> return (g x)
= ContT (\k1 -> unContT f (\x1 -> unContT (a >>= \x -> return (x1
x)) k1))
= ...
= ContT (\k -> unContT f (\g -> unContT a (\x -> k (g x))))

So, a direct Applicative` instance would be:

> instance Applicative (ContT t)
>  where
>   pure x  = ContT (\$x)
>   f <*> a = ContT (\k -> unContT f (\g -> unContT a (\x -> k (g x))))

The more interesting bits are conversions between the original and the
lifted types. As mentioned earlier, if `f` is a pointed functor, then
we can convert values of type `ContT f a` to values of type `f a`.

runContT :: Pointed f => ContT f a -> f a
runContT a = unContT a point

Ryan Ingram pointed in the other direction:

> You are missing one important piece of the puzzle for ContT:
>
> ~~~
> lift :: Monad m => m a -> ContT m a
> lift m = ContT \$ \k -> m >>= k
> ~~~
>
> This >>= is the bind from the underlying monad.  Without this
> operation, it's not very useful as a transformer!

That is a fine reason for the *class* declaration of `MonadTrans` to
mention `Monad m` as a constraint for `lift`. But as `ContT t` is a
monad for any `t :: * -> *`, a constraint `Monad t` on the *instance*
declaration for `Monad (ContT t)` is moot. This constraint is not
necessary to define `lift`.

>  where
>   lift m = ContT (m>>=)

Ryan continues:

> Without lift, it's quite difficult to get effects from the
> instance would be just as good replacing with the "free"
> alternative functor:
>
> ~~~
> data MPlus a = Zero | Pure a | Plus (MPlus a) (MPlus a)
> ~~~
>
> and then transforming MPlus into the desired type after runContT;
> it's the embedding of effects via lift that makes ContT useful.

Let's see whether I got your point here. If we have a computation

a :: Monad m => m a

and we have a pointed functor `f`, then we can get the result of the
computation `a` in our functor `f` because `runContT a :: f a`.

If we now have a computation with additional monadic effects (I use
non-determinism as a specific effect, but Edward Kmett shows in his
second post on Kan extensions how to lift other effects like Reader,
State, and IO)

b :: MonadPlus m => m b

then we have two possibilities to express the result using `f` if `f` is
also an alternative functor.

1. If `f` is itself a monad (i.e. an instance of MonadPlus), then
the expression `runContT (lift b)` has type `f b`. (Well, `b`
itself has type `f b`..)

2. If `f` is *not* a monad, we can still get the result of `b` in
our functor `f` (using the `MonadPlus` instance from my previous
mail), because `runContT b` also has type `f b`.

Clearly, `runContT (lift b)` (or `b` itself) and `runContT b` may
behave differently (even if they both (can) have the type `f b`)
because `ContT` 'overwrites' the definition for `>>=` of `f` if `f`
has one. So it depends on the application which of those behaviours is
desired.

Ryan:

> The CPS transfrom in ContT also has the nice property that it makes
> most applications of >>= in the underlying monad be
> right-associative.

Do you have a specific reason to say *most* (rather than *all*) here?
Because if we have a left-associative application of `>>=` in `ContT`,
then we have:

(a >>= f) >>= g
= ContT (\k1 -> unContT (a >>= f) (\x1 -> unContT (g x1) k1))
= ContT (\k1 ->
unContT (ContT (\k2 -> unContT a (\x2 -> unContT (f x2) k2)))
(\x1 -> unContT (g x1) k1)
= ContT (\k1 -> unContT a (\x2 -> unContT (f x2) (\x1 -> unContT (g
x1) k1)))
= ContT (\k1 -> unContT a (\x2 ->
unContT (ContT (\k2 -> unContT (f x2) (\x1 -> unContT (g x1)
k2)))
k1))
= ContT (\k1 -> unContT a (\x2 -> unContT (f x2 >>= g) k1))
= a >>= (\x -> f x >>= g)

Cheers,
Sebastian

```