[Haskell-cafe] Monad laws

[Yitzchak Gale]

David Sabel wrote:
>> when checking the first monad law (left unit) for the IO-monad (and also for
>> the ST monad):
>> I figured out that there is the "distinguishing" context (seq [] True) which
>> falsifies the law...

It's worse than that - Haskell types and functions do not
even form a category under Haskell composition:

Prelude> seq (id . undefined) 42
42
Prelude> seq undefined 42
*** Exception: Prelude.undefined

So (id . undefined) /= undefined, violating one of the category laws.

This is not just a problem with IO - it's a problem with Haskell
itself.

Luke Palmer wrote:
> 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.

Ignoring the existence of seq does solve both problems.
This seems like a messy solution, because seq really
*does* exist, and it seems essential. But it's not as bad as it
sounds. Even without the built-in seq, you can define seq
manually for most common types:

class Seq a where seq :: a -> b -> b

instance Seq Int where
  seq 0 x = x
  seq _ x = x

etc. You just wouldn't have seq for function types.

There is another way around this problem in which we
don't need to ignore seq. Let's define strict composition:

f .! g = f `seq` g `seq` f . g

This is "true" function composition in the mathematical
sense - it doesn't have the extra layer of laziness that
Haskell usually imposes. With strict composition,
Haskell types and functions do form a category even
when we include seq.

Unfortunately, IO still does not satisfy the monad laws.
But that could easily be fixed by making return strict,
so that return undefined == undefined. (Note also that
by "monad laws" here I mean the points-free version of the
laws, with strict composition. That is the version of the
laws we get if take the mathematical monad laws
in the category we have just defined and translate them
into Haskell monad notation.)

Category theorists tend not to like this method of resolving
the problem as much. The category we get this way is lacking
some important basic properties, so it is harder for them to
work with. But I think it better reflects the reality of Haskell,
which does in fact include seq.

For this reason, I consider it a bug in GHC that return :: IO a
is lazy.

Regards,
Yitz