Indexed vs. non-indexed monads in the stdlib

[ajrouvoet]

The library defines both indexed (i.e., parameterized) and usual monads on Set, and non-indexed monads on indexed sets (RawPMonad), but not indexed monads on indexed sets.

Having all these flavors is a bit annoying. Also because you want instances for your usual monads of all these flavors...

I would like to propose defining only the indexed monads on Set and Pred and getting the non-indexed version by indexing with the unit type. This makes things more uniform and avoids the flavor explosion; indexing by unit does not bother the client of the library afaict.

I'm interested in this because I want to propose two type-classes for strong monads. One for strength over the pointwise product, and one for strength over the separating conjunction. Having these for both types of monads again explodes a bit...

[MatthewDaggitt]

Hmm... so this proposal would go against the design of other indexed datatypes in the library (e.g. Relation.Binary.Indexed) which are usually defined separately.

indexing by unit does not bother the client of the library afaict.

This unfortunately wasn't true when I played around with designing indexed versions of the metrics found in pull request #1038 (the indexed versions aren't included in the PR). The problem was that it was very hard to guarantee that the trivial indexing type was always inferrable. Done naively by simply re-exporting the type applied to ⊤ you still end up having to scatter things like {⊤} throughout your code when applying functions in which the indexing type has to be inferred but for whatever reason can't be.

To get around this you end up having to create a copy of lots functions where you manually provide ⊤ as implicit argument. This is annoying (but probably managable) for the library maintainers, but super annoying for users who then have to fiddle about with it when writing their own functions. Furthermore, even with this approach, I seem to remember I was still running into the occasional problem. In the end I abandoned the idea and went back to defining them separately.

Of course there may be something different about monads that make them more amenable to indexing! Have you tried making some limited changes and looking at the effects?

Basically, based on my (non-monad) experience I would argue for keeping the definitions separate. Indexed versions of definitions are much less common than non-indexed versions, so I would argue it makes sense to optimise for the latter rather than the former... For example, I would start quaking in terror if someone suggested we do the same thing for the algebra hierarchy :fearful:

[gallais]

@JacquesCarette probably has relevant opinions on generalising monads to arbitrary categories rather than introducing a bunch of special cases.

[ajrouvoet]

I haven't experimented with changing the definitions in the stdlib itself, but I have a library for doing separation logic in Agda based on ternary relations. It defines various monads---both indexed and non-indexed---based on an indexed definition of monads on predicates:

here is the definition of indexed monads on indexed sets. here is an example of an indexed instance. here is an example of a non-indexed instance.

I've don't recall needing to insert {⊤} annotations. But I'm not sure where you needed annotations. I'm explicitly saying that the instance is indexed by ⊤; after that I can use the monad's API without trouble it seems.

[ajrouvoet]

on generalising monads to arbitrary categories

In my mind that is what distinguishes these special cases from other monads at the moment is that we have an idea of how to program with them in Agda. It is not so clear to me to what extent that affects how they should be formalized.

[JacquesCarette]

Sorry for being slow on this.

The thing is, indexed Monads aren't - as well explained on this StackOverflow answer. For them to be seen as monads, you need to climb up a level to 2-Monads in 2-Categories, and in fact, something slightly weaker still. The categorically-minded can read A 2-Categorical Study of Graded and Indexed Monads, a Master's Thesis by Soijiro Fujii. Also worth reading about are graded monads and the references there.

In particular, the paper Unifying graded and parametrised monads does make a valiant attempt at also looking at programming with them.

In many ways, the stuff that is currently in stdlib is really awful [unlike others, I rather like most of stdlib, but this is definitely one of its dark corners]. It's a direct port of Haskell-oriented things, without really trying hard enough to lift to the dependently-typed case. It can belong in a very programming-oriented library, but is ill-suited to a proof-oriented library.

Basically I'm saying that these generalizations really belong in an experimental library (or 3 or 5 such libraries), to shake out what is really needed/wanted. I don't think we have the right knowledge available to us right now to make those design choices. So it feels very premature to talk about it for the stdlib. We can live with the historical warts in the current RawMonad stuff, but let's not hurry to add more sub-optimal designs!