feat: Generalize type of step indices with metaprogramming and typeclasses - #576
feat: Generalize type of step indices with metaprogramming and typeclasses #576markusdemedeiros wants to merge 53 commits into
Conversation
… for `Nat` in `StepIndexFinite.lean`
…stances not yet complete
Replace all proofs in section `Fixpoint`, all requires rewrite
…and `Contractive.succ`
Parametrisation of `CMRA` to be done in a future PR
…nt with `SI = Nat`
|
I merged master into this branch and resolved the conflicts. Something is broken with the Display tests, which I don't understand. @alvinylt Can you look into this? |
|
(I'm doing a pass and will also fix the |
Do you mean |
Very weird. It seems like I got my local copy into a weird state where the test would fail. A I am done with my cleanup pass over this PR. From my side, the only thing that is missing is moving the |
|
!bench |
|
Benchmark results for ece2feb against fa57ead are in. There are significant results. @MackieLoeffel
Large changes (5🟥)
Medium changes (18🟥)
Small changes (34🟥)
|
I have to say that I am a bit worried about this. OFE is the only file that is generic over the stepindex right now. If all files become twice as slow when we make them parametric over the step index, this would be not so great. It seems like this is due to the added typeclass search, but I have to look into this more. |
|
My pass is done. All
I think 2x would be not great, but it could also be worse than 2x. Perhaps we should ask around on the Zulip about this? |
|
I wonder if there's another file we could generalize to see if the pattern holds (though, we might have to generalize CMRA first to experiment with that, which seems like a big job) |
|
Do we have any data on how big was the slowdown in the Rocq version? |
|
A superlinear slowdown would worry me enough to rethink the mechanism used in this PR. A 2x slowdown would not so much. This PR is about 10s faster than Iris-Rocq atm and even with a 2x slowdown we might be able to sqeeze it back under (of course, if there's a substantially faster implementation of |
|
!bench |
|
Benchmark results for 782f99f against a5f3796 are in. There are significant results. @MackieLoeffel
Large changes (5🟥)
Medium changes (33🟥)
Small changes (136🟥)
|
|
I am currently experimenting with an alternative version of the typeclass hierarchy in #627 . It seems to cut the typeclass synthesis time in OFE.lean in half, but it requires more care that we don't have duplicate instances in the context. I will post a message once I am done with my experiments and have something to report. |
|
I've looked into this and I have good news and bad news. The good news is that there is a version of this generalization that works and where the slowdown is significantly lower for Suspected cause of the slowdown in #576My suspicion for the cause of the slowdown of the version in this PR is that using Causes the following typeclass trace, just for These failing typeclass searches appear for every Alternative version using outparam #627In #627, I did an experiment with an alternative version where Performance comparisonHere are the performance numbers of the different versions. All comparisons use commit a5f3796 as the base commit of the master branch. Bench of #576 against master Bench of #627 against master Comparison of #627 directly against #576 Since these performance numbers are always very abstract, I also profiled master As one can see, there is a significant difference between all three versions. ( What now?The following options come to mind: A) Merge #576 as is and take the performance hit B) Improve #627 with metaprogramming to give errors when the user imports two instances C) Port more files to be generalized over the step index to see how big the performance impact is when more code is generalized. D) Come up with some other version that has none of the downsides and all of the advantages My personal preference would be D) if someone has an idea, otherwise C). I hope this comment gives enough information that we can discuss this. |
|
Bummer! Thanks for digging into this, and I'll also say it was great foresight on your part to set up this radar stuff. Indeed, I cannot think of a way around having a default instance (for its mvar setting abilities) and also a high priority instance. So any SIdx instance that is default will be tried last. Can you trace where those 6 failing As for just eating the cost: I would now not feel comfortable doing that without knowing what the long term implications are, especially if 6 is actually o(n). Maybe we should just try generalizing some more files and see what happens? |
5 participants
This PR builds off of Alvin's work in #550, as well as Mario's work and my own attempt. I believe it solves every single problem reported with the prior attempts at this feature. The text here is long because I will try to explain how.
TL;DR:
outParambehaviors around local class inference.OFE.eq_dist: see limitations below).SIdxclasses even in the same theorem.In PR #550 I mentioned that having local scoped instances that could depend on section variables would solve all of our problems. This PR started by trying to emulate that, and morphed into something I think might make everybody 99%-100% happy.
Technique
The trick is to have a special typeclasss for default
SIdximplementations, and let that provide the default instance forSIdx. Concretely, we start with the normal implicit index version of OFE (similar for COFE, OFunctor, etc)however, we add a second class for declaring default step index instances with an
outParamindex, and let it be the default instance for the step index typeInitially I did this to put different defaults in different scopes (so we could emulate scoped default instances) but I ended up deciding that an elab was a better way to control it. To that end, the
stepindexcommand puts an instance of theDefaultSIclass in scope and does some sanity checks to ensure that it is the only one at elab time:scoped stepindex NatOrdinal works in IrisMath too. Unlike hypothetical scoped default instances, the default index type can depend on section variables, so your type of step indices can be defined from any other Lean machinery. Here is how to generalize a section to use a generic type of step indices, such that the
SIdxconstraint on the type obeys normal typeclass synthesis rules:Hierarchy
Once a
stepindexis declared, aDefaultSIinstance is put in scope, so plain typeclass synthesis will handle filling in theSItype and the[SIdx SI]instances almost exactly like it would have in theoutParamapproach. However there are big improvements related to how stable this is. Synthesis of this arbitrary instance happens once, at the time thelocal stepindexcommand is elab'd, and in the happy path this instance will be synthesized using normal synthesis rules (ie. it will pick the[SIdx SI]instance forSIin the snippet above, not an arbitrary instance at every call site). Even if you get it wrong, and break the hierarchy in some other way, because synthesis happens only once this choice is guaranteed to be self-consistent for the rest of the section.I've also used the module system to make declaring
DefaultSIinstances out of band difficult. It's not impossible, I don't think, but I think it is very hard to do by accident. Compare this to accidentally copy-pasting anopenstatement that includes a scope you didn't realize had aSIdxinstance in it: the latter is much easier to get wrong. Setting a global step index type is also disabled.Basic hierarchy discipline like avoiding non-definitional diamonds still applies of course, but it is no longer possible for an unrelated
SIdxtypeclass instance to break unrelatedOFEsynthesis. Thestepindexcommand also has an option to provide an explicit instance name: I suspect this is unnecessary, but it gives you to turn off even the command elab-time nondeterminism if such a need arises. The final hierarchy thing I'll mention is that, unlike theoutParamappraoches, the default step indices are fully opt-in. I can useOFE/COFE/OFunctor/... without interacting setting default step indices at all, and it behaves like any other two-parameter Lean typeclass. You can use multiple index types in the same theorem if you want. The stability of our algebraic hierarchy is preserved with or without default step indices set.Notations
Because of the
outParam, you get nearly every nicety of Alvin's original approaches, and adapting old code is nearly zero work.OFEdoes not need to specify itsSIparameter, and step indices (even0) do not need to specify their type. I also reused thestepindex%term elab from my other attempt: this elaborates to the current default step index type or a hole if none is set. However, unlike my prior approach, this is not used for any oddoptParamstuff: it's used a total of three times so that we can have reuse the old notation and make it fill in theSItype at its elab site:Doing it this way avoids the need for the duplicate scoped notations as in Mario's version. I didn't even define notation for adding in the type
SIbecause I think at this point it is not necessary.Limitation
The only edge case I could not resolve was for
eq_dist(and a few one-offs like it): this is an annoying combination of both not being a notation, and not referencing the step index type, so neither typeclass inference nor anoptParamcan be used to fill the type. Admittedly, theoutParamversion (nondetermistically) fills this in at every call site where mind doesn't.In this PR I explicitly fixed each
SIinstance beNatorSIas at each call site so that the Lean code looks normal. I could have also definedeq_dist'to beeq_distfixing(SI := stepindex%)with anoptParamand it would be uniform across the repo. I'm open to any solutions to this problem.Conclusion
I hope this version meets everybody's requirements! I think this solution is more than the sum of its parts, and cards on the table, I'm very pleased with it. To me it feels quite inline with other Lean features. I look forward to your feedback :)
cc: @alvinylt @MackieLoeffel @Kaptch @digama0