Both Alternative and Monad provide Applicative

Stream: lean4

[Thomas Murrills]

There are some declarations that take in a Monad m and an Alternative m. However, both Monad and Alternative extend Applicative, so we wind up with two potentially different data-carrying Applicative instances in context, which often just so happen to be the same. (Context: I'm experimenting with the upcoming overlapping instances linter @Jovan Gerbscheid and I are working on; you can see warnings produced in mathlib in #34955, and this is among them. Disclaimer that there are still some bugs.)

Is there an alternative (no pun intended) design for such declarations here? Has this been discussed before? (I couldn't find a thread.)

[Robin Arnez]

Well, there is docs#AlternativeMonad (which comes from batteries#1152) for this purpose (see also #lean4 > Functor.map instance with `Alternative`)

[Thomas Murrills]

Aha, that’s exactly what I was looking for. Thanks! :)

[Jovan Gerbscheid]

Indeed. But in core lean they are having the exact same problem as in mathlib, but they don't have AlternativeMonad. What would be a good design to fix this in lean core? Should AlternativeMonad be upstreamed?

[Robin Arnez]

Well, I don't see how duplicate instance requirements would produce problems? The generic functions will most likely anyways eventually be instantiated with compatible instances. The only real problem that occurs with [Monad m] [Alternative m] is in proofs, e.g. in proving docs#failure_bind, and we only have those starting in batteries.

[Thomas Murrills]

The only way I could see it causing non-proof issues (in this case, unexpected behavior) in practice is if one or the other instance was defined “all at once” and inlined a behaviorally different applicative instance. I agree this would be very unlikely to happen, especially in core, but also because there usually aren’t terribly many options for Applicative instances.

These interfaces are exposed for downstream use, though…maybe that’s a point in favor of good practice.

I think a reasonable design would be to unbundle Alternative to take in an Applicative instance argument instead of extending it, and that this wouldn’t cause too many breaking changes.