Open YaZko opened 2 months ago
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.
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?
I think we can have it out by the end of the week. Would that work?
Most certainly yes, that would be great!
@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.
Thanks @gmalecha . I need to take more time to dive into and play with it, but this looks great!
Thanks go to David Swasey for doing much of the development and the upstreaming work.
Goal
This ongoing PR experiments with switching from
ext-lib
tostdpp
. 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:Ongoing issues
Reduction behaviour of
mbind (m := itree E)
Broken proof for
cat_iter
inKTreeFacts.v
at the moment. Runningcbn
unfoldsmbind
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
andMBind
. They therefore replace theMonad
class that used to package both. This change comes with three immediate additional side effects:Naming: the operations are called
mret
andmbind
(instead ofret
andbind
)Notations: the associated notations live at different levels than what we were used too. Furthermore, they are slightly distinct.
x <- c;; k
becomesx ← c ; k
(only one ";", and a \gets ← instead of ascii <-)x >>= k
becomesx ≫= k
(a \gg ≫ instead of ascii >>)Change of order of arguments in
mbind
:mbind
takes the continuation first, similar to what we usually callsubst
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:Would completely expose the definition of
bind
, reducingbind c k
to(fun s : S => bind (c s) (fun sa : S * A => k (snd sa) (fst sa)))
. In contrast withmbind
, 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 replacingis_true
. Its definition is however slightly different, requiring to destructb
instead of rewriting the coerced hypothesis. As far as I understand, the typical way to do so would be via thedestr_bool
tactic. However, this tactic currently loops¹ in presence of a section variable boolean, making it a little less smooth than desired.¹ See https://github.com/coq/coq/issues/18858
Chaining class constraints
I discovered in the process the following syntax:
to list class constraints.
Progress