incorrect MonadPlus law "v >> mzero = mzero"?

[John Lato]

On Wed, Feb 5, 2014 at 6:32 PM, wren ng thornton
<winterkoninkje at gmail.com>wrote:

> On Wed, Feb 5, 2014 at 8:38 PM, John Lato <jwlato at gmail.com> wrote:
> > On Wed, Feb 5, 2014 at 5:01 PM, wren ng thornton <
> winterkoninkje at gmail.com>
> > wrote:
> >>
> >> On Wed, Feb 5, 2014 at 7:59 PM, wren ng thornton
> >> <winterkoninkje at gmail.com> wrote:
> >> > The rules I'd expect MonadPlus to obey are:
> >> >
> >> >     mzero >>= f    =    mzero
> >> >
> >> >     (x `mplus` y) >> mzero    =    (x >> mzero) `mplus` (y >> mzero)
> >>
> >> Er, sorry, that should've been:
> >>
> >>     (x `mplus` y) >> z    =    (x >> z) `mplus` (y >> z)
> >>
> >> from which the above instance follows trivially.
> >
> > I don't think this is correct. [...] Or concretely,
> >
> >> let x = lift (print "x!") :: MaybeT IO ()
> >> let y = lift (print "y!") :: MaybeT IO ()
> >> runMaybeT $ (x `mplus` y) >> mzero
> >
> > "x!"
> > Nothing
> >
> >> runMaybeT $ (x >> mzero) `mplus` (y >> mzero)
> >
> > "x!"
> > "y!"
> > Nothing
>
> Well, notably, the Maybe part of things does agree. It's the
> transformer part which breaks things. However, this is something that
> could be "fixed" by changing the implementation of mplus for MaybeT.
> In particular, if we have it fully execute both arguments, but then
> discard the results of latter ones whenever earlier ones have
> succeeded. That is,
>
>     mplus x y = MaybeT $ do
>         v <- runMaybeT x
>         w <- runMaybeT y
>         case v of
>             Nothing -> return w
>             Just _  -> return v
>
> This "fix" ensures that the law is obeyed regardless of the underlying
> monad. However, it's not necessarily the instance we want. So the
> question is: for monad transformers, what --explicitly, concretely-- do
> we want? Do we consider the current MaybeT instance sacrosanct? What
> about the other popular instances?
>

That instance would mean that  x `mplus` y /= x, when y assumes certain
zeros.  This property is more important to me than the other, at least as
far as MaybeT is concerned.   YMMV.

Personally, I'm ok with treating all zeros as equal so far as the laws are
concerned.  Any particular instance with multiple zeros should document how
they're propagated at mplus though.  Of course, if we treat zeros as
equivalent, then (v >> mzero = mzero) holds ;)

John


> I still think the above laws are the most sensible ones. I discuss a
> bit about why I believe that in this blog post I just posted[1]. The
> only alternative I see is to drop every law about how mplus interacts
> with bind, which isn't a solution quite so much as giving up.
>
> [1] <http://winterkoninkje.dreamwidth.org/90905.html>
>
> --
> Live well,
> ~wren
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20140205/377ef1d7/attachment.html>