Monads as adjunctions

Question

I've been reading about monads in category theory. One definition of monads uses a pair of adjoint functors. A monad is defined by a round-trip using those functors. Apparently adjunctions are very important in category theory, but I haven't seen any explanation of Haskell monads in terms of adjoint functors. Has anyone given it a thought?

Answer 1

Edit: Just for fun, I'm going to do this right. Original answer preserved below

The current adjunction code for category-extras now is in the adjunctions package: http://hackage.haskell.org/package/adjunctions

I'm just going to work through the state monad explicitly and simply. This code uses Data.Functor.Compose from the transformers package, but is otherwise self-contained.

An adjunction between f (D -> C) and g (C -> D), written f -| g, can be characterized in a number of ways. We'll use the counit/unit (epsilon/eta) description, which gives two natural transformations (morphisms between functors).

class (Functor f, Functor g) => Adjoint f g where      counit :: f (g a) -> a      unit   :: a -> g (f a) 

Note that the "a" in counit is really the identity functor in C, and the "a" in unit is really the identity functor in D.

We can also recover the hom-set adjunction definition from the counit/unit definition.

phiLeft :: Adjoint f g => (f a -> b) -> (a -> g b) phiLeft f = fmap f . unit  phiRight :: Adjoint f g => (a -> g b) -> (f a -> b) phiRight f = counit . fmap f 

In any case, we can now define a Monad from our unit/counit adjunction like so:

instance Adjoint f g => Monad (Compose g f) where     return x = Compose $ unit x     x >>= f  = Compose . fmap counit . getCompose $ fmap (getCompose . f) x 

Now we can implement the classic adjunction between (a,) and (a ->):

instance Adjoint ((,) a) ((->) a) where     -- counit :: (a,a -> b) -> b     counit (x, f) = f x     -- unit :: b -> (a -> (a,b))     unit x = \y -> (y, x) 

And now a type synonym

type State s = Compose ((->) s) ((,) s) 

And if we load this up in ghci, we can confirm that State is precisely our classic state monad. Note that we can take the opposite composition and get the Costate Comonad (aka the store comonad).

There are a bunch of other adjunctions we can make into monads in this fashion (such as (Bool,) Pair), but they're sort of strange monads. Unfortunately we can't do the adjunctions that induce Reader and Writer directly in Haskell in a pleasant way. We can do Cont, but as copumpkin describes, that requires an adjunction from an opposite category, so it actually uses a different "form" of the "Adjoint" typeclass that reverses some arrows. That form is also implemented in a different module in the adjunctions package.

this material is covered in a different way by Derek Elkins' article in The Monad Reader 13 -- Calculating Monads with Category Theory: http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

Also, Hinze's recent Kan Extensions for Program Optimization paper walks through the construction of the list monad from the adjunction between Mon and Set: http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf

---

Old answer:

Two references.

1) Category-extras delivers, as as always, with a representation of adjunctions and how monads arise from them. As usual, it's good to think with, but pretty light on documentation: http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html

2) -Cafe also delivers with a promising but brief discussion on the role of adjunction. Some of which may help in interpreting category-extras: http://www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html

Answer 2

Derek Elkins was showing me recently over dinner how the Cont Monad arises from composing the (_ -> k) contravariant functor with itself, since it happens to be self-adjoint. That's how you get (a -> k) -> k out of it. Its counit, however, leads to double negation elimination, which can't be written in Haskell.

For some Agda code that illustrates and proves this, please see http://hpaste.org/68257.