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

On Mon, 2007-12-17 at 09:58 -0500, David Menendez wrote:

On Dec 17, 2007 4:34 AM, Yitzchak Gale 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.