[Haskell-cafe] Monad laws

[Lennart Augustsson]

Brian,

Are you really sure Haskell compilers do that optimization?
I would regard a compiler that does optimizations that are justified  
by laws that the compiler cannot check as broken.

	-- Lennart

On Sep 7, 2006, at 08:50 , Brian Hulley wrote:

> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe