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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
