This section is not as precise and contains some intuitive thoughts for how to define a monad properly. Usually, your goal is to extend an arbitrary primitive computation f : a -> b in some way. Try to find the "extended type" that describes the extended computation. Here are some examples using some standard monads in Haskell.
In each case, the type on the right side of the a -> gives the right definition for the type of the monad. Thus a State monad has type (state -> (b, state)).
| Monad | Extension of f : a -> b | Comments |
| Maybe | a -> (b union Nothing) | An additional value Nothing is allowed beyond whatever outputs were allowed in the primitive computation. |
| Reader | a -> environment -> b | The computation can depend on the environment, but cannot change the environment (the environment is read-only). |
| Writer | a -> (b, extraOutput) | Extra output (the "log") is produced, but the computation cannot depend on the extra output (the log is write-only)*. |
| State | a -> state -> (b, state) | The computation can depend on both the primitive input a and the state, and the output can yield a new state (both read and write are allowed for the state). |
| List | a -> [b] | The computation may produce any number (0,1,2,...) of values. |
The standard definition of a monad in category theory is as follows.
C1. A monad on a category C is a functor T : C -> C, together with 2 natural transformations η:id -> T and μ:T^2 -> T such that they obey certain "identity" and "associativity" laws:
How does category theory apply to Haskell? The objects of the category are types, and the arrows between two objects (types) a and b are the functions a -> b. (Reference) So, the corresponding definition in Haskell would be as follows. Note that this is not how monads are actually implemented in Haskell; in Haskell, fmap and join are derived from the more primitive bind (>>=) operator. We will discuss the relationship between fmap, join, and bind later.
H1. A monad m induces a type m a for every type a, with the following operations defined on it:The 3 functions fmap, return, join correspond to the category theory T, η, and μ. The laws of monads are then written in Haskell notation as follows. We choose ○ to denote composition rather than the Haskell dot (.) so that it shows up clearer typographically. We place some type annotations as subscripts for clarity.
Laws 3 and 4 correspond to the commutative square which defines a natural transformation between 2 functors F and G:
Laws 5 and 6 correspond to the left and right identity laws (the left diagram in definition C1 above). Law 5 corresponds to going down, then right; law 6 corresponds to going right, then down.
Law 7 is the associative law (the right diagram in definition C1 above). The left side corresponds to going right, then down; the right side corresponds to going down, then right.
When performing calculations with fmap, it is more convenient to use a different notation. We write f# for (fmap f). In this notation, the laws above can be written more compactly:
Now let's consider another definition which reflects how monads are actually implemented in Haskell.
H2. A monad m induces a type m a for every type a, with the following operations defined on it:They must obey the following laws.
Again, we define a more compact notation f* by f*(m) = m >>= f. In this new notation, the laws may be written without explicit arguments such as m and x, and thus appear in a simpler form:
(We'll demonstrate the equivalence for the 2 versions of H2-3. (m >>= f) >>= g = g*(f*(m)) = (g* ○ f*)(m), while m >>= ( \x -> f x >>= g ) = m >>= (\x -> g*(f(x))) = (g* ○ f)*(m).)
Claim: The definitions H1 and H2 are equivalent. To see this, note that both definitions have return in common, so we'll show how to derive fmap and join from >>=, and vica versa.
To define >>= in terms of fmap and join
Given f : a -> m b, we apply the functor fmap to get a map m a -> m (m b), then compose with join to get a map m a -> m b:
Or, in the compact notation:
To define fmap and join in terms of >>=
For fmap: Given a -> b, compose with returnb -> m b to get a map a -> m b, then apply >>= to get a map m a -> m b.
For join: Given m (m a), bind with idm a to get a map m (m a) -> m a.
In the compact notation:
We must also show that the laws for each definition can be derived from the laws for the other.
To derive H1 from H2
We use H2-1' through H2-3' and B1' and B2' to derive H1-1' through H1-7' and A1'.
To derive H2 from H1
We use H1-1' through H1-7' and A1' to derive H2-1' through H2-3' and B1', B2'.
Note that all of the laws of each set were used to derive the laws of the other.
It satisfies a true associative law, and return is a two-sided identity:
These laws are easily verified using the previously stated laws. Using these facts, we may construct the Kleisli category whose objects are the types in Haskell (as before), but an arrow from a to b is defined to be a map a -> m b. Composition in the Kleisli category is >=>. The identity arrow on a in the Kleisli category is the return map sending a -> m a.
A similar construction of the Kleisli category works in any monad over any category. There is an adjunction between the original category and the Kleisli category, and the monad defined by the adjunction is the monad we started with.
The Kleisli category is one extreme of possible categories which produce an adjunction defining a given monad. The other extreme is the category of algebras for a monad (called a T-algebra if the monad has functor T). Reference: Maclane, Categories for the working mathematician, chapter 6.