Difference between revisions of "Monad laws"

From HaskellWiki
Jump to navigation Jump to search
m (Category Monad)
m (Monad Laws moved to Monad laws)
(No difference)

Revision as of 17:22, 14 October 2006

All instances of the Monad class should obey:

1. return a >>= f  =  f a
2. m >>= return  =  m
3. (m >>= f) >>= g = m >>= (\x -> f x >>= g)

What is the practical meaning of the monad laws?

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

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