[Haskell-cafe] Monad laws

[Brian Hulley]

Deokhwan Kim wrote:
> What is the practical meaning of monad laws?
>
> (M, return, >>=) is not qualified as a category-theoretical monad, if
> the following laws are not satisfied:
>
>  1. (return x) >>= f == f x
>  2. m >>= return == m
>  3. (m >>= f) >>= g == m >> (\x -> f x >>= g)
>
> But what practical problems can unsatisfying them cause? In other
> words, I wonder if declaring a instance of the Monad class but not
> checking it for monad laws may cause any problems, except for not
> being qualified as a theoretical monad?

Afaiu the monad laws are needed so the compiler can do various 
optimizations, especially in regard to the "do" notation. Consider:

    g c = do
                    if c
                        then p
                        else return ()
                    q

Intuitively, the "else" branch of the "if" statement does nothing 
interesting, but we need to put something there because we can't just leave 
the branch empty, hence the use of (return ()), but thankfully, because of 
the monad laws, the compiler can apply transformations to get rid of it when 
it desugars the "do" notation.

The above is equivalent to:

    g c = (if c then p else return ()) >>= (\_ -> q)

which could be re-written as:

    g c = if c then (p >>= (\_ -> q)) else (return () >>= (\_ -> q))

which can be optimized using monad law 1) to:

    g c = if c then (p >>= (\_ -> q)) else (\_ -> q) ()

which can further be optimized to:

    g c = if c then (p >>= (\_ -> q)) else q

so when the condition (c) is False we don't waste time doing the (return ()) 
action, but go straight to (q).

However if your monad didn't satisfy the laws, the compiler would still 
assume that it did thus leading to a flawed "optimization" ie the compiler 
would throw your program away and substitute it for a different, unrelated, 
program...

Regards, Brian.
-- 
Logic empowers us and Love gives us purpose.
Yet still phantoms restless for eras long past,
congealed in the present in unthought forms,
strive mightily unseen to destroy us.

http://www.metamilk.com