[Haskell-cafe] Monad laws

[Albert Lai]

Deokhwan Kim <dk at ropas.snu.ac.kr> writes:

> What is the practical meaning of monad laws?
> 
>   1. (return x) >>= f == f x
>   2. m >>= return == m
>   3. (m >>= f) >>= g == m >> (\x -> f x >>= g)

I offer to re-write the laws in do-notation.  (Please view with a
fixed-width (non-proportional) font.)

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
                                     }

I think in this notation everyone sees the laws as plain common sense.
If you do write a monad that doesn't follow some common sense, the
dire consequence (practical or theoretical) is obvious.

Just in case it is still not obvious to somebody...

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.  (To put it into perspective, you hardly notice
yourself breathing, but this only makes the practical meaning of
breathing more profound, not less.)

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.