Must mplus always be associative? Haskell wiki vs. Oleg Kiselyov

Question

The Haskell wikibook asserts that

Instances of MonadPlus are required to fulfill several rules, just as instances of Monad are required to fulfill the three monad laws. ... The most essential are that mzero and mplus form a monoid.

A consequence of which is that mplus must be associative. The Haskell wiki agrees.

However, Oleg, in one of his many backtracking search implementations, writes that

-- Generally speaking, mplus is not associative. It better not be,
-- since associative and non-commutative mplus makes the search
-- strategy incomplete.

Is it kosher to define a non-associative mplus? The first two links pretty clearly suggest you don't have a real MonadPlus instance if mplus isn't associative. But if Oleg does it ... (On the other hand, in that file he's just defining a function called mplus, and doesn't claim that that mplus is the mplus of MonadPlus. He chose a pretty confusing name, if that's the right interpretation.)

Answer 1

Below is the opinion of Oleg Himself, with my comment and his clarification.

O.K. First I would like to register my disagreement with Gabriel Gonzalez. Not everyone agrees that MonadPlus should be monoid with respect to mplus and mzero. The Report says nothing about it. There are many compelling cases when this is not so (see below). Generally, the algebraic structure should fit the task. That's why we have groups, and also weaker semi-groups or groupoids (magmas). It seems MonadPlus is often regarded as a search/non-determinism monad. If so, then the properties of MonadPlus should be those that facilitate search and reasoning about search — rather than some ideal ad hoc properties someone likes for whatever reason. Let me give an example: it is tempting to posit the law

m >> mzero === mzero

However, monads that support search and can do other effects (think of NonDeT m) cannot satisfy that law. For example,

print "OK" >> mzero  =/==  mzero

because the left-hand side prints something but the right-hand doesn't. By the same token, mplus cannot be symmetric: mplus m1 m2 generally differs from mplus m2 m1, in the same model.

Let us come to mplus. There are two main reason NOT to require mplus be associative. First is the completeness of the search. Consider

ones = return 1 `mplus` ones

foo = ones `mplus` return 2
  === {- inlining ones -}
  (return 1 `mplus` ones) `mplus` return 2
  === {- associativity -}
  return 1 `mplus` (ones `mplus` return 2)
  ===
  return 1 `mplus` foo

It would seem therefore, coinductively ones and foo are the same. That means, we will never get the answer 2 from foo.

That results holds for ANY search that can be represented by MonadPlus, so long as mplus is associative and non-commutative. Therefore, if MonadPlus is a monad for search, then associativity of mplus is an unreasonable requirement.

Here is the second reason: sometimes we wish for a probabilistic search — or, in general, weighted search, when some alternatives are weighted. It is obvious that the probabilistic choice operator is not associative. For that reason, our JFP paper specifically avoids imposing monoid (mplus, mzero) structure on MonadPlus.

http://okmij.org/ftp/Computation/monads.html#lazy-sharing-nondet (see the discussion around Figure 1 of the paper).

R.C. I think Gabriel and you agree on the fact that search monads do not exhibit the monoid structure. The argument boils down to whether MonadPlus should be used for search monads or should there be another class, let's call it MonadPlus', which is just like MonadPlus but with more lax laws. As you say, the report doesn't say anything on this topic, and there's no authority to decide.

For the purpose of reasoning, I don't see any problem with that — one just has to state clearly her assumptions about the MonadPlus instances.

As for the rewrite rule that re-associates mplus'es, the mere existence and widespread use of MonadPlus instances that are not associative, regardless of whether they are "broken", means that one should probably abstain from defining it.

O.K. I guess I disagree with Gabriel's statement

The monoid laws are the minimum requirement because without them the other laws are meaningless. For example, when you say mzero >>= f = mzero, you first need some sensible definition of mzero is, but without the identity laws you don't have that. The monoid laws are what keep the other proposed laws "honest". If you don't have the monoid laws then you have no sensible laws and what's the point of a theoretical type class that has no laws?

For example, LogicT paper and especially the JFP paper has lots of examples of equational reasoning about non-determinism, without associativity of mplus. The JFP paper omits all monoid laws for mplus and mzero (but uses mzero >>= f === mzero). It seems one can have "honest" and "sensible laws" for non-determinism and search without the monoid laws for mplus and mzero.

I'm also not sure I agree with the claim

The two laws that everybody agrees that MonadPlus should obey are the identity and associativity laws (a.k.a. the monoid laws):

I'm not sure a poll has been taken on this. The Report states no laws for mplus (perhaps the authors were still debating them). So, I would say the issue is open — and this is the main message to get across.

Answer 2

The two laws that everybody agrees that MonadPlus should obey are the identity and associativity laws (a.k.a. the monoid laws):

mplus mempty a = a

mplus a mempty = a

mplus (mplus a b) c = mplus a (mplus b c)

I always assume they hold in all MonadPlus instances that I use and consider instances that violate those laws to be "broken", whether or not they were written by Oleg.

Oleg is right that associativity does not play nicely with breadth-first search, but that just means that MonadPlus is not the abstraction he is looking for.

To answer the point you made in a comment, I would always consider that rewrite rule of yours sound.

Answer 3

It's rare that MonadPlus instances violate associativity, but clearly not impossible. Typeclasses can only be counted to satisfy the "obvious" laws up to a certain amount. For instance, four further sets of possible laws for MonadPlus are discussed here without any conclusion and with libraries following various conventions without specifying which.

Clearly, Oleg has a reason to dismiss associativity. Is it "truly a MonadPlus instance"? Who knows, it's not well enough defined to say.