Add monotone predicate monad to sdtlib

[ajrouvoet]

We've developed monotone predicate monads for e.g. monotone typed state.
I was wondering if there is interest in getting such definitions into the standard library.
If so, I can prepare a PR.

One implements a monotone predicate monad by instantiating:

record RawMPMonad (M : Pt I ℓ) : Set (suc ℓ) where
  infixl 1 _≥=_
  field
    return : ∀ {P} → P ⊆ M P
    _≥=_   : ∀ {P Q} → M P ⊆ ((P ↗ M Q) ⇒ M Q)

where (P ↗ M Q) is the kripke function space.
You get an RawPMonad instance for free, as well as monadic strength.
Using monadic strength and appropriate instances of the Monotone typeclass, you can
program with it.

Monotone Predicate Monads
Monotone Typed State
Monotone Type class
An instance
Kripke stuff

Tasks

• decompose Kripke function space; drop alternative notation
• What we call Monotone is called Closed in the stdlib

[MatthewDaggitt]

@gallais any thoughts? You've done the most tinkering with this part of the library.

[gallais]

I think it would be nice to have.

Note that the Kripke function space can be decomposed into

• Closure wrt a Relation (The preorder closure in particular https://agda.github.io/agda-stdlib/Relation.Unary.Closure.Preorder.html)
• Standard implication between two relations

We can write □ (P ⇒ M Q) for P ↗ M Q.

[ajrouvoet]

Yes indeed. I'll prepare a PR next week. Would be good to have an idea of what parts are widely applicable enough to include. The referenced code has a bunch of instances that do not have RawMonad counterparts in the stdlib, so it might not make sense to include their monotone counterparts.

[ajrouvoet]

Related to this I wanted to raise the question whether it would be worth considering to extend do-notation in Agda to support convenient programming with monads that require application of monadic strength.

For these kinds of monads that maintain strong invariants, strength is essential, but bothersome to apply manually. I imagine that automated application would not require much more than closure conversion. Haskell's support for arrow notation seems to require similar transformations.

I can move this discussion upstream to the compiler implementation, but I thought it made sense to attach it to a potential use-case to test the waters for interest.