On Tue, Mar 2, 2010 at 1:17 PM, David Sabel
Hi, when checking the first monad law (left unit) for the IO-monad (and also for the ST monad):
return a >>= f ≡ f a
I figured out that there is the "distinguishing" context (seq [] True) which falsifies the law for a and f defined below
let a = True let f = \x -> (undefined::IO Bool) seq (return a >>= f) True True seq (f a) True *** Exception: Prelude.undefined
Is there a side-condition of the law I missed?
No, IO just doesn't obey the laws. However, I believe it does in the seq-free variant of Haskell, which is nicer for reasoning. In fact, this difference is precisely what you have observed: the distinguishing characteristic of seq-free Haskell is that (\x -> undefined) == undefined, whereas in Haskell + seq, (\x -> undefined) is defined. Operationally speaking, GHC cannot normalize an expression with IO without executing the IO, because of the evaluation model. Luke