Re: State monads don't respect the monad laws in Haskell
Simon Marlow wrote [snip]
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). [snip]
Cheers Simon. One of the awkward things about the Haskell events I implemented is that although I make them an instance of Monad, they don't actually satisfy left identity. Now I can say that "Yes, Event isn't really a Monad, but neither is IO". According to the report
Instances of Monad should satisfy the following laws:
return a >>= k = k a m >>= return = m m >>= (\x -> k x >>= h) = (m >>= k) >>= h so neither IO nor my events satisfy this. Up to now I haven't had any problems with this.
Does GHC or any other Haskell compiler actually rely on instances of Monad satisfying left identity? If not, I would suggest dropping the requirement, if it can be done without upsetting category theorists. (What the hell, they stole the term "Monad" from philosophy and changed its meaning, so why shouldn't we?) I presume it would not in fact be difficult to synthesise a left identity at the cost of making things slower, thus (forgive any syntax errors, I'm not going to test this). data MonadIO a = Action (IO a) | Return a instance Monad (MonadIO a) where return a = Return a (>>=) (Return a) k = k a (>>=) (Action act) f = Action (act >>= (\ a -> case f a of {Return a -> return a;Action act -> act})) (I considered doing something similar to turn Events into a real monad, but decided to choose efficiency over category theory. For events its slightly more complicated as you need to handle the choice operator as well.)
On Tue, May 14, 2002 at 04:57:12PM +0200, George Russell wrote:
According to the report
Instances of Monad should satisfy the following laws:
return a >>= k = k m >>= return = m m >>= (\x -> k x >>= h) = (m >>= k) >>= h so neither IO nor my events satisfy this. Up to now I haven't had any problems with this.
Does GHC or any other Haskell compiler actually rely on instances of Monad satisfying left identity? If not, I would suggest dropping the requirement, if it can be done without upsetting category theorists. (What the hell, they stole the term "Monad" from philosophy and changed its meaning, so why shouldn't we?)
I don't think this is necessarily wise to drop this from the report altogether. To me, it seems comparable to associativity of addition for instances of Num; many instances don't satisfy it (e.g., Float), but it's a useful guideline to keep in mind. I've often been bothered by the inconsistent treatment of laws in the report; why are there laws for functors, monads, and quot/rem and div/mod, and not much else? I'm pleased to see that the laws that are given actually do have exceptions. --Dylan
Dylan Thurston wrote: [snip]
I've often been bothered by the inconsistent treatment of laws in the report; why are there laws for functors, monads, and quot/rem and div/mod, and not much else? I'm pleased to see that the laws that are given actually do have exceptions. [snip] Even the quot/rem and div/mod laws are not always true, for example if you divide by zero, or (for div/mod, where overflows cause an error) where you get an overflow with (x `div` y) * y. Perhaps we need something in the report to state that these laws like these and the Monad laws are only intended as aspirations rather than promises.
participants (2)
-
Dylan Thurston -
George Russell