[WIP] Moving to stdpp

[YaZko]

Goal

This ongoing PR experiments with switching from ext-lib to stdpp. The essential rational is the increasing traction that the latter has had: it is largely both used and contributed to. Potential more concrete benefits include:

• learning from and benefiting from the effort they put into appropriately controlling reduction and type class resolution
• benefitting from their generic infrastructure in terms of tactics
• benefitting from their fin-maps
• easing interfacing with iris for project such as the one conducted by @euisuny on Vellvm
• and one may dream, converge some day towards a resolution of the universe issues surrounding the the template polymorphic definitions from the standard library.

Ongoing issues

Reduction behaviour of mbind (m := itree E)

Broken proof for cat_iter in KTreeFacts.v at the moment. Running cbn unfolds mbind and exposes the cofix brutally.

Changes and observations

Classes: Monad vs. MBind and MRet

There are already two relevant classes defined in stdpp, exclusively for notation purposes: MRet and MBind.
They therefore replace the Monad class that used to package both. This change comes with three immediate additional side effects:

1. Naming: the operations are called mret and mbind (instead of ret and bind)

2. Notations: the associated notations live at different levels than what we were used too. Furthermore, they are slightly distinct.

• x <- c;; k becomes x ← c ; k (only one ";", and a \gets ← instead of ascii <-)
• x >>= k becomes x ≫= k (a \gg ≫ instead of ascii >>)

3. Change of order of arguments in mbind: mbind takes the continuation first, similar to what we usually call subst

Reduction behaviour

Considering for instance theories/Basics/MonadState.v.
We used to have a very aggressive unfolding behaviour over the state monad.
For instance, in:

  Goal forall {A B} (c : stateT S M A) (k : A -> stateT S M B),
      bind c k = bind c k.
 intros.
 cbn.

Would completely expose the definition of bind, reducing bind c k to (fun s : S => bind (c s) (fun sa : S * A => k (snd sa) (fst sa))).
In contrast with mbind, it is inert.

Ensembles.Ensemble vs. propset

It seems to make sense to use propset, for instance when it comes to the so-called Prop monad. Although it's still too early to tell really.

Existing coercion: Is_true

ERRATUM: the coercion and the tactic come from the standard library!!

stdpp already has a coercion replacing is_true. Its definition is however slightly different, requiring to destruct b instead of rewriting the coerced hypothesis. As far as I understand, the typical way to do so would be via the destr_bool tactic. However, this tactic currently loops¹ in presence of a section variable boolean, making it a little less smooth than desired.

¹ See rocq-prover/rocq#18858

Chaining class constraints

I discovered in the process the following syntax:

Definition foo {M} `{MRet M, MBind M, ...}

to list class constraints.

Progress

• : theories/Basics/CategoryOps.d
• : theories/Basics/Utils.v
• : theories/Basics/Utils.v
• : theories/Basics/Basics.v
• : theories/Basics/HeterogeneousRelations.v
• : theories/Basics/Category.v
• : theories/Basics/CategoryOps.v
• : theories/Basics/CategoryTheory.v
• : theories/Basics/CategoryFacts.v
• : theories/Basics/CategorySub.v
• : theories/Basics/CategoryFunctor.v
• : theories/Basics/CategoryRelations.v
• : theories/Basics/Monad.v
• : theories/Basics/MonadProp.v
• : theories/Basics/MonadState.v
• : theories/Basics/CategoryKleisli.v
• : theories/Basics/CategoryKleisliFacts.v
• : theories/Basics/Function.v
• : theories/Basics/FunctionFacts.v
• : theories/Core/ITreeDefinition.v
• : theories/Core/ITreeMonad.v
• : theories/Core/KTree.v
• : theories/Core/KTreeFacts.v
• : theories/Eq/Eqit.v
• : theories/Eq/Rutt.v
• : theories/Eq/SimUpToTaus.v
• : theories/Eq/UpToTaus.v

[Lysxia]

1. Does stdpp not have those standard monads?
2. Can we take the opportunity to make this a record instead?

[YaZko]

1. They seem to have surprisingly little, no. We might eventually want to package things into a PR, or an independent library as @euisuny suggested at some point.
2. To enforce the abstraction to only leak through an explicit run? That's probably wise, although the new reduction behavior already helps a little bit in this direction.

[gmalecha]

We are pushed to use stdpp with iris and it generally works well. Their monad library is pretty minimal, but we've done a lot of work at bedrock building universe polymorphic monads, traversable and applicative as well as monads like state, reader, etc. we would like to get those released at some point.

[YaZko]

We are pushed to use stdpp with iris and it generally works well. Their monad library is pretty minimal, but we've done a lot of work at bedrock building universe polymorphic monads, traversable and applicative as well as monads like state, reader, etc. we would like to get those released at some point.

Hey @gmalecha ,
That sounds awesome, that would certainly save us some overhead in porting our libraries. Do you have any idea how soon such a release could take place?

[gmalecha]

I think we can have it out by the end of the week. Would that work?

[YaZko]

Most certainly yes, that would be great!

[gmalecha]

@YaZko Here is the repository that we have right now. https://github.com/bedrocksystems/BRiCk/tree/master/coq-upoly It is currently licensed using LGPL2 with a BedRock exception, but I don't think it will be a problem to drop the exception. We would welcome contributions.

[YaZko]

Thanks @gmalecha .
I need to take more time to dive into and play with it, but this looks great!

[gmalecha]

Thanks go to David Swasey for doing much of the development and the upstreaming work.