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