Difference between revisions of "Monad laws"
(by "3.14"? please clarify) 
m (Replaced `=` and `==` with `≡` where they indicate "identical to".) 

Line 1:  Line 1:  
All instances of the [[Monad]] class should obey: 
All instances of the [[Monad]] class should obey: 

−  # "Left identity": <hask> return a >>= f 
+  # "Left identity": <hask> return a >>= f ≡ f a </hask> 
−  # "Right identity": <hask> m >>= return 
+  # "Right identity": <hask> m >>= return ≡ m </hask> 
−  # "Associativity": <hask> (m >>= f) >>= g 
+  # "Associativity": <hask> (m >>= f) >>= g ≡ m >>= (\x > f x >>= g) </hask> 
+  
== What is the practical meaning of the monad laws? == 
== What is the practical meaning of the monad laws? == 

Line 11:  Line 11:  
<haskell> 
<haskell> 

1. do { x' < return x do { f x 
1. do { x' < return x do { f x 

−  ; f x' 
+  ; f x' ≡ } 
} 
} 

−  2. do { x < m 
+  2. do { x < m ≡ do { m 
; return x } } 
; return x } } 

3. do { y < do { x < m do { x < m 
3. do { y < do { x < m do { x < m 

; f x ; do { y < f x 
; f x ; do { y < f x 

−  } 
+  } ≡ ; g y 
; g y } 
; g y } 

} } 
} } 

Line 25:  Line 25:  
do { x < m 
do { x < m 

; y < f x 
; y < f x 

−  +  ≡ ; g y 

} 
} 

</haskell> 
</haskell> 

Line 103:  Line 103:  
Using this operator, the three laws can be expressed like this: 
Using this operator, the three laws can be expressed like this: 

−  # "Left identity": <hask> return >=> g 
+  # "Left identity": <hask> return >=> g ≡ g </hask> 
−  # "Right identity": <hask> f >=> return 
+  # "Right identity": <hask> f >=> return ≡ f </hask> 
−  # "Associativity": <hask> (f >=> g) >=> h 
+  # "Associativity": <hask> (f >=> g) >=> h ≡ f >=> (g >=> h) </hask> 
It's now easy to see that monad composition is an associative operator with left and right identities. 
It's now easy to see that monad composition is an associative operator with left and right identities. 
Revision as of 11:33, 25 May 2009
All instances of the Monad class should obey:
 "Left identity":
return a >>= f ≡ f a
 "Right identity":
m >>= return ≡ m
 "Associativity":
(m >>= f) >>= g ≡ m >>= (\x > f x >>= g)
What is the practical meaning of the monad laws?
Let us rewrite the laws in donotation:
1. do { x' < return x do { f x
; f x' ≡ }
}
2. do { x < m ≡ do { m
; return x } }
3. do { y < do { x < m do { x < m
; f x ; do { y < f x
} ≡ ; g y
; g y }
} }
do { x < m
; y < f x
≡ ; g y
}
In this notation the laws appear as plain common sense.
But why should monads obey these laws?
When we see a program written in a form on the LHS, we expect it to do the same thing as the corresponding RHS; and vice versa. And in practice, people do write like the lengthier LHS 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 law #2)
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 law #3 so you can pretend it is
main = do { unused < getLine
; answer < getLine
; putStrLn answer
}
Law #3 is amazingly pervasive: you have always assumed it, and you have never noticed it.
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.