Personal tools

Monad laws

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
(Why is it an "associative law"?)
(possible half-way point?)
 
(11 intermediate revisions by 5 users not shown)
Line 1: Line 1:
All instances of the [[Monad]] class should obey:
+
All instances of the [[Monad]] typeclass should obey the three '''monad laws''':
   
# "Left identity": <hask> return a >>= f = f a </hask>
+
{|
# "Right identity": <hask> m >>= return = m </hask>
+
|-
# "Associativity": <hask> (m >>= f) >>= g = m >>= (\x -> f x >>= g) </hask>
+
| '''Left identity:'''
  +
| <haskell>return a >>= f</haskell>
  +
| ≡
  +
| <haskell>f a</haskell>
  +
|-
  +
| '''Right identity:'''
  +
| <haskell>m >>= return</haskell>
  +
| ≡
  +
| <haskell>m</haskell>
  +
|-
  +
| '''Associativity:'''
  +
| <haskell>(m >>= f) >>= g</haskell>
  +
| ≡
  +
| <haskell>m >>= (\x -> f x >>= g)</haskell>
  +
|}
  +
  +
Here, ''p'' ≡ ''q'' simply means that you can replace ''p'' with ''q'' and vice-versa, and the behaviour of your program will not change: ''p'' and ''q'' are equivalent.
   
 
== What is the practical meaning of the monad laws? ==
 
== What is the practical meaning of the monad laws? ==
Line 9: Line 9:
 
Let us re-write the laws in do-notation:
 
Let us re-write the laws in do-notation:
   
<haskell>
+
{|
1. do { x' <- return x do { f x
+
|-
; f x' == }
+
| '''Left identity:'''
}
+
| <haskell>
+
do { x' <- return x;
2. do { x <- m == do { m
+
f x'
; return x } }
+
}
+
</haskell>
3. do { y <- do { x <- m do { x <- m
+
|
; f x ; do { y <- f x
+
| <haskell>
} == ; g y
+
do { f x }
; g y }
+
</haskell>
} }
+
|-
+
| '''Right identity:'''
do { x <- m
+
| <haskell>
using 3.14 ; y <- f x
+
do { x <- m;
== ; g y
+
return x
}
+
}
  +
</haskell>
  +
| ≡
  +
| <haskell>
  +
do { m }
  +
</haskell>
  +
|-
  +
| '''Associativity:'''
  +
| <haskell>
  +
do { y <- do { x <- m;
  +
f x
  +
}
  +
g y
  +
}
  +
</haskell>
  +
| ≡
  +
| <haskell>
  +
do { x <- m;
  +
do { y <- f x;
  +
g y
  +
}
  +
}
  +
</haskell>
  +
| ≡
  +
| <haskell>
  +
do { x <- m;
  +
y <- f x;
  +
g y
  +
}
 
</haskell>
 
</haskell>
  +
|}
   
In this notation the laws appear as plain common sense.
+
In this notation the laws appear as plain common-sense transformations of imperative programs.
   
 
== But why should monads obey these laws? ==
 
== But why should monads obey these laws? ==
   
When we see a program written in a form on the LHS, we expect it to do
+
When we see a program written in a form on the left-hand side, we expect it to do
the same thing as the corresponding RHS; and vice versa. And in
+
the same thing as the corresponding right-hand side; and vice versa. And in
practice, people do write like the lengthier LHS once in a while.
+
practice, people do write like the lengthier left-hand side once in a while.
 
First example: beginners tend to write
 
First example: beginners tend to write
   
 
<haskell>
 
<haskell>
skip_and_get = do { unused <- getLine
+
skip_and_get = do
; line <- getLine
+
unused <- getLine
; return line
+
line <- getLine
}
+
return line
 
</haskell>
 
</haskell>
   
 
and it would really throw off both beginners and veterans if that did
 
and it would really throw off both beginners and veterans if that did
not act like (by law #2)
+
not act like (by right identity)
   
 
<haskell>
 
<haskell>
skip_and_get = do { unused <- getLine
+
skip_and_get = do
; getLine
+
unused <- getLine
}
+
getLine
 
</haskell>
 
</haskell>
   
Line 57: Line 58:
   
 
<haskell>
 
<haskell>
main = do { answer <- skip_and_get
+
main = do
; putStrLn answer
+
answer <- skip_and_get
}
+
putStrLn answer
 
</haskell>
 
</haskell>
   
Line 66: Line 67:
   
 
<haskell>
 
<haskell>
main = do { answer <- do { unused <- getLine
+
main = do
; getLine
+
answer <- do
}
+
unused <- getLine
; putStrLn answer
+
getLine
}
+
putStrLn answer
 
</haskell>
 
</haskell>
   
and applying law #3 so you can pretend it is
+
and applying associativity so you can pretend it is
   
 
<haskell>
 
<haskell>
main = do { unused <- getLine
+
main = do
; answer <- getLine
+
unused <- getLine
; putStrLn answer
+
answer <- getLine
}
+
putStrLn answer
 
</haskell>
 
</haskell>
   
Law #3 is amazingly pervasive: you have always assumed it, and you
+
The associativity law is amazingly pervasive: you have always assumed it, and you
 
have never noticed it.
 
have never noticed it.
   
Line 98: Line 99:
 
<haskell>
 
<haskell>
 
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
 
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
m >=> n = \x -> do { y <- m x; n y }
+
(m >=> n) x = do
  +
y <- m x
  +
n y
 
</haskell>
 
</haskell>
   
 
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 = g </hask>
+
{|
# "Right identity": <hask> f >=> return = f </hask>
+
| '''Left identity:'''
# "Associativity": <hask> (f >=> g) >=> h = f >=> (g >=> h) </hask>
+
| <haskell> return >=> g </haskell>
  +
| ≡
  +
| <haskell> g </haskell>
  +
|-
  +
| '''Right identity:'''
  +
| <haskell> f >=> return </haskell>
  +
| ≡
  +
| <haskell> f </haskell>
  +
|-
  +
| '''Associativity:'''
  +
| <haskell> (f >=> g) >=> h </haskell>
  +
| ≡
  +
| <haskell> f >=> (g >=> h) </haskell>
  +
|}
   
 
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.
Line 111: Line 112:
 
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 theory|category]]. So the monad laws can be summarised in convenient Haiku form:
 
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 theory|category]]. So the monad laws can be summarised in convenient Haiku form:
   
<blockquote>
+
:Monad axioms:
Monad axioms:<br/>
+
:Kleisli composition forms
Kleisli composition forms<br/>
+
:a category.
a category.
 
</blockquote>
 
   
 
[[Category:Standard_classes]]
 
[[Category:Standard_classes]]

Latest revision as of 18:00, 5 April 2012

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)

Here, pq simply means that you can replace p with q and vice-versa, and the behaviour of your program will not change: p and q are equivalent.

[edit] 1 What is the practical meaning of the monad laws?

Let us re-write the laws in do-notation:

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 common-sense transformations of imperative programs.

[edit] 2 But why should monads obey these laws?

When we see a program written in a form on the left-hand side, we expect it to do the same thing as the corresponding right-hand side; and vice versa. And in practice, people do write like the lengthier left-hand 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.

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 counter-intuitive program behaviour that brittlely depends on how many redundant "return"s you insert or how you nest your do-blocks.

[edit] 3 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.