[Haskell-cafe] Monad laws

[Robert Dockins]

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