Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

RFC: tweak structure instance elaboration to avoid un-needed eta expansion #2451

Closed
mattrobball opened this issue Aug 23, 2023 · 1 comment · Fixed by #2478
Closed

RFC: tweak structure instance elaboration to avoid un-needed eta expansion #2451

mattrobball opened this issue Aug 23, 2023 · 1 comment · Fixed by #2478
Assignees
Labels
Mathlib4 high prio Mathlib4 high priority issue

Comments

@mattrobball
Copy link
Contributor

mattrobball commented Aug 23, 2023

Currently, we have the following behavior for structure instance elaboration

structure A where 

structure B extends A where 

def a : A := sorry 

def b : B := { a with } 
#print b 
-- def b' : B :=
-- let src := a;
-- { toA := { } } <- There is an extra eta expansion for the `toA` field: 

I believe it would be advisable to change this to the following behavior

structure A where 

structure B extends A where 

def a : A := sorry 

def b : B := { a with } 
#print b 
-- def b' : B :=
-- let src := a;
-- { toA := src } <- There is no eta expansion for the `toA` field: 

The extra eta expansion is due to the following: the function mkProjStx? will not apply when the arguments are _ `A `toA as `toA is not a field of `A.

The change in behavior can be achieved by adding two lines to the function addMissingFields here:

if let some stx := s.source.explicit.find? (·.structName == substructName)|>.map (·.stx) then
  addField (FieldVal.term stx)

This accounts for the case where the projection is exactly to the type of an explicit source.

User Experience: How does this feature improve the user experience?

There is no extra eta expansion when constructing fields which are also fields of the explicit sources. This change makes the behavior more uniform and therefore reduces mental overhead for the user.

Furthermore, there is a performance penalty for the extra eta expansion. While small for a single instance, things can snowball when the pattern is nested. The expanded term forces unfolding during unification when otherwise it would not be necessary.

Beneficiaries: Which Lean users and projects do benefit most from this feature/change?

The largest benefit is for the libraries with deeply nested type class hierarchies, so Mathlib.

In leanprover-community/mathlib4#6759 I benchmarked Mathlib with a toolchain containing this change plus some complementary changes directly to Mathlib. The changes were overall very positive including a 4% reduction to total CPU instructions and dramatic improvements in many files.

Furthermore, at least one example of a serious timeout in algebraic hierarchy presented on Zulip has been completely eliminated.

Community Feedback: Have you sought feedback or insights from other Lean users?

This arose from multiple discussions on Zulip about performance problems in Mathlib, especially in the algebraic hierarchy. It bubbled up already in a separate issue #2387.

Maintainability: Will this change streamline code maintenance or simplify its structure?

Given the simplicity of the change, I would not expect additional maintenance burden.

I have a branch on my fork with this change plus a simple test (as above) to document the behavior and am ready to submit a PR. Looking forward to hearing feedback!

@kim-em kim-em added the Mathlib4 high prio Mathlib4 high priority issue label Aug 24, 2023
@kim-em kim-em self-assigned this Aug 24, 2023
@kim-em
Copy link
Collaborator

kim-em commented Aug 25, 2023

I made a Mathlib-free minimisation of a "real world" example from Zulip at https://gist.github.com/semorrison/784edf9e5ccc02f83ce5707cad59ca51. (To be clear, this example from Zulip has possible workarounds. Nevertheless this class of slow performance is being hit all over Mathlib.) The minimisation is quite long, but I think will be okay as a test. The final statement in this test fails on master unless you put synthInstance.maxHeartbeats up to 40000, but succeeds with Matthew's linked branch with set_option synthInstance.maxHeartbeats 500, so for problems like this is at least a 60x speedup!

github-merge-queue bot pushed a commit that referenced this issue Feb 1, 2024
…s in structure instance elaboration (#2478)

Modifies the structure instance elaborator to
1. Fill in missing fields from sources in strict left-to-right order. In
`{a, b with}`, sometimes the elaborator
would ignore `a` even if both `a` and `b` provided the same field,
depending on what subobject fields they had.
2. Use the sources, or subobjects of the sources, to fill in entire
subobjects of the target structure as much as possible.
Currently, a field cannot be filled directly by a source itself
resulting in the term being eta expanded.
This change avoids this unnecessary and surprisingly costly extra eta
expansion.

Adds two new tests to illustrate the performance benefit (one courtesy
@semorrison). These are currently failing on master and succeed on this
branch.

There is one additional test to exercise the changes to the elaboration
of structure instances.

Changes to make mathlib build are in leanprover-community/mathlib4#9843

Closes #2451
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Mathlib4 high prio Mathlib4 high priority issue
Projects
None yet
2 participants