[Haskell-cafe] Monad laws

[Luke Palmer]

On Tue, Mar 2, 2010 at 1:17 PM, David Sabel
<sabel at ki.informatik.uni-frankfurt.de> wrote:
> 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