Software! Math! Data! The blog of R. Sean Bowman
The blog of R. Sean Bowman
February 01 2016

We learned about monoids, we learned the (mathematician’s) definition of a Monad, and now we’re going to take a look at at least one alternative (but equivalent) definition more often used in computer science. This is the Kleisli triple.

Recall our definition of Monad (shortened here). Fixing a category \(\CC\), a monad is triple of a functor \(F\colon \CC\rightarrow \CC\), a natural transformation \(\eta\colon I\rightarrow F\), and a “multiplication map” \(\mu\colon F\times F\rightarrow F\). The properties the monad must satisfy (again, look back at the monoids post if you don’t quite remember) for each \(X\in \CC\) are listed below. Here, \(f\colon A\rightarrow B\) is an arrow in \(\CC\).

  1. \(\mu_X\circ F\mu_X = \mu_X\circ\mu_{FX}\); Associativity of \(\mu\),
  2. \(\mu_X\circ F\eta_X = \mu_X\circ \eta_{FX} = id_{\CC}\); Identity is \(\eta\),
  3. \(\eta\circ f = F(f) \circ \eta\); \(\eta\) commutes with the “monadic” version of an arrow \(f\) of \(\CC\),
  4. \(\mu\circ F(F(f)) = F(f)\circ \mu\); \(\mu\) commutes with \(f\) as long as we apply the monad functor the right number of times.

Examples of Monads in programming languages

In most programming languages, we think of the underlying category as a category of types of the language. The functor \(F\) is usually thought of as a type constructor, or (especially in languages other than Haskell) a parameterized type. The natural transformation \(\mu\) takes a type wrapped in another type, wrapped in the same type again, and turns it into a type wrapped only once. The natural transformation \(\eta\) actually does the wrapping, taking a raw \(X\) value from \(\CC\) and turning it into an \(FX\). In fact, these are usually given the names join and unit (usually called return in Haskell), respectively. Finally, we need the functor \(F\) in order to turn maps \(A\rightarrow B\) in to maps \(FA\rightarrow FB\); this operation of “mapping” \(F\) on to arrows is called fmap.

Small, simple examples

The Maybe monad is perhaps the one I understand the best, so let’s think about this one. Values of type Maybe are either Just a with a some type variable, or Nothing. They can represent null pointers, functions that sometimes don’t return a value, and all sorts of other cool stuff. The transformation \(\eta\) turns a raw value (6, maybe) and into Just 6. Finally, \(\mu\) combines two Maybes into one: \(\mu\) applied to Just (Just 11)) gives Just 11. On the other hand, if we apply it to Just Nothing, we get back Nothing, which is as it should be.

Maybe in Haskell

Here is a short Haskell example of the Maybe monad, basically just restating these rules. The Functor type represents a functor, here named t. The Monad type represents a monad whose underlying functor is t. (Note: these are not the monad types in the standard library, see below.)

class Functor t where
  fmap :: (a -> b) -> t a -> t b

class Functor t => Monad t where
  eta :: a -> (t a)
  mu  :: t (t a) -> (t a)

instance Functor Maybe where
  fmap f (Just x) = Just (f x)
  fmap f Nothing = Nothing

instance Monad Maybe where
  eta x = Just x
  mu (Just (Just x)) = Just x
  mu (Just Nothing) = Nothing

List monad in Haskell

The List monad is another simple monad, allowing us to chain functions that return lists. Here’s a simple implementation.

instance Functor [] where
  fmap f (x:xs) = f x : fmap f xs

instance Monad [] where
  eta x = [x]
  mu = concat

As you can see fmap just maps over a list, \(\eta\) creates a singleton list, and \(\mu\) concatenates a list of lists into one flat list. Again, pretty much what we’d expect.

Kleisli triples

Suppose that \((F, \mu, \eta)\) is a monad over a category \(\CC\). The Kleisli category of \(\CC\) is the category \(\CC_F\) whose objects are just the objects of \(\CC\), but whose arrows are functions \(f\colon A\rightarrow FB\). Composition of morphisms \(f\colon X\rightarrow FY\) and \(g\colon Y\rightarrow FZ\) in \(\CC_F\) is defined by

\[ g\circ_F f = \mu_Z\circ Fg\circ f. \]

The identity morphism is given by the monad unit \(\eta\).

Kleisli triples are usually the setting for programming with monads. As such, their operations have names similar to the ones above: the type constructor is just the functor F itself. As before, return is the natural transformation \(\eta\), and there’s one additional operation, called bind and spelled >>= in Haskell. Bind takes a value of type \(FA\) (a type wrapped in the monad), a function from \(A\) to \(FB\), and returns a type of \(FB\). In other words, bind :: Monad m => m a -> (a -> m b) -> m b. Although it looks a bit weird, we can define it using join and fmap:

(>>=) :: Monad m => m a -> (a -> m b) -> m b
x >>= f = join (fmap f x)

Not too difficult: x has type m a for some monad m, and f has type a -> m b. Applying fmap to f, we get a function of type m a -> m (m b). Applying this function to x, we get back a value whose type is m (m b). But join is exactly the operation of “unwrapping” one of the ms; and we get back a value of type m b. Note that this definition of Kleisli triple (as a type constructor, return, and bind) squares up with the one given by wikipedia above.

In fact, we can recover join from bind, so it doesn’t really matter which sets we give. Traditionally, mathematicians use \(\mu\) and \(\eta\), but programmers use return and >>=.

One reason is that bind can be more convenient for making and chaining calls. Suppose we’re in the Maybe monad and we’d like to apply a function to a value. If the value is Nothing, it makes no sense to apply the function. We could write an if/then expression, or do some pattern matching, but bind makes things much easier:

Nothing  >>= _ = Nothing
(Just x) >>= f = f x

We don’t have to worry about cases or anything, and these can be chained together. If some computation returns Nothing, no more functions will be called, and the result of the entire computation will be Nothing. A simple example:

f x = if x >= 0 then Just (x*x*x  - 13x + 12) else Nothing
g x = if x >= 0 then Just (2*x - 20) else Nothing

Just 4 >>= f >>= g    -- evaluates to Just 28
Just (-1) >>= f >>= g -- Nothing (f returns Nothing)
Just 2 >>= f >> g     -- Nothing (g returns Nothing; f(2) < 0)

Similarly, the List monad can be used for chaining computations that produce more than one result. Sometimes this is seen as “nondeterministic” computing. An example:

s x = [x*x + 1, 2*x - 3, x]
t x = [x*x*x - 1, 1 - x]

[1] >>= s >>= t -- evaluates to [7, -1, -2, 2, 0, 0]
-- because, for example, the head of s(1) is 2 and
-- the head of t(2) is 7.  The second element of t(2)
-- is -1, which is the second entry in the above list.

Approx. 1210 words, plus code