State monads don't respect the monad laws in Haskell

[S.M.Kahrs]

> "S.M.Kahrs" wrote:
> [snip]
> > I don't think this really solves the problem with the left unit
> > (not in general, and not for IO either),
> > it merely pushes it to a different place.
> [snip]
> Not being a category theorist I find this all a bit confusing.

Nothing to do with category theory.
I took the law you cited and checked it out.

>  Can you
> give an example where with GHC and the fix I suggested you can show tha=
t
> the associative law has been broken?

I didn't try to find a counter example.
I tried to prove the result and got stuck:

This is the law I was stuck with:
	m >>=3D (\x -> k x >>=3D h) =3D=3D=3D (m >>=3D k) >>=3D h  =


There were two cases to consider, m=3DR a, and m=3DM a - the former works=
 out nicely,
but with the latter you get:

m >>=3D (\x -> k x >>=3D h)
=3D	M a >>=3D (\x -> k x >>=3D h)
=3D	M (a >>=3D \a'->case (\x -> k x >>=3D h) a' of
                                R b -> return b
                                M c -> c)
=3D	M (a >>=3D \a'->case (k a' >>=3D h) of
                                R b -> return b
                                M c -> c)

and on the other side:
(m >>=3D k) >>=3D h =

=3D	(M a >>=3D k) >>=3D h
=3D	M (a >>=3D \a'->case k a' of
                                R b -> return b
                                M c -> c) >>=3D h
=3D	M ((a >>=3D \a'->case k a' of
                                R b -> return b
                                M c -> c) >>=3D \a''->case h a'' of
                                			R b -> return b
                               				M c -> c)

Assuming that the associativity law holds for the original monad
(the one we try to fix for its dodgy left unit) then this can be changed =
to:

M (a >>=3D \a' -> (\a'->case k a' of
                                R b -> return b
                                M c -> c) a' >>=3D \a''->case h a'' of
                                			R b -> return b
                               				M c -> c)
=3D	M ((a >>=3D \a' -> case k a' of
                                R b -> return b
                                M c -> c) >>=3D \a''->case h a'' of
                                			R b -> return b
                               				M c -> c)

Using associativity again:
=3D	M (a >>=3D \x->(\a' -> case k a' of
                                R b -> return b
                                M c -> c)x>>=3D(\a''->case h a'' of
                                			R b -> return b
                               				M c -> c))
=3D	M (a >>=3D \a' -> (case k a' of
                                R b -> return b
                                M c -> c) >>=3D \a''->case h a'' of
                                			R b -> return b
                               				M c -> c)

Assuming further that >>=3D is left-strict we can change that to:
=3D	M (a >>=3D \a' -> (case k a' of
                                R b -> return b >>=3D \a''->...
                                M c -> c >>=3D \a''->...))
where the ... is twice the old case h a'' expression.

Now, this is the expression why I claimed the left-unit property of
the underlying monad would still show: if (return b>>=3Df) is the same
as f b (in the monad we try to fix) then the first part of this case
expression simplifies to exactly the same thing as we had derived from th=
e
other side of the equation.

But if it does not hold, we should be able to construct a counter example=

using the left-unit counter example from the underlying monad together
with, say, k=3DR.  This all under the assumptions that the original monad=
 m
satisfied the assoc law and that its >>=3D is left-strict.

Stefan Kahrs