Monad Laws

For a type to be a proper monad, it must satisfy three laws that ensure it behaves consistently and predictably. These laws are mathematical properties that should hold for any monad implementation. See also: Monads Basics, Common Monads, Monad Transformers, Equational Reasoning.

The Three Monad Laws

1. Left Identity

return a >>= f = f a

This law states that if we take a value, wrap it in a monad using return, and then feed it to a function using >>=, the result should be the same as just applying the function directly to the value. For more on return and >>=, see Monads Basics.

Intuition

return is a “neutral” way to inject a value into a monad. It shouldn’t add any computational effect or change the value. So using return and then immediately extracting the value with >>= should be equivalent to not using the monad at all.

Example with Maybe

return 5 >>= (\x -> Just (x + 3))
-- is the same as
(\x -> Just (x + 3)) 5
-- Both evaluate to Just 8

2. Right Identity

m >>= return = m

This law states that if we have a monadic value and we feed its result to return using >>=, we should get back the original monadic value.

Intuition

Since return simply injects a value into the monad without adding any effects, taking a monadic value, extracting its core value, and then reinjecting it with return should give us back what we started with.

Example with List

[1, 2, 3] >>= return
-- is the same as
[1, 2, 3]

3. Associativity

(m >>= f) >>= g = m >>= (\x -> f x >>= g)

This law states that the order of application doesn’t matter when chaining monadic operations. Whether we first apply f to m and then apply g to the result, or we define a new function that applies f and then g, and apply that to m, the result should be the same. See Monads Basics for how this relates to do notation.

Intuition

This ensures that when we chain monadic operations, we can group them however we want without affecting the result. This is essential for building complex computations out of simpler ones in a modular way.

Example with IO

-- These two expressions are equivalent:
(getLine >>= readFile) >>= putStrLn
getLine >>= (\filename -> readFile filename >>= putStrLn)

Verifying the Laws for Specific Monads

Let’s verify the monad laws for a few common monads to better understand them. See Common Monads for more on these types.

Maybe Monad

The Maybe monad is defined as:

instance Monad Maybe where
  return = Just
 
  Nothing >>= _ = Nothing
  (Just x) >>= f = f x

Left Identity

return a >>= f
= Just a >>= f
= f a

Right Identity

m >>= return

For m = Nothing:

Nothing >>= return
= Nothing

For m = Just a:

Just a >>= return
= return a
= Just a

Associativity

(m >>= f) >>= g

For m = Nothing:

(Nothing >>= f) >>= g
= Nothing >>= g
= Nothing
 
Nothing >>= (\x -> f x >>= g)
= Nothing

For m = Just a:

(Just a >>= f) >>= g
= f a >>= g
 
Just a >>= (\x -> f x >>= g)
= (\x -> f x >>= g) a
= f a >>= g

List Monad

The List monad is defined as:

instance Monad [] where
  return x = [x]
  
  xs >>= f = concat (map f xs)

Left Identity

return a >>= f
= [a] >>= f
= concat (map f [a])
= concat [f a]
= f a

Right Identity

xs >>= return
= concat (map return xs)
= concat (map (\x -> [x]) xs)
= concat [[x] | x <- xs]
= xs

Associativity

The proof is more involved, but it relies on the associativity of concat and the distributivity of map over concat.

Why the Monad Laws Matter

The monad laws ensure that:

1. Consistency: Monads behave in a consistent, predictable way
2. Equational Reasoning: We can reason about monadic code using substitution (Equational Reasoning)
3. Refactoring: Code can be refactored without changing behavior
4. Composability: Monadic operations can be composed in any order (Monads Basics)
5. Do-Notation: The translation of do notation relies on these laws (Monads Basics)

Consequences of Breaking the Laws

If a monad implementation breaks these laws:

1. Code using that monad might behave unexpectedly
2. Refactoring could change the behavior of the code
3. The do notation might not work as expected
4. Composition with other monadic operations might be inconsistent

Practical Implications

For do Notation

The translation of do notation to >>= relies on the monad laws. For example:

do
  a <- ma
  b <- mb
  return (a, b)

This translates to:

ma >>= (\a -> 
  mb >>= (\b -> 
    return (a, b)))

The associativity law ensures that this is equivalent to:

(ma >>= (\a -> mb)) >>= (\b -> return (a, b))

For Monad Transformers

Monad transformers combine the effects of multiple monads. The monad laws ensure that these combinations behave reasonably.

For Library Design

When designing a library that uses monads, adhering to the monad laws ensures that users can reason about your library’s behavior and combine it with other monadic code.

Testing the Monad Laws

You can use property-based testing with QuickCheck to verify that your monad implementation satisfies the laws:

import Test.QuickCheck
 
-- For a custom monad MyMonad
prop_leftIdentity :: (Eq (m b), Monad m) => a -> (a -> m b) -> Bool
prop_leftIdentity a f = (return a >>= f) == f a
 
prop_rightIdentity :: (Eq (m a), Monad m) => m a -> Bool
prop_rightIdentity m = (m >>= return) == m
 
prop_associativity :: (Eq (m c), Monad m) => m a -> (a -> m b) -> (b -> m c) -> Bool
prop_associativity m f g = ((m >>= f) >>= g) == (m >>= (\x -> f x >>= g))

Key Points to Remember

1. The three monad laws are left identity, right identity, and associativity
2. These laws ensure consistent and predictable behavior when using monads
3. All proper monad implementations must satisfy these laws
4. The laws are not enforced by the type system - it’s the developer’s responsibility
5. The laws are essential for reasoning about monadic code and for the correct functioning of do notation