MonadZero and MonadPlus seem redundant?
LukaJCB opened this issue · 10 comments
Given the laws of Monad that state apply = ap as well as the laws of Alternative that state
empty <*> f = empty, we can practically derive the MonadZero law empty >>= f = empty.
Thus, it seems to me that we do not need to specify this law in addition to the laws already present.
Furthermore, MonadPlus has the requirement that >>= distribute over <|>. Though as it extends Alternative which already requires distribution of <*> over <|> and again, since <*> = ap we already get that property. Am I missing something here?
Hmm yeah, that does seem right!
To add to that: it's not entirely clear to me that if we have <*> distributing over <|> plus apply = ap, that this implies that >>= distributes over <|>. Do you have a proof of this?
I don't have a proof and maybe I'm wrong here, what is the case where Maybe doesn't distribute?
> x = Just false
> y = Just true
> f cond = if cond then Just 0 else Nothing
> (x <|> y) >>= f
Nothing
> (x >>= f) <|> (y >>= f)
(Just 0)
This is why Maybe has MonadZero but not MonadPlus.
Very interesting! Of course the above won't work for <*> so I guess that distinction is safe. I wonder if my misconception also extends to absorption.
Yeah, I've verified that Maybe is indeed a valid Alternative so MonadPlus isn't redundant. I'm not sure about absorption though: all of the monads I can think of which have Alternative instances satisfy both the <*> and >>= absorption laws.
Oops, the MonadZero question isn't yet resolved.
I think you’re right about MonadZero: suppose F is a type constructor with valid Monad and Alternative instances. Now the type of its empty is forall a. F a, which means that it can’t possibly contain a value of whatever type a ends up being instantiated as. Now if we write empty >>= f, the implementation of >>= can’t apply f at any point, because we don’t have anything to apply it to. Therefore empty >>= f can’t depend on the behaviour of f. Therefore empty >>= f is the same as empty >>= g for any fixed g whose result type is the same as f. In particular, if we pick g = pure, the right identity monad law ensures that empty >>= pure = empty, and so empty >>= f = empty for all f.