Saturday, November 08, 2008

From Monoids to Monads

Generalising Monoids



The word 'monad' is derived from the word 'monoid'. The explanation usually given is that there is an analogy between monoids and monads. On the surface, this seems a bit unlikely. The join operation in a monad is supposed to correspond to the binary operator in the monoid, but join is a completely different kind of thing, certainly not a binary operator in any usual sense.

I'm going to make this analogy precise so that it's clear that both monoids and monads are examples of the same construction. In fact, I'm going to write some Haskell code to define monoids and monads in almost exactly the same way. I was surprised to find I could do this because instances of Haskell's Monoid and Monad aren't even the same kind of thing (where I'm using 'kind' in its technical sense). But it can be done.

So let's start thinking about monoids. They are traditionally sets equipped with a special element and a binary operator so that the special element acts as an identity for the binary operator, and where the binary operator is associative. We expect type signatures something like one :: m and mult :: m -> m -> m so that, for example, m (m a b) c == m a (m b c). That's fine as it stands, but it doesn't generalise easily. In particular it'd be nice to generalise this definition to other categories. To do that we need to rephrase the definitions so that they are completely point-free and are written purely as the compositions of arrows.

Let's start by thinking about the rule that says multiplying by the identity on the left should leave a value unchanged. Ie. we want mult one x == x for all x. We already have a problem, it refers to a couple of 'points', both one, the identity, and x the unknown. We can deal with the first one easily, we just replace one with an arrow () -> m. But we also need some plumbing to provide two arguments to the mult function. Rather than belabour the point, I'll just give the full code:


> {-# OPTIONS_GHC -fglasgow-exts #-}

> import Control.Monad
> import Test.QuickCheck

> class Monoid m where
> one :: () -> m
> mult :: (m,m) -> m


The law for multiplication on the left is then given by law1_left == law1_middle and so on:


> law1_left,law1_middle,law1_right :: m -> m
> law1_left = mult . (one <#> id) . lambda
> law1_middle = id
> law1_right = mult . (id <#> one) . rho


The associativity law is then given by law2_left x = law2_right x.


> law2_left,law2_right :: ((m,m),m) -> m
> law2_left = mult . (mult <#> id)
> law2_right = mult . (id <#> mult) . alpha


The left and right hand sides of the laws are now point-free. But in order to do this I've had to write some auxiliary functions:


> lambda :: a -> ((),a)
> lambda x = ((),x)

> rho :: a -> (a,())
> rho x = (x,())

> alpha :: ((a,b),c) -> (a,(b,c))
> alpha ((x,y),z) = (x,(y,z))


I've also used the fact that (,) is a bifunctor, ie. it's a functor in each of its arguments so (,) doesn't just give a way to generate a new type (a,b) from types a and b. It also combines pairs of arrows to make new arrows. I'll call the part of (,) that acts on arrows by the name <#>:


> (<#>) :: (a -> c) -> (b -> d) -> (a, b) -> (c, d)
> (f <#> g) (x,y) = (f x,g y)


Intuitively, f <#> g maps f on the left and g on the right of (a,b)

Try unpacking those definitions to see that we get the usual monoid laws. For example


law2_left ((x,y),z) == mult $ (mult <#> id) ((x,y),z) == mult (mult (x,y),z)
law2_right ((x,y),z) == mult $ (id <#> mult) $ alpha ((x,y),z) == mult (x,mult (y,z))


So we get


mult (mult (x,y),z) == mult (x,mult (y,z))


the usual associativity law.

Now that this definition is point-free it seems we could just carry it over to any category. In fact, we've implicitly done this because we've carried over the definition of a monoid from Set to Hask, the category of Haskell types and total functions. We're so used to treating Hask as a proxy for Set we can forget they are actually different categories. But this definition of a monoid works in both. But what about that lambda, rho and alpha? Well they're easy to define in any Cartesian closed category (CCC). But we don't need all of the features of a CCC to define a monoid, we just need lambda, rho and alpha and some kind of 'product' on the set of objects that also acts like a bifunctor. In fact, there's a bunch of 'obvious' laws that these functions satisfy in a CCC. Any category with these functions satisfying these same laws is called a monoidal category. The above definitions allow us to transfer the definition of a monoid to any such category. For the full definition, see the wikipedia entry.

Anyway, let's check to see if the type Int might be a monoid:


> instance Monoid Int where
> one _ = 1
> mult (a,b) = a*b

> check1 = quickCheck $ \n -> law1_left n == law1_middle (n :: Int)
> check2 = quickCheck $ \n -> law1_left n == law1_right (n :: Int)
> check3 = quickCheck $ \n -> law2_left n == (law2_right n :: Int)


Of course that's no proof, but it gives us some confidence. (Eg. what about large numbers close to 231...?)

Another Category in the World of Haskell



Most people around here will be familiar with how Haskell types and functions form a category Hask in the obvious way. But it's less well known that there is another category lurking in Haskell. Consider the set of all Haskell functors. These are endofunctors, ie. functors Hask→Hask. Between any two functors is the set of natural transformations between those functors. (If f and g are functors, then the polymorphic functions f a -> g a are the natural transformations.) In addition, you can compose natural transformations and the composition is associative. In other words, Haskell functors form a category. (See the appendix for more abstract nonsense relating to this.)

We'll call the category of endofunctors on Hask by the name E. Functors can be composed like so:


> type (f :<*> g) x = f (g x)


It'd be cool if this was a product in the usual categorical sense, but it isn't. There isn't a natural way to map to both f a and g a from f (g a) with the universal property of products. Instead it's a weaker type of product which is still a bifunctor. Here's how it acts on arrows (remembering that in E, arrows are natural transformations):


> (<*>) f g = f. fmap g


(We could also have used fmap g . f.) If you think of f <#> g as making f act on the left and g act on the right, then you can think of f <*> g as making f and g act on the outer and inner containers of a container of containers.

Here's the identity element for this product, the identity functor. It plays a role similar to () in Hask:


> data Id x = Id x deriving Show
> instance Functor Id where
> fmap f (Id x) = Id (f x)


We can now define some familiar looking natural transformations:


> lambda' :: Functor f => f a -> (Id :<*> f) a
> lambda' x = Id x

> rho' :: Functor f => f a -> (f :<*> Id) a
> rho' x = fmap Id x

> alpha' :: f (g (h a)) -> f (g (h a))
> alpha' = id


With these we have turned E into a monoidal category.

(OK, this may be confusing. We're 'multiplying' functors and we have associativity and a left- and right-identity. So functors form a monoid (modulo isomorphism). But that's a distraction, these are not the monoids that you're looking for. See the appendix for more on this.)

So now we can define monoids in this category using almost the same code as above:


> class Functor m => Monoid' m where
> one' :: Id a -> m a
> mult' :: (m :<*> m) a -> m a

> law1_left',law1_middle',law1_right' :: m a -> m a
> law1_left' = mult' . (one' <*> id) . lambda'
> law1_middle' = id
> law1_right' = mult' . (id <*> one') . rho'

> law2_left',law2_right' :: ((m :<*> m) :<*> m) a -> m a
> law2_left' = mult' . (mult' <*> id)
> law2_right' = mult' . (id <*> mult') . alpha'


And here's the punch line. That's precisely a monad, laws 'n' all.

If you want, you can unpack the definitions above and see that they correspond to the usual notion of a monad. We can write code to do the translation:


> data Monad m => TranslateMonad m a = TM { unTM :: m a } deriving (Eq,Show)

> translate :: Monad m => m a -> TranslateMonad m a
> translate x = TM x

> instance (Monad m,Functor m) => Functor (TranslateMonad m) where
> fmap f (TM x) = TM (fmap f x)

> instance (Functor m,Monad m) => Monoid' (TranslateMonad m) where
> one' (Id x) = TM $ return x
> mult' (TM x) = TM $ fmap unTM x >>= id


In other words, any instance of Monad gives an instance of Monoid'. I'll let you write the reverse mapping. We can even check (not prove!) the laws are satisfied by a particular monad by using QuickCheck:


> instance Arbitrary a => Arbitrary (Id a) where
> arbitrary = liftM Id arbitrary

> instance (Monad m,Eq (m a),Arbitrary (m a)) => Arbitrary (TranslateMonad m a) where
> arbitrary = liftM TM arbitrary

> check4 = quickCheck $ \n -> law1_left' n == law1_middle' (n :: TranslateMonad [] Int)
> check5 = quickCheck $ \n -> law1_left' n == law1_right' (n :: TranslateMonad [] Int)
> check6 = quickCheck $ \n -> law2_left' n == (law2_right' n :: TranslateMonad [] Int)


I don't know about you, but I find this mind-blowing. We took a definition of a simple concept, the monoid. We then abstractificated its definition so that it applied to any monoidal category, and in doing so we completely changed the meaning of one and mult. And yet the resulting object, including its laws, are precisely what you need to solve a whole host of problems in algebra and Haskell programming. This is an amazing example of the unreasonable effectiveness of mathematics. The concept might be a little tricky to grasp: monads are like ordinary monoids, but with outer and inner replacing left and right. But the payoff from this is that intuitions about monoids carry over to monads. I hope to say more about this in future episodes.

Appendix



Consider the category, H, with one object, Hask, and whose arrows are the endofunctors on Hask. We've shown how the arrows on this category aren't just a set, they themselves form a category. This makes H a 2-category. A category with one object is a monoid. But this is a 2-category, so we have a 2-monoid. In fact, there are some extra details required to show we have a 2-category. For example, we need to show that composition of arrows (which now form a category, not a set) is a functor (not just a function). That follows from the Interchange Law which I've already talked about. But note that H is a monoid in a completely conventional way, its arrows form a set with a binary operator on them. This is not the structure that corresponds to monads, although it plays a part in constructing them. Also, don't confuse this monoid with the one that appears in a MonadPlus.

Confession



I'm having trouble giving <*> the correct type signature. I think it should be something like (forall x.a x -> c x) -> (forall x.b x -> d x) -> (forall x.a (b x) -> c (d x)). GHC doesn't like it. Can anyone come up with the correct thing? The code still works.

Links


Another account of the same subject, modulo some details.

17 comments:

  1. This works, but it's rather boring:

    (<*>) :: (Functor a, Functor b, Functor c, Functor d) => (a (d x) -> c (d y)) -> (b z -> d x) -> a (b z) -> c (d y)

    ReplyDelete
  2. Monads and monoids are related in many ways. This is one of them, namely that a monad is a monoid object in Cat. Another simple one is that the structure of monoids can be given with a monad (just as with any algebraic structure.) Another is that we can generalize monads from Cat to arbitrary bicategories. Then monoids are special cases of monads, though this isn't terribly interesting.

    I came across another way of characterizing monads several months ago that is interesting. A lax functor from a category into Cat (or presumably any bicategory), is like a normal functor except instead of id = F id and Ff . Fg = F(g . f) we have natural tranformations id -> F id and Ff . Fg -> F(g . f) that satisfy the "obvious" coherence conditions. A monad is then simply a lax functor 1 -> Cat.

    (See Two constructions on lax functors)

    ReplyDelete
  3. In the forth paragraph you wrote:

    mult id x == x

    did you mean?

    mult one x == x

    ReplyDelete
  4. Actually, the connection is immediate. A lax functor from the terminal category into another category is just a monoid object so (of course, this is necessary) this is just a different perspective on the same construction.

    ReplyDelete
  5. this works here:
    (<*>) :: Functor a => (forall x.a x -> c x) -> (forall x.b x -> d x) -> (forall x.a (b x) -> c (d x))
    f <*> g = f . fmap g

    ReplyDelete
  6. Saizan: if I try that I get errors in the definitions of law2_left' and law2_right'

    ReplyDelete
  7. A Haskell newbie question: Is it possible to define extend this futher? I mean, define an algebra over R as a monoid in (R-Vect, tensor, R), a category as a monoid in category of O-graphs, a strict monoidal category as a monoid in Cat and so on?

    ReplyDelete
  8. Actually, monad is a very old word, most notably used by Leibniz.

    ReplyDelete
  9. Kea,

    The mathematical folklore is that this sense of monad is derived from 'monoid' and 'triad' and is independent of older uses.

    ReplyDelete
  10. gie,

    > Is it possible to define extend this futher?

    Depends what you mean by 'this'. For example, this already shows how to do what you want for algebras. But that example is more successful than this. In that post, I really did unify different algebraic structures as a single Haskell object. In this post I just have definitions that are textually similar but represent quite different things in the Haskell universe. I 'm not sure I could construct a single Haskell object that unified all the senses of monoid you describe. I think this should be seen as a pointer to what we might want from future programming languages. OTOH I wouldn't rule it out Haskell completely...

    ReplyDelete
  11. When you write

    m (m a b) c == m a (m b c)

    I think you mean mult, not m.

    ReplyDelete
  12. Apparently the term monad for the categorical thing is due to Jean BĂ©nabou. If he's still around someone could ask him.

    ReplyDelete
  13. With kind polymorphism (supported by UHC), monads and monoids can be written as a single type class.

    http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28248

    ReplyDelete
  14. Re: "A monad is just a monoid in the category of endofunctors, what's the problem?" (seems to be attributed to Wadler)

    Aw crap, now this isn't just a joke to me, it's a meaningful question.

    ReplyDelete
  15. I think "m (m a b) c == m a (m b c)" should be "mult (mult a b) c == mult a (mult b c)" and "law1_left == law1_middle" should be "law1_left x == law1_middle x".

    ReplyDelete
  16. The most general type signature for (<*>) (which works for me) would be

    (<*>) :: (f b -> c) -> (a -> b) -> f a -> c

    ReplyDelete