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

[Derek Elkins]

On Sun, 2007-12-16 at 13:49 +0100, apfelmus wrote:
> Dan Weston wrote:
> > newtype O f g a = O (f (g a))   -- Functor composition:  f `O` g
> >
> > instance (Functor f, Functor g) => Functor (O f g) where ...
> > instance Adjunction f g         => Monad   (O g f) where ...
> > instance Adjunction f g         => Comonad (O f g) where ... 
> >
> > class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where
> >   leftAdjunct  :: (f a -> b) -> a -> g b
> >   rightAdjunct :: (a -> g b) -> f a -> b
> > ----------------------------------------------------------
> > 
> > Functors are associative but not generally commutative. Apparently a 
> > Monad is also a Comonad if there exist left (f) and right (g) adjuncts 
> > that commute.
> 
> Yes, but that's only sufficient, not necessary.
> 
> Jules and David already pointed out that while every monad comes from an 
> adjunction, this adjunction usually involves categories different from 
> Hask. So, there are probably no adjoint functors f and g in Hask such that
> 
>    [] ~= g `O` f
> 
> or
> 
> >> data L a = One a | Cons a (L a)   -- non-empty list
> 
>    L ~= g `O` f
> 
> (proof?) Yet, both are monads and the latter is even a comonad.
> 
> Moreover, f and g can only commute if they have the same source and 
> target category (Hask in our case). And even when they don't commute, 
> the resulting monad could still be a comonad, too.
> 
> > My category theory study stopped somewhere between Functor and 
> > Adjunction, but is there any deep magic you can describe here in a 
> > paragraph or two? I feel like I will never get Monad and Comonad until I 
> > understand Adjunction.
> 
> Alas, I wish I could, but I have virtually no clue about adjoint 
> functors myself :)

Learn about representability.  Representability is the core of category
theory.  (Though, of course, it is closely related to adjunctions.)

> I only know the classic example that conjunction and implication
> 
>    f a = (a,S)
>    g b = S -> b
> 
> are adjoint
> 
>    (a,S) -> b  =  a -> (S -> b)
> 
> which is just well-known currying. We get the state monad
> 
>    (g `O` f) a = S -> (S,a)
> 
> and the stream comonad
> 
>    (f `O` f) a = (S, S -> a)
> 
> out of that.

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).