[Haskell-cafe] Monad laws

[Brian Hulley]

Lennart Augustsson wrote:
> On Sep 7, 2006, at 08:50 , Brian Hulley wrote:
>> Deokhwan Kim wrote:
>>> What is the practical meaning of monad laws?
>> 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
>>
>> which can further be optimized to:
>>
>>    g c = if c then (p >>= (\_ -> q)) else q
>
> 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.

I think at least GHC does, if I understand the -ddump-simpl output below 
properly:

    -- in Monad.hs
    module Main where

    import Control.Monad

    test :: Bool -> IO ()
    test c = do
         if c
              then putStr "True"
              else return ()
         putStrLn "Finish"

    main = test False

ghc --make -O2 -ddump-simpl monad

gives:

==================== Tidy Core ====================
Main.s :: GHC.Base.String
[GlobalId]
[Str: DmdType]
Main.s = GHC.Base.unpackCString# "Finish"

Main.main :: GHC.IOBase.IO ()
[GlobalId]
[Arity 1
 Str: DmdType L]

Main.main = \ (eta_a26L :: GHC.Prim.State# GHC.Prim.RealWorld) ->
       case (# GHC.Prim.State# GHC.Prim.RealWorld, () #) GHC.IO.hPutStr
          GHC.Handle.stdout Main.s eta_a26L
       of wild_a26O { (# new_s_a26M, a85_a26N #) ->
       System.IO.lvl1 new_s_a26M
       }

Main.s1 :: GHC.Base.String
[GlobalId]
[Str: DmdType]
Main.s1 = GHC.Base.unpackCString# "True"

Main.test :: GHC.Base.Bool -> GHC.IOBase.IO ()
[GlobalId]
[Arity 2
 Str: DmdType SL]
Main.test = \ (c_a19p :: GHC.Base.Bool)
       (eta_s27s :: GHC.Prim.State# GHC.Prim.RealWorld) ->
       case (# GHC.Prim.State# GHC.Prim.RealWorld, () #) c_a19p of wild_B1 {
  GHC.Base.False -> Main.main eta_s27s;
  GHC.Base.True ->
    case (# GHC.Prim.State# GHC.Prim.RealWorld, () #) GHC.IO.hPutStr
              GHC.Handle.stdout Main.s1 eta_s27s
    of wild1_a27o { (# new_s_a27m, a85_a27n #) ->
    Main.main new_s_a27m
    }
       }

So when the condition in Main.test is False, the compiler immediately 
executes Main.main eta_s27s which does the putStr "Finish" directly, so the 
return () has been optimized out.

Whether this is because ghc has used the monad laws, or has applied some 
different optimization due to it's knowledge of the built-in IO monad etc I 
don't know.

Even if the compiler is not itself making use of the laws, other parts of 
standard library code might be, and their correctness would therefore also 
depend on something which the compiler can't verify.

It seems a pity that having gone to the trouble of ensuring a monad obeys 
the laws, the compiler can't make use of them. What then *is* the point of 
the monad laws?

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