[Haskell-cafe] Monad laws
Lennart Augustsson
lennart at augustsson.net
Thu Sep 7 09:04:42 EDT 2006
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
More information about the Haskell-Cafe
mailing list