
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 lifted to this "monad for free", so you get, e.g., a 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 also get instances for `Functor` and `Applicative` for free. We could use the `Monad` instance to get them for free by `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))
We also get an Applicative instance for free: 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`.
instance MonadTrans ContT where lift m = ContT (m>>=)
Ryan continues:
Without lift, it's quite difficult to get effects from the underlying Applicative *into* ContT. Similarily, your MonadPlus 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