Add list monad transformer (for commutative monads)#181
Conversation
| Definition right_id (r : forall A, F A) (op : forall B, F B -> F B -> F B) := | ||
| forall A (m : F A), op _ m (r _) = m. | ||
|
|
||
| Definition commutative := |
There was a problem hiding this comment.
This definition is already in monad_lib.v.
There was a problem hiding this comment.
But monad_lib.v depends on hierarchy.v.
Should I just move the comment there, and remove the occurrence in monad_lib.v ?
There was a problem hiding this comment.
Which comment?
Why not move the definition from monad_lib.v to hierarchy.v to avoid the duplicate?
There was a problem hiding this comment.
There is a comment in the header of monad_lib.v relating this definition with Mu's paper.
There was a problem hiding this comment.
Oh, right, yes the "documentation" should move along.
There was a problem hiding this comment.
Speaking of documentation, the "MathComp discipline" is that at least each definition (Definition, mixins, etc.) should be reflected in the header.
|
the CI error is: not our fault, maybe transient |
2 participants
This defines the list monad transformer.
Note that it defines a monad only if the base monad is commutative, which suggests that we need a type of commutative monads to make the inference work in practice.