State monads don't respect the monad laws in Haskell
An interesting revelation just occurred to Simon P.J. and myself while wondering about issues to do with exceptions in the IO monad (see discussion on glasgow-haskell-users@haskell.org if you're interested). The question we were considering was whether the following should hold in the IO monad: (return () >>= \_ -> undefined) `seq` 42 == undefined as we understand the IO monad it certainly shouldn't be the case. But according to the monad laws: (law) return a >>= k == k a so (return () >>= \_ -> undefined) `seq` 42 => ((\_ -> undefined) ()) `seq` 42 => undefined `seq` 42 => undefined So the IO monad in Haskell, at least as we understand it, doesn't satisfy the monad laws (or, depending on your point of view, seq breaks the monad laws). This discrepancy applies to any state monad. Suppose we define return a = \s -> (s, a) m >>= k = \s -> case m s of (s', a) -> k a s' now return a >>= k => \s -> case (return a) s of (s', a') -> k a' s' => \s -> case (s, a) of (s', a') -> k a' s' => \s -> k a s but (\s -> k a s) /= (k a) in Haskell, because seq can tell the difference. What should the report say about this? Cheers, Simon
On Tue, May 14, 2002, Simon Marlow wrote:
An interesting revelation just occurred to Simon P.J. and myself while wondering about issues to do with exceptions in the IO monad (see discussion on glasgow-haskell-users@haskell.org if you're interested).
The question we were considering was whether the following should hold in the IO monad:
(return () >>= \_ -> undefined) `seq` 42 == undefined
as we understand the IO monad it certainly shouldn't be the case. But
Why shouldn't this be the case? It seems kind of obvious.
So the IO monad in Haskell, at least as we understand it, doesn't satisfy the monad laws (or, depending on your point of view, seq breaks the monad laws).
This discrepancy applies to any state monad. Suppose we define
return a = \s -> (s, a) m >>= k = \s -> case m s of (s', a) -> k a s'
now return a >>= k => \s -> case (return a) s of (s', a') -> k a' s' => \s -> case (s, a) of (s', a') -> k a' s' => \s -> k a s
but (\s -> k a s) /= (k a) in Haskell, because seq can tell the difference.
What should the report say about this?
"Changes from Haskell 98: removed the seq primitive." Well, maybe not. But it would be really nice to find an alternative that didn't screw up so many different things. It seems that general cleanliness is more important for understanding programs than being able to use functions in all the same ways as datatypes (yes, I am aware that there are loads of issues regarding this that I don't understand, but the whole seq thing smells really funny. \a->\b->e should really equal \a b->e, \x->f x should equal f, etc. etc. Sometimes it seems as though every rule in Haskell has a list of exceptions relating to seq, and that sucks.) -- Night. An owl flies o'er rooftops. The moon sheds its soft light upon the trees. David Feuer
On Tue, May 14, 2002 at 12:14:02PM +0100, Simon Marlow wrote:
The question we were considering was whether the following should hold in the IO monad:
(return () >>= \_ -> undefined) `seq` 42 == undefined
[as implied by the left-identity monad law]
This discrepancy applies to any state monad.
It also fails for the reader, writer and continuation monads, also thanks to lifted functions and tuples. The right-identity law also fails for these monads: (undefined >>= return) `seq` 42 /= undefined `seq` 42
participants (3)
-
David Feuer -
Ross Paterson -
Simon Marlow