[Haskell-cafe] Monad laws
Robert Dockins
robdockins at fastmail.fm
Thu Sep 7 09:43:31 EDT 2006
On Sep 7, 2006, at 9:04 AM, Lennart Augustsson wrote:
> 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.
What, like list fusion?
;-)
Although, more seriously, there are a number of "monads" in the
standard libs that don't follow the monad laws (including IO http://
article.gmane.org/gmane.comp.lang.haskell.general/5273 !!).
I can't imagine that any haskell compilers rely on these laws to do
program transformations.
> -- 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
Rob Dockins
Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
-- TMBG
More information about the Haskell-Cafe
mailing list