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?

回答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

回答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.

回答3:

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 h.T 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) to check your understanding.

回答4:

I've found a standard constructions of adjunct functors for any monad by Eilenberg-Moore, but I'm not sure if it adds any insight to the problem. The second category in the construction is a category of T-algebras. A T algebra adds a "product" to the initial category.

So how would it work for a list monad? The functor in the list monad consists of a type constructor, e.g., Int->[Int] and a mapping of functions (e.g., standard application of map to lists). An algebra adds a mapping from lists to elements. One example would be adding (or multiplying) all the elements of a list of integers. The functor F takes any type, e.g., Int, and maps it into the algebra defined on the lists of Int, where the product is defined by monadic join (or vice versa, join is defined as the product). The forgetful functor G takes an algebra and forgets the product. The pair F, G, of adjoint functors is then used to construct the monad in the usual way.

I must say I'm none the wiser.

回答5:

If you are interested,here's some thoughts of a non-expert on the role of monads and adjunctions in programming languages:

First of all, there exists for a given monad T a unique adjunction to the Kleisli category of T. In Haskell,the use of monads is primarily confined to operations in this category (which is essentially a category of free algebras,no quotients). In fact, all one can do with a Haskell Monad is to compose some Kleisli morphisms of type a->T b through the use of do expressions, (>>=), etc., to create a new morphism. In this context, the role of monads is restricted to just the economy of notation.One exploits associativity of morphisms to be able to write (say) [0,1,2] instead of (Cons 0 (Cons 1 (Cons 2 Nil))), that is, you can write sequence as sequence, not as a tree.

Even the use of IO monads is non essential, for the current Haskell type system is powerful enough to realize data encapsulation (existential types).

This is my answer to your original question, but I'm curious what Haskell experts have to say about this.

On the other hand, as we have noted, there's also a 1-1 correspondence between monads and adjunctions to (T-)algebras. Adjoints, in MacLane's terms, are 'a way to express equivalences of categories.' In a typical setting of adjunctions <F,G>:X->A where F is some sort of 'free algebra generator' and G a 'forgetful functor',the corresponding monad will (through the use of T-algebras) describe how (and when) the algebraic structure of A is constructed on the objects of X.

In the case of Hask and the list monad T, the structure which T introduces is that of monoid,and this can help us to establish properties (including the correctness) of code through algebraic methods that the theory of monoids provides. For example, the function foldr (*) e::[a]->a can readily be seen as an associative operation as long as <a,(*),e> is a monoid, a fact which could be exploited by the compiler to optimize the computation (e.g. by parallelism). Another application is to identify and classify 'recursion patterns' in functional programming using categorical methods in the hope to (partially) dispose of 'the goto of functional programming', Y (the arbitrary recursion combinator).

Apparently, this kind of applications is one of the primary motivations of the creators of Category Theory (MacLane, Eilenberg, etc.), namely, to establish natural equivalence of categories, and transfer a well-known method in one category to another (e.g. homological methods to topological spaces,algebraic methods to programming, etc.). Here, adjoints and monads are indispensable tools to exploit this connection of categories. (Incidentally, the notion of monads (and its dual, comonads) is so general that one can even go so far as to define 'cohomologies' of Haskell types.But I have not given a thought yet.)

As for non-determistic functions you mentioned, I have much less to say... But note that; if an adjunction <F,G>:Hask->A for some category A defines the list monad T, there must be a unique 'comparison functor' K:A->MonHask (the category of monoids definable in Haskell), see CWM. This means, in effect, that your category of interest must be a category of monoids in some restricted form (e.g. it may lack some quotients but not free algebras) in order to define the list monad.

Finally,some remarks:

The binary tree functor I mentioned in my last posting easily generalizes to arbitrary data type T a1 .. an = T1 T11 .. T1m | .... Namely,any data type in Haskell naturally defines a monad (together with the corresponding category of algebras and the Kleisli category), which is just the result of any data constructor in Haskell being total. This is another reason why I consider Haskell's Monad class is not much more than a syntax sugar (which is pretty important in practice,of course).