[Haskell-cafe] Re: Monads that are Comonads and the role of Adjunction

[Derek Elkins]

On Mon, 2007-12-17 at 09:58 -0500, David Menendez wrote:
> 
> 
> On Dec 17, 2007 4:34 AM, Yitzchak Gale <gale at sefer.org> wrote:
>         Derek Elkins wrote:
>         > There is another very closely related adjunction that is
>         less often
>         > mentioned.
>         >
>         > ((-)->C)^op -| (-)->C
>         > or
>         > a -> b -> C ~ b -> a -> C 
>         >
>         > This gives rise to the monad,
>         > M a = (a -> C) -> C
>         > this is also exactly the comonad it gives rise to (in the op
>         category
>         > which ends up being the above monad in the "normal"
>         category). 
>         
>         
>         That looks very like the type of mfix. Is this
>         related to MonadFix?
> 
> I think that's the continuation monad.

Let's do some (more) category theory.  The unit of an adjunction (which
is the unit of the monad it gives rise to) is the image of id in the
isomorphism of hom-sets that defines an adjunction.  In this case that
isomorphism is (a -> b -> c) ~ (b -> a -> c), and the type completely
determines the implementation (if you don't immediately recognize it),
the isomorphism (in both ways actually) is flip.  So the unit of the
adjunction (return) is flip id and indeed that is exactly what Cont's
definition of return is.  

(a -> C) is a contravariant functor in a, so
class ContraFunctor f where
    cofmap :: (b -> a) -> f a -> f b

instance ContraFunctor (-> c) where -- not legal
    cofmap f = (. f)
This obviously satisfies the (contravariant) functor laws,
cofmap id = id and cofmap (f . g) = cofmap g . cofmap f

instance Functor M where
    fmap = cofmap . cofmap
This obviously satisfies the functor laws,
fmap id = id and fmap (f . g) = fmap f . fmap g

join is then
join :: M (M a) -> M a
join = cofmap (flip id) -- flip id is also the counit

This implementation is also forced by the types.

(>>=) then has it's standard definition in terms of join and fmap,
m >>= f = join (fmap f m)
and if this is expanded out, this is indeed seen to be the
implementation of (>>=) for the continuation monad.