On Apr 30, 2005, at 9:51 AM, Jacques Carette wrote:

Ashley Yakeley <ashley@semantic.org> wrote:

...

I've added a bit more to <http://haskell.org/hawiki/MonadPlus>. I highly recommend people read it before they start claiming in papers that such-and-such a type "may thus be an instance of MonadPlus".

Very nice.

One of the problems I have encountered with MonadPlus is that too many people try to force it to be a Monoid, when it doesn't always want to be. Your suggestion of separating out the identity operation from the binary operation makes it much clearer that these various Monads are actually instances of Magma(s) http://en.wikipedia.org/wiki/Magma_%28algebra%29 than necessarily a Monoid.

And the binary operation in a Magma has *no* properties. My feeling is that there MonadPlus must have *some* set of properties in order to be useful---otherwise it's just an ad-hoc mechanism to call a pile of different binary operations "mplus". I think most people would agree that's undesiriable, and the only confusion is which properties must hold. I claim "monoid" is a point of agreement, at least.

On the above Wikipedia article, there is a useful ontology of identities that can be useful to describe various Magmas.

And points up the sheer complexity of the hierarchy that would result if we tried to slice it into minimal orthogonal pieces (even if we immediately reject, say, division as uninteresting). The focus must be on identifying the properties that really matter, encoding those, and rejecting those which merely add unnecessary complexity.

Jacques

PS: your discussion of the laws of MonadPlus reinforces to me the real need for being able to declare the laws that a typeclass should satisfy, not just the signature.

On this I cannot but agree. But we don't usually count on being able to prove these by construction. -Jan-Willem Maessen

Jan-Willem Maessen <jmaessen@alum.mit.edu> wrote:

...

...discussion of the laws of MonadPlus reinforces to me the real need for being able to declare the laws that a typeclass should satisfy, not just the signature.

On this I cannot but agree. But we don't usually count on being able to prove these by construction.

Note that I was just suggesting that the laws be given and available (ie as type-level constructs, not comments). I was not suggesting that 'proofs' be either done by the compiler, nor even given as necessary annotations. Although if they were present (as annotations), the proof itself might furnish some additional ingredients that an advanced optimizer might be able to use to good effect... Jacques