docs: Library note on performance when defining instances#7432
docs: Library note on performance when defining instances#7432ChrisHughes24 wants to merge 4 commits intomasterfrom
Conversation
riccardobrasca
left a comment
There was a problem hiding this comment.
Sometimes it is better to avoid with, right? Maybe we can explain more here.
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
I'm writing instructions with this PR in mind. So after that PR it won't necessarily be best to avoid |
|
My understanding of unification is still mainly anecdotal but this lines up with my expectations. It might be useful to open this up to a broader discussion on Zulip where we can get some input from core and others. One point I do know and that is implicit here but might benefit from being made explicit: aligning the inheritance structure for instance construction only matters mainly for data carrying fields. |
|
Lean also seems to really dislike unifying instances constructed using differing patterns. My guess that it has to unfold everything on both sides to reach a common state. |
|
I solicited some expert opinion on Zulip for any potential refinements. |
|
I haven't followed this discussion closely, but a library note like this is good (and we can refine it later with more experience). I presume that this library note is still relevant after lean4#2644? bors d+ |
|
✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with |
|
I don't think it is still relevant. Or at least the gains are much less. See #7554 . I haven't had time to investigate more closely, but I will probably close my open PRs. |
|
Some things are still relevant but it's less clear after leanprover/lean4#2644. My guess is that the jumping up the hierarchy by explicitly a data carrying instance at the top might be counterproductive since the improved defeq cache does a much more efficient job of discharging the checks in between and the fact we are forcing unfolded terms is hurting more. |
|
Ok, then feel free to close it. |
|
Coming here from issue triage: what's the current state of this PR? |
|
The issue about def-eq performance is no longer relevant after the lean3 PR. There were commits made to improve def-eq performance that referenced this note that are probably no longer important and could be reversed.There are still a bunch of TODOs in mathlib referencing this PR. The changes they are next to are probably no longer important and could be reversed. |
Quoting the docstring: `fast_instance% inst` takes an expression for a typeclass instance `inst`, and unfolds it into constructor applications that leverage existing instances. For instance, when used as ```lean instance instSemiring : Semiring X := sorry instance instRing : Ring X := fast_instance% Function.Injective.ring .. ``` this will define `instRing` as a nested constructor application that refers to `instSemiring`. The advantage is then that `instRing.toSemiring` unifies almost immediately with `instSemiring`, rather than having to break it down into smaller pieces. Related to #7432 Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
This method can improve speed, for example #7434, #7435, #7401, #6874, #7408, #7430, #7435, #7436
Sometimes it slows things dow though, e.g #7431