Difference between revisions of "Monad laws"
(→But why should monads obey these laws?: c/e (edit para on similarity to folding)) 
(→But why should monads obey these laws?: remove one incorrect statement added in the previous edit) 

(One intermediate revision by the same user not shown)  
Line 25:  Line 25:  
The last law can be rewritten for clarity as 
The last law can be rewritten for clarity as 

<haskell> 
<haskell> 

−  (m >>= (\x > f x)) >>= g ≡ 
+  (m >>= (\x > f x)) >>= g ≡ 
−  m >>= (\x > f x >>= g) 
+  m >>= (\x > f x >>= g) 
+  </haskell> 

+  or, equally, 

+  <haskell> 

+  (m >>= (\x > f x)) >>= (\y > g y) ≡ 

+  m >>= (\x > f x >>= (\y > g y)) 

</haskell> 
</haskell> 

Line 140:  Line 140:  
have never noticed it. 
have never noticed it. 

−  Associativity of a ''binary'' operator 
+  Associativity of a ''binary'' operator allows for ''any'' number of operands to be combined by applying the binary operator with any arbitrary grouping to get the same welldefined result, just like the result of summing up a list of numbers is fully defined by the binary (+) operator no matter which parenthesization is used (yes, just like in folding a list of any type of monoidal values). 
Whether compilers exploit the laws or not, you still want the laws for 
Whether compilers exploit the laws or not, you still want the laws for 
Latest revision as of 09:42, 9 November 2019
All instances of the Monad typeclass should obey the three monad laws:
Left identity:  return a

>>= f

≡  f a

Right identity:  m

>>= return

≡  m

Associativity:  (m >>= f)

>>= g

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

The last law can be rewritten for clarity as
(m >>= (\x > f x)) >>= g ≡
m >>= (\x > f x >>= g)
or, equally,
(m >>= (\x > f x)) >>= (\y > g y) ≡
m >>= (\x > f x >>= (\y > g y))
Here, p ≡ q simply means that you can replace p with q and viceversa, and the behaviour of your program will not change: p and q are equivalent.
What is the practical meaning of the monad laws?
Let us rewrite the laws in donotation:
Left identity:  do { x′ < return x;
f x′
}

≡  do { f x }
 
Right identity:  do { x < m;
return x
}

≡  do { m }
 
Associativity:  do { y < do { x < m;
f x
}
g y
}

≡  do { x < m;
do { y < f x;
g y
}
}

≡  do { x < m;
y < f x;
g y
}

In this notation the laws appear as plain commonsense transformations of imperative programs.
But why should monads obey these laws?
When we see a program written in a form on the lefthand side, we expect it to do the same thing as the corresponding righthand side; and vice versa. And in practice, people do write like the lengthier lefthand side once in a while. First example: beginners tend to write
skip_and_get = do
unused < getLine
line < getLine
return line
and it would really throw off both beginners and veterans if that did not act like (by right identity)
skip_and_get = do
unused < getLine
getLine
Second example: Next, you go ahead to use skip_and_get:
main = do
answer < skip_and_get
putStrLn answer
The most popular way of comprehending this program is by inlining (whether the compiler does or not is an orthogonal issue):
main = do
answer < do
unused < getLine
getLine
putStrLn answer
and applying associativity so you can pretend it is
main = do
unused < getLine
answer < getLine
putStrLn answer
The associativity law is amazingly pervasive: you have always assumed it, and you have never noticed it.
Associativity of a binary operator allows for any number of operands to be combined by applying the binary operator with any arbitrary grouping to get the same welldefined result, just like the result of summing up a list of numbers is fully defined by the binary (+) operator no matter which parenthesization is used (yes, just like in folding a list of any type of monoidal values).
Whether compilers exploit the laws or not, you still want the laws for your own sake, just so you can avoid pulling your hair for counterintuitive program behaviour that brittlely depends on how many redundant "return"s you insert or how you nest your doblocks.
But it doesn't look exactly like an "associative law"...
Not in this form, no. To see precisely why they're called "identity laws" and an "associative law", you have to change your notation slightly.
The monad composition operator (also known as the Kleisli composition operator) is defined in Control.Monad:
(>=>) :: Monad m => (a > m b) > (b > m c) > a > m c
(m >=> n) x = do
y < m x
n y
Using this operator, the three laws can be expressed like this:
Left identity:  return >=> g

≡  g

Right identity:  f >=> return

≡  f

Associativity:  (f >=> g) >=> h

≡  f >=> (g >=> h)

It's now easy to see that monad composition is an associative operator with left and right identities.
This is a very important way to express the three monad laws, because they are precisely the laws that are required for monads to form a mathematical category. So the monad laws can be summarised in convenient Haiku form:
 Monad axioms:
 Kleisli composition forms
 a category.