> "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 that
> 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 >>= (\x -> k x >>= h) === (m >>= k) >>= h
There were two cases to consider, m=R a, and m=M a - the former works out nicely,
but with the latter you get:
m >>= (\x -> k x >>= h)
= M a >>= (\x -> k x >>= h)
= M (a >>= \a'->case (\x -> k x >>= h) a' of
R b -> return b
M c -> c)
= M (a >>= \a'->case (k a' >>= h) of
R b -> return b
M c -> c)
and on the other side:
(m >>= k) >>= h
= (M a >>= k) >>= h
= M (a >>= \a'->case k a' of
R b -> return b
M c -> c) >>= h
= M ((a >>= \a'->case k a' of
R b -> return b
M c -> c) >>= \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 >>= \a' -> (\a'->case k a' of
R b -> return b
M c -> c) a' >>= \a''->case h a'' of
R b -> return b
M c -> c)
= M ((a >>= \a' -> case k a' of
R b -> return b
M c -> c) >>= \a''->case h a'' of
R b -> return b
M c -> c)
Using associativity again:
= M (a >>= \x->(\a' -> case k a' of
R b -> return b
M c -> c)x>>=(\a''->case h a'' of
R b -> return b
M c -> c))
= M (a >>= \a' -> (case k a' of
R b -> return b
M c -> c) >>= \a''->case h a'' of
R b -> return b
M c -> c)
Assuming further that >>= is left-strict we can change that to:
= M (a >>= \a' -> (case k a' of
R b -> return b >>= \a''->...
M c -> c >>= \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>>=f) 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 the
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=R. This all under the assumptions that the original monad m
satisfied the assoc law and that its >>= is left-strict.
Stefan Kahrs
_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
