Monads as adjunctions

 

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?

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

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.

This is an old thread, but I found the question interesting, so I did some calculations myself. Hopefully Bartosz is still there and might read this..

In fact, the Eilenberg-Moore construction does give a very clear picture in this case. (I will use CWM notation with Haskell like syntax)

Let T be the list monad < T,eta,mu > ( eta = return and mu = concat ) and consider a T-algebra h:T a -> a .

(Note that T a = [a] is a free monoid <[a],[],(++)> , that is, identity [] and multiplication (++) .)

By definition, h must satisfy hT h == h.mu a and h.eta a== id .

Now, some easy diagram chasing proves that h actually induces a monoid structure on a (defined by x*y = h[x,y] ), and that h becomes a monoid homomorphism for this structure.

Conversely, any monoid structure < a,a0,* > defined in Haskell is naturally defined as a T-algebra.

In this way ( h = foldr ( * ) a0 , a function that 'replaces' (:) with (*) ,and maps [] to a0 , the identity).

So, in this case, the category of T-algebras is just the category of monoid structures definable in Haskell, HaskMon.

(Please check that the morphisms in T-algebras are actually monoid homomorphisms.)

It also characterizes lists as universal objects in HaskMon, just like free products in Grp, polynomial rings in CRng, etc.

The adjuction corresponding to the above construction is < F,G,eta,epsilon >

where

  • F:Hask -> HaskMon , which takes a type a to the 'free monoid generated by a ',that is, [a] ,
  • G:HaskMon -> Hask , the forgetful functor (forget the multiplication),
  • eta:1 -> GF , the natural transformation defined by x::a -> [x] ,
  • epsilon: FG -> 1 , the natural transformation defined by the folding function above (the 'canonical surjection' from a free monoid to its quotient monoid)

    • Next, there is another 'Kleisli category' and the corresponding adjunction. You can check that it is just the category of Haskell types with morphisms a -> T b , where its compositions are given by the so-called 'Kleisli composition' (>=>) . A typical Haskell programmer will find this category more familiar.

    Finally,as is illustrated in CWM, the category of T-algebras (resp. Kleisli category) becomes the terminal (resp. initial) object in the category of adjuctions that define the list monad T in a suitable sense.

    I suggest to do a similar calculations for the binary tree functor T a = L a | B (T a) (T a) T a = L a | B (T a) (T a) to check your understanding.

    链接地址: http://www.djcxy.com/p/47690.html

    上一篇: >）Monad的实例和混淆（

    下一篇: Monads作为附件