Update documentation of post-AMP `MonadPlus` laws
AbandonedPublic

Authored by hvr on Nov 6 2014, 2:17 AM.

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Branch
master
Lint
Lint OK
Unit
No Unit Test Coverage
Build Status
Buildable 1738
Build 1745: GHC Patch Validation (amd64/Linux)
hvr updated this revision to Diff 1295.Nov 6 2014, 2:17 AM
hvr retitled this revision from to Update documentation of post-AMP `MonadPlus` laws.
hvr added reviewers: ekmett, dfeuer.
hvr added a comment.Nov 6 2014, 2:20 AM

Here's a screenshot of the resulting Haddock output:

dfeuer edited edge metadata.Nov 6 2014, 2:52 AM

Let's think this through a bit. The current rules say that mplus is associative and mzero is its identity, and that

mzero >>= f  =  mzero
v >> mzero   =  mzero

We're also told that (<|>) is associative and has empty as its identity, but we're not told anything else about them whatsoever. Ouch. We know that for any MonadPlus, we want

mzero = empty
mplus = (<|>)

which means the monoid laws for mzero and mplus follow directly from the ones for empty and (<|>) and don't necessarily need to be repeated.

The above suggest that perhaps we want to require

v *> empty = empty

and also

empty <*>  x = empty

And then build the MonadPlus laws on top (if there are any left). Are there sane Alternative instances that don't obey those rules?

dfeuer added a comment.Nov 6 2014, 8:48 AM
v *> empty = empty

means

(id <$ v) <*> empty = empty

I'm pretty sure this actually implies that for all v,

v <*> empty = empty

although I'm not quite certain of that (@ekmett may know). That would give Alternative the nice, symmetrical rules

v <*> empty = empty
empty <*> v = empty

Intuitively, this seems to make sense: if you apply some functions to no values, or no functions to some values, you get no results.

dfeuer added a comment.Nov 6 2014, 8:53 AM

One thing that's still missing, perhaps, is some kind of "distributive" law relating <*> to <|>. It feels like there should be something like that to relate the two.

ekmett edited edge metadata.Nov 6 2014, 12:06 PM

the right unit law doesn't hold.

putStrLn "hello world" <*> empty /= empty

For that matter it is a longstanding issue that this also doesn't hold for:

putStrLn "hello world" `mplus` mzero /= mzero
dfeuer added a comment.Nov 6 2014, 1:49 PM
In D449#11004, @ekmett wrote:

the right unit law doesn't hold.

putStrLn "hello world" <*> empty /= empty

For that matter it is a longstanding issue that this also doesn't hold for:

putStrLn "hello world" `mplus` mzero /= mzero

A discussion of some of the issues with MonadPlus can be found in the MonadPlus reform proposal on the wiki.

The reform proposal starts with a MonadZero class with

mzero >>= k = mzero

This immediately produces two sensible laws for fmap and <*>:

fmap f empty = empty
empty <*> x = empty

The proposed subclasses each add a monoid operation. The one they choose to call MonadPlus satisfies a "left distribution" law:

mplus a b >>= k = mplus (a >>= k) (b >>= k)

The "left distribution" law, applied to Alternative, looks like this:

(a <|> b) <*> c
= (a <|> b) >>= \f -> c >>= \x -> return (f x)
= (a >>= \f -> c >>= \x -> return (f x)) <|> (b >>= \f -> c >>= \x -> return (f x))
= (a <*> c) <|> (b <*> c)

which suggests, then, the Alternative law

(a <|> b) <*> c = (a <*> c) <|> (b <*> c)

Now Maybe doesn't satisfy the left distribution law, but it "morally" satisfies the Alternative version:

(Just f <|> b) <*> c = Just f <*> c = case c of {Nothing -> Nothing; Just x -> Just (f x)}
(Nothing <|> b) <*> c = b <*> c
(Just f <*> c) <|> (b <*> c) = case c of {Nothing -> b `seq` Nothing; Just x -> Just (f x)}
(Nothing <*> c) <|> (b <*> c) = Nothing <|> (b <*> c) = b <*> c

The failure of precision there gets much worse with IO, unfortunately.


I'm not seeing anything terribly interesting or useful about the alternative "left catch" version, that they call MonadOr and that Maybe and IO fit into naturally.

dfeuer added a comment.Nov 6 2014, 2:44 PM

Actually, IO doesn't really fit into any of these things very well, does it? Maybe that's why the entire module making it an instance of MonadPlus is marked as deprecated. I think we can probably safely document these laws:

fmap f empty = empty
empty <*> x = empty

Much more and we'll need a lot more community support. Personally, I love the idea of splitting the class—as it is, MonadPlus and Alternative mean very little. But that's not my decision.

empty <*> x = empty

doesn't hold. Monad has to inspect the left argument or be trivial because there is no way to see under the lambda in the right hand argument to proceed. However, Applicative is under no such limitation.

>>> import Control.Applicative
>>> import Control.Applicative.Backwards
>>> import Control.Monad.IO.Class
>>> import Control.Monad.List
>>> runListT $ forwards (empty <*> Backwards (liftIO $ putStrLn "hello"))
hello
[]
>>> runListT $ forwards empty
[]

Here I'm not using IO's Alternative, but IO is in the monad transformer stack.

fmap f empty = empty

can be documented though! =)

hvr added a comment.Nov 7 2014, 10:57 AM

...so, what's the conclusion so far? what laws shall we write into MonadPlus's Haddock docstring?

I think we should get rid of the monoid claim, as it's apparently not true, and write that <|> and mplus are binary operators that must "do the needful", to borrow a most vague Indian English phrase.

rwbarton edited edge metadata.Nov 7 2014, 2:32 PM

What's the counterexample to MonadPlus being a monoid?

I'm a little confused about the status of the instance MonadPlus IO, but the only problem I see with it being a monoid is that throwIO SomeFunnyIOException <|> mzero is mzero and not throwIO SomeFunnyIOException. But surely the law is closer to being satisfied than not satisfied: the only difference is in which exception is thrown.

austin requested changes to this revision.Nov 24 2014, 1:37 PM
austin edited edge metadata.

Requesting further bikeshedding until we reach a consensus.

This revision now requires changes to proceed.Nov 24 2014, 1:37 PM
hvr added a comment.Nov 25 2014, 7:31 AM

Btw, if anyone feels entitled to take the lead, please feel free to commandeer this code-revision and take control. I'm too distracted to be able to follow where this discussion is going... :-)

hvr abandoned this revision.Nov 1 2015, 6:26 AM

I'm giving up this one, as at this point I consider MonadPlus somewhat obsolete

See also https://prime.haskell.org/ticket/157