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