Multi-source structure instance elaboration (lean4#2478)

Stream: lean4

[Kyle Miller]

(This is a continuation of discussion in the example (p : P) : Q := p takes 0.25s to fail! thread, but there's a broader discussion so I'll bring it up here.)

Re lean4#2478, I'm busy with the beginning of the quarter teaching a large class and getting seminar talk together for the CS department, but I'll have time soon-ish (the end of next week?) to get things moving. It's an important PR for optimization structure instance elaboration, which has large performance impacts on mathlib.

In case anyone can help me with some research, here are some questions:

1. What is the expected elaboration of a multi-source structure instance? I personally would have thought that ({s, t with} : C) would be as if the fields of s and then the fields of t were consulted in order. However, as Matt's examples show, this is not currently the case. Is that intentional, or an oversight with a previous eta optimization? Or maybe at some point these were generalized from single-source to multi-source?
2. How should elaboration of multi-source structure instances work? There are a few options:
   A. Fill fields using the sources in left-to-right order (and try to do this ~optimally, by fusing fields into compatible subobject projections when possible).
   B. Fill fields from any of the sources, by looking at all fields of C (including subobject fields) in a depth-first manner and using the first source that provides it (note: this means that earlier sources might not be consulted for a field they provide!).
   C. Declare that which field comes from which source is unspecified behavior, or, probably better, an error.
   In A and B, note that it only makes sense to use a subobject projection from a source if the destination structure has that subobject. Just to note a small complexity, when there are items in the with clause, this can inhibit using certain subobjects due to overlap.

My intent is that as part of merging lean4#2478 we have specified how this part of the language is supposed to work. It's an important part of the language for mathlib because it's how __ := ... spread notation is implemented. It's also important because I'd prefer that, if we change how elaboration works, we do it in one clean and well-justified break.

[Kim Morrison]

I think A (left-to-right), or erroring on ambiguity, are the two options that allow the user to have the simplest mental model.

[Eric Wieser]

What does "ambiguity" mean here? If two fields are defeq, presumably this doesn't count as ambiguous; but which one is used?

[Eric Wieser]

I think the problem is that there are two ways of talking about the fields of:

structure A where a : Nat
structure B extends A where b : Nat

Either the fields of B are [toA, b] (how .mk presents them) or [a, b] (the mental model we inherited from Lean 3), and the interpretation of left-to-right changes depending on which outlook you use.

[Eric Wieser]

I think this is just a thorn we have to deal with when using nested structures; just like we have to deal with the weird signature of .mk

[Kyle Miller]

Let's say "field" means [a, b], but with the understanding that there's actually a tree here with all of the subobject fields being remembered.

With your A and B, Lean allows

structure C where a : Nat

variable (c : C)
#check ({c with b := 0} : B)

That is, the fields of B can't just be [toA, b]. The illusion Lean aims to maintain is that B really does have two fields a and b.

[Kyle Miller]

With multi-source structure instances, this is allowed, following the mental model of drawing from sources left-to-right:

structure D where
  (a b : Nat)

variable (a : A) (b : B)
#check ({a, b with} : D) -- { a := a.a, b := b.b } : D

It currently does something completely different though if a subobject field matches:

#check ({a, b with} : B) -- { toA := b.toA, b := b.b } : B

I don't see why it couldn't give { toA := a, b := b.b } here, which is what I'd expect in the A option (left-to-right), or, if it can't figure out the optimization, at least { a := a.a, b := b.b } : B.

[Eric Wieser]

Kyle Miller said:

The illusion Lean aims to maintain is that B really does have two fields a and b.

This illusion is broken around:

• B.a hiding a B.toA.a term which will match lemmas about A.a
• the shape ofB.mk
• ⟨⟨a⟩, b⟩ notation
• lean4#2905

I'm not sure attempting to maintain it is helpful, since it somewhat amounts to pretending these traps don't exist.

[Eric Wieser]

Kyle Miller said:

I don't see why it couldn't give { toA := a, b := b.b } here,

Yes, and this is an easy fix; right now the PR does two passes searching for fields, but I think mixing them in a single pass would have this effect

[Mario Carneiro]

I think we should properly handle these fields as a tree, and the structure eta reduction trick should be a mere optimization. Here's a concrete algorithm that has the right specification and also avoids superfluous eta expansion where possible:

• The target struct S has fields arranged in a tree; our goal is to provide a "covering" of the tree by values. We don't actually look at the types here, only the field names are significant.
• First, use all the directly provided fields to fill the specified nodes. (Duplicates here are an error.)
• Then, go through the sources from left to right:
  • Loop over the fields / subfields in preorder. (The left-to-right order doesn't matter but we want to visit roots before leaves.)
  • For each field a of the source A, if a is completely uncovered (meaning a and all of its children are unassigned), cover it with a value from this source.
• If not all fields are covered, error.

[Mario Carneiro]

In the example above, this yields:

structure A where a : Nat
structure B extends A where b : Nat
variable (a : A) (b : B)
#check ({a, b with} : B) -- { toA := a, b := b.b } : B

[Mario Carneiro]

other examples:

structure A where a : Nat
structure B where (toA : A) (b : Nat) -- `a` is not a field of `B`
variable (a a' : A) (b : B)
#check ({a, b with} : B) -- b : B
#check ({a, b with toA := a'} : B) -- { toA := a', b := b.b } : B
#check ({a, b with toA.a := 1} : B) -- { toA := { a := 1 }, b := b.b } : B

[Kyle Miller]

Just to clarify, you're agreeing that option A (left-to-right) is the correct behavior, and you're giving a suggested algorithm, correct? (And "left-to-right" in your sub-bullet is referring about details of the preorder, and not the sources)

[Mario Carneiro]

yes

[Mario Carneiro]

It's also not really necessarily the real algorithm, it's for specification purposes. I think the real algorithm goes one field at a time instead of one source at a time (then again, this may be exactly the cause of the bug!)

[Mario Carneiro]

One oddity of this algorithm is that a parent field with no subfields is always considered covered, so it will never draw from any explicit sources, e.g

structure A
structure B extends A
structure C extends B with c : Nat
variable (b : B) (c : C)
#check {b with} -- { toA := {} } : B
#check {c with} -- c : C
#check {c with c := 1} -- { toB := { toA := {} }, c := 1 } : C

[Mario Carneiro]

Actually I take it back, a field with no subfields would be completely uncovered by the rules above, so the first source to provide the field will be used

#check {b with} -- b : B
#check {c with} -- c : C
#check {c with c := 1} -- { toB := c.toB, c := 1 } : C
#check ({c := 1} : C) -- { toB := { toA := {} }, c := 1 } : C

which looks like sensible behavior to me

[Matthew Ballard]

Thanks Kyle for this. I know you are busy with more important things.

I agree that "left-to-right" is the simplest mental model.

But I don't think that should be driving factor in this specification. I base my opinion off a couple things:

1. If the left-to-right model was at the top of users minds when building instances, I would expect a good deal more breakage in #9007 since the extra eta expansion of the source instances allows for more likelihood of overlap being exposed. I found exactly one such case in docs#sigmaCurryEquiv here. From looking at how users construct instances with multiple sources, my belief is that the vast majority of the time the thought process is "All of these cover all the fields I need. Lean put them together."
2. Ordering choices can seriously impact performance for structures in Lean 4. We basically have no concrete sense right now of the optimal way to order the parent classes across the library. Allowing ordering of the sources to play a large role invites problems like these.
3. There is another mechanism for users to specify fields, after the with. I understand the convenience if there are many fields you want to take from one particular source. But if you need to do this, it might be an indication to revisit the inheritance pattern for the structures are working with.

Taking these together, I think the sources before the with should be put together maximizing performance in unification and in a way that is robust to refactorings of ordering of parents. The user should only worry that they have covered all fields with their sources when reasoning. If they want a particular term for a field it should be supplied explicitly after the with.

[Matthew Ballard]

Eric Wieser said:

Kyle Miller said:

I don't see why it couldn't give { toA := a, b := b.b } here,

Yes, and this is an easy fix; right now the PR does two passes searching for fields, but I think mixing them in a single pass would have this effect

Yes this is a good idea. The fundamental issue with the current design is that toA is not a field of A.

[Matthew Ballard]

Mario Carneiro said:

yes

I am confused because this sounds very similar to what the current implementation is

[Mario Carneiro]

The model I described is not intended to diverge from what was proposed above it so much as to make it precise and answer all the edge case questions

[Mario Carneiro]

In particular it has the property that for any field or subfield, if multiple sources provide it then the left-most source is always the one that supplies the value

[Matthew Ballard]

I am probably being dense. But "what was proposed" to me is left-to-right and "current implementation" is top-down.

[Mario Carneiro]

there are aspects of both left to right and top down in both algorithms, I guess it's a matter of which loop you do first

[Matthew Ballard]

Yes, agree.

[Mario Carneiro]

but I think I would describe my algorithm as "left to right" in the sense you mean

[Matthew Ballard]

Right now we loop over the fields of the instance we want to construct and eta-expand if we cannot fill with projections from the sources.

[Matthew Ballard]

If multiple projections work, then the left-most is used via findSome?

[Mario Carneiro]

right, I agree that gives the wrong result when the second source provides a parent of some field from the first source

[Matthew Ballard]

Wrong in what way?

[Mario Carneiro]

Mario Carneiro said:

In particular it has the property that for any field or subfield, if multiple sources provide it then the left-most source is always the one that supplies the value

[Mario Carneiro]

this property is violated with that algorithm

[Matthew Ballard]

Perhaps I should re-read more carefully. But stepping back, I worry about the trade-offs of such a property in practice.

[Mario Carneiro]

structure A where a : Nat
structure B extends A where b : Nat
variable (a : A) (b : B)
#check ({ a, b with } : B)
-- currently: { toA := b.toA, b := b.b } : B
-- should be: { toA := a, b := b.b } : B

[Matthew Ballard]

Ok yes. I agree understand

[Mario Carneiro]

This is an easy mental model, it means you don't have to worry about subfields and can easily deduce where each thing comes from

[Mario Carneiro]

(It's also what I thought we implemented, and in lean 3 I think this is what you get)

[Matthew Ballard]

I agree that it is an easy mental model for those who make such considerations. But, in practice, I don't see that happening.

[Matthew Ballard]

Yeah, I am curious about Lean 3.

[Mario Carneiro]

For those who don't take the consideration you get option (C) - it is unspecified, don't do it unless all the fields are defeq and you don't care which is picked

[Mario Carneiro]

but when you do care it's good if the algorithm is predictable

[Matthew Ballard]

I think they would be fine with any choice

[Mario Carneiro]

or that

[Matthew Ballard]

I don't think C is good for the reason you just said

[Mario Carneiro]

I mean (C) is the "effective model" as understood by someone who doesn't learn the algorithm

[Matthew Ballard]

But there is a problem with attaching importance to the ordering when most people don't care in practice

[Mario Carneiro]

and the next level of understanding is that everything is treated like flat structures and the first one to supply each field wins

[Mario Carneiro]

which is the lean 3 algorithm, and also coincides with the algorithm I described (and Kyle's option A) up to structure eta applications

[Matthew Ballard]

I would argue the performance penalties in Lean 4 that we pay for mis-orderings by those who don't care outweigh this benefit. Especially when there is another mechanism to specify fields.

[Mario Carneiro]

If you supply fields, those take priority of course

[Mario Carneiro]

so it gives you a way to additionally control the behavior

[Matthew Ballard]

Right, why do we need two?

[Mario Carneiro]

but I think correct semantics is more important than performance, it's no good to get the wrong answer quickly

[Mario Carneiro]

but we can optimize under those constraints

[Matthew Ballard]

Did the semantics for structure inheritance change between the Lean 3 version you are referring to and Lean 4?

[Mario Carneiro]

it did, the example I just gave is a counterexample

[Mario Carneiro]

This looks very much like a bug

[Matthew Ballard]

Are we talking old style structures vs now?

[Mario Carneiro]

with new style structures in lean 3, we do get the same behavior as current lean 4

structure A := (a : nat)
structure B extends A := (b : nat)
variables (a : A) (b : B)
#check ({ ..a, ..b } : B) -- {to_A := b.to_A, b := b.b} : B

[Mario Carneiro]

with old style structures we get the sensible behavior

set_option old_structure_cmd true
structure A := (a : nat)
structure B extends A := (b : nat)
variables (a : A) (b : B)
#check ({ ..a, ..b } : B) -- {a := a.a, b := b.b} : B

[Matthew Ballard]

So it would be a bug in Lean 3 then?

[Matthew Ballard]

(that propagated)

[Mario Carneiro]

more or less

[Mario Carneiro]

I'm pretty sure the code was completely rewritten, but the abstract algorithm is the one at fault here

[Matthew Ballard]

I think that we need to see the performance impact of enforcing this invariant

[Matthew Ballard]

My experience mucking around timeouts makes me very concerned

[Mario Carneiro]

relative to your eta reduced version of the original algorithm, or relative to the current version?

[Eric Wieser]

(note that you can use lean3 to mark things as lean3 code, and in a few weeks they will lead to the lean3 playground)

[Mario Carneiro]

I think the eta reductions will cause the most obvious performance differences

[Matthew Ballard]

The current version. A more substantial rewrite is necessary to enforce this invariant. The PR in question perpetuates top-down as in current code.

[Matthew Ballard]

The scope of the PR is to avoid the eta expansion

[Mario Carneiro]

This algorithm is also eta reduced, it will have slightly fewer eta reductions than the original algorithm though

[Matthew Ballard]

Assuming that all users have intentionally ordered their sources

[Mario Carneiro]

Let me name the algorithms:

• A: Original algorithm
• AR: Your rewrite, with eta reduction
• BR: My algorithm / kyle's option A

AFAICT, A < BR < AR in terms of number of successful eta reductions, because AR prioritizes eta reduction over selecting from the right sources. So we would expect the performance numbers to look similar

[Eric Wieser]

Kyle Miller said:

My intent is that as part of merging lean4#2478 we have specified how this part of the language is supposed to work. It's an important part of the language for mathlib because it's how __ := ... spread notation is implemented. It's also important because I'd prefer that, if we change how elaboration works, we do it in one clean and well-justified break.

Given the performance benefits are so great for mathlib, from the perspective of user + CI time (and CO₂), I'd perhaps argue that preferring to merge a poorly-specified fix with refinement in a follow-up is preferable to waiting for a fully specified fix

[Mario Carneiro]

I'm pretty sure that sources are intentionally ordered in mathlib whenever they result in different defeqs

[Eric Wieser]

I think usually in mathlib when we're unsure of the defeq, we just override the field again, which breaks all the eta optimizations anyway

[Mario Carneiro]

not necessarily, you can override a parent field

[Matthew Ballard]

I think people tend to dump everything before the with

[Eric Wieser]

I mean that we currently do { a, b with a := a.a } if we're not sure whether a will be taken from a or b, and the difference matters

[Mario Carneiro]

Also note that as long as A and B have a common parent C which is the reason why they have common fields, it is C itself that will be selected so there is no performance cost to using BR over AR

[Mario Carneiro]

Eric Wieser said:

Given the performance benefits are so great for mathlib, from the perspective of user + CI time (and CO2), I'd perhaps argue that preferring to merge a poorly-specified fix with refinement in a follow-up is preferable to waiting for a fully specified fix

I agree with this. A > AR is a performance optimization, AR > BR is a bugfix

[Matthew Ballard]

Color me skeptical about performance impacts. I am happy to be proven wrong. Good sematics + good performance would be the best of all worlds

[Mario Carneiro]

The only cases where AR and BR even have different answers is when A / AR is picking the "wrong" result. Do we have any examples of this in the wild?

[Eric Wieser]

Eric Wieser said:

from the perspective of user + CI time (and CO2)

another consideration is preventing #8386 from rotting, which I believe depends on one of AR or BR being merged quickly

[Kyle Miller]

For reference, here's the Lean 3 implementation of structure instance elaboration: https://github.com/leanprover-community/lean/blob/f91b574c40ad862c5134d48995ad083fe48e4cd4/src/frontends/lean/elaborator.cpp#L2871

It looks like the loop is in create_field_mvars

[Kyle Miller]

@Matthew Ballard Could you remind me what the state of lean4#2478 is with respect to changing semantics? Are there still examples where it elaborates structure instance with different fields from the current algorithm?

If so, my large reservation with merging as-is is that for core, we don't change elaboration without it being well tested and carefully justified. There are plenty of programming uses of structure instances, and if there are any downstream projects that use multi-source structure instances, we might be silently causing the programs to evaluate differently. If the semantics are changing, I believe this warrants doing it just once.

On the other hand, if the semantics are the same, and if this is just an optimization, then it might be OK proceeding since at worst a proof might need to be fixed up.

[Kyle Miller]

Here's a short summary of the discussion so far as I'm understanding it:

1. Treating structures as flat records and filling fields from sources left-to-right is generally accepted as the "right" conceptual model. (Though Eric appears to disagree)
2. There are reservations that this might not necessarily give the optimal representation, and for mathlib getting the optimal representation may be more important than the "right" one.
3. There are no reservations about the need for representing structure instances more efficiently.

What if there were an option you could set where the structure instance elaborator would warn you if you have the sources in a non-optimal order? Or if it's non-optimal, suggest fields to include? With that sort of setting, maybe we could get nice semantics of 1 while perhaps satisfying @Matthew Ballard's concerns about 2?

[Matthew Ballard]

The PR follows the existing semantics as much as I understand them. Fill the structure instance top-down with the first occurrence that works (by name).

Currently, the algorithm only uses projections from the supplied source instances when it tries to match a missing field with something from the source. For example, if you have a:A in your source list and we are trying to fill toA then it will not use abecause it is not a projection of A.

The change, which is one-line, is to first run a search to see if the name of the field we are filling is the same as one of the supplied sources. If so, slot that in.

[Matthew Ballard]

Given the delicacy of elaboration, I made this as targeted as possible to allow a:A to fill toA and avoid the extra eta expansion coming from no match.

[Kyle Miller]

In particular, are there any concrete examples that you know of where the semantics differ? I shared an example that gave non-equal results for some recent-ish version of the PR, but you've change it in the meantime. (And just to make sure we're using words in the same way, and while I might be misusing the term, by "preserve semantics" in this context I mean "yields a result that's Eq to the previous algorithm's result". Defeq is even better, and with structure eta these should be the same.)

[Matthew Ballard]

Sorry. I thought you meant semantics in terms of initial discussion. The current PR version which takes the first that fits out of all sources and projections will in principle break some defeq’s (though I only found one such instance in mathlib).

I have a version in a branch which only fills with source if there is no overlap in a source. It is not tested for performance and would in principle still break defeq since we could have filled with something after it. One could make a version which fills only if there is no overlap with any other source. I am not sure of the utility of this.

It might be useful to consult someone else who was around when the behavior changed to understand the intention.

@Sebastian Ullrich what motivated the change in behavior in Lean 3 for structure instance elaboration?

[Sebastian Ullrich]

Which change specifically?

[Matthew Ballard]

Mario Carneiro said:

with old style structures we get the sensible behavior

set_option old_structure_cmd true
structure A := (a : nat)
structure B extends A := (b : nat)
variables (a : A) (b : B)
#check ({ ..a, ..b } : B) -- {a := a.a, b := b.b} : B

vs

[Matthew Ballard]

Mario Carneiro said:

with new style structures in lean 3, we do get the same behavior as current lean 4

structure A := (a : nat)
structure B extends A := (b : nat)
variables (a : A) (b : B)
#check ({ ..a, ..b } : B) -- {to_A := b.to_A, b := b.b} : B

[Matthew Ballard]

First source listed (left to right) with a field will fill it in elaboration of the instance.

[Sebastian Ullrich]

I doubt it was an intentional change. The code was basically rewritten.

[Matthew Ballard]

You would expect the left to right invariant to hold then?

[Eric Wieser]

Treating structures as flat records and filling fields from sources left-to-right is generally accepted as the "right" conceptual model. (Though Eric appears to disagree)

I think my claim is that while this model is perhaps "right" in the ideal sense, it's certainly not "right" in the sense of consistency with many other properties of new structures, and I think when the choices are "ideal but inconsistent and unperformant" vs "non-ideal but consistent and performant", the latter wins. Even with performance out of the picture, I think global consistency is better than local idealness.

[Matthew Ballard]

That sounds like my concerns but better stated.

[Matthew Ballard]

(Aside: I’m heading to Berkeley now so might not be able to engage much until later tomorrow)

[Eric Wieser]

If having the ideal "flat" semantics is really important to the user, then the most reliable way to get them consistently would be to let that user truly use flat structures; something like lean4#2940, though I don't claim that we are at the point where we should seriously consider merging it.

[Kyle Miller]

What do you think about my suggestion to have an option that can warn about ill-performing structure instances? (That wouldn't be for the initial PR, but it could be a later extension.)

[Eric Wieser]

That sounds great, though I'm not sure we have enough data for certain to tell if a structure is ill-performing by construction

[Eric Wieser]

This might make sense as a (Std-style) linter; or maybe as motivation for refactoring linters upstream so that they can inspect the elaborated declaration

[Kyle Miller]

"ill-performing" might just mean "the any-source greedy subobject algorithm would give a different result" (I don't know what to call it -- it's the one that you and Matt have been suggesting).

[Kyle Miller]

I'd like to say that I don't think it's fair to characterize this in terms of consistent vs inconsistent. The main interface to structures are the fields, and every structure also comes with projections to everything it extends. It's supposed to be an implementation detail how it packs the fields into nested objects. Sure, the .mk constructor exposes this detail, as does anonymous constructor notation, but the interface for constructing structures is structure instance notation. We could hide x.toA.a by having the structure command define projections for each field, if that's something we really wanted. There's also a leak where structure instances can't set parent projection fields that aren't true fields, but that could be fixed.

I'm having a hard time seeing how drawing fields from sources in a complicated order depending on the exact details of the orderings of all the extends clauses in a hierarchy of structures (and depending on the exact algorithm that is used to process these) could be characterized as "consistent", other than the mere fact that it's consistent with how the implementation details of new structures sometimes leak.

If we don't do the "ideal" left-to-right algorithm, then that limits our ability to have features that adjust how structures are laid out. Let's say we have an extension for flat structures -- wouldn't you want to be able to switch a particular structure over without worrying whether all the structure instances in your codebase now might mean something different?

[Kyle Miller]

Put another way, structure instance notation should be invariant to the actual structure layout. You should be able to refactor your structures all you want (factor out a common sub-structure with extends, reorder the extends clauses, switch the structure layout algorithm) and you shouldn't have to worry about whether structure instances will evaluate to something different -- may it be because the algorithm is the "idea" one or because the changes signal an error that needs to be corrected.

Something that just occurred to me is that potentially computationally irrelevant fields (proofs and types) could be allowed to come from any source. That's an optimization though.

[Eric Wieser]

Something that just occurred to me is that potentially computationally irrelevant fields (proofs and types) could be allowed to come from any source.

I think this is risky for Types; computational irrelevance (Subsingleton?) isn't enough to ensure definitional equality

[Kyle Miller]

Oh right, I was thinking proofs first and then generalized too far without thinking.

[Matthew Ballard]

Looks like I’ll have to take back my reservations

[Matthew Ballard]

#9843 has the changes to mathlib for left to right

[Matthew Ballard]

Here are the changes to get full left to right elaboration on all structure instances giving the benchmark results above. You can use the existing loop over fields of the target structure but enforce that you are only allowed to choose a projection of a supplied instance if its fields don’t overlap with any fields of a supplied instance listed before it.

The code can probably cleaned up a little. Suggestions are welcome.

A more subtle issue is: what counts as a field. For example

structure A where
    x : Nat
    y : Nat

structure B where
    toA : A
    z : Nat

structure C extends A where
    z : Nat

What are the fields of B here? Are they the same as C?

[Kyle Miller]

If the fields of B are accidentally the same as C right now, that might be an OK bug for now. I don't think they're meant to have the same fields. Subobject projections ought to only be subobject projections if they are declared so.

[Matthew Ballard]

You can probably guess the results of getStructureFieldsFlattened on each

[Matthew Ballard]

[`toA, `z] — B
[`x, `y, `z] — C

[Matthew Ballard]

Should the following work?

def bar (s : B) : C := {s with}

[Kyle Miller]

That's a good boundary case. I think it's ok if it works, but it doesn't need to, and maybe it shouldn't.

[Matthew Ballard]

Amusingly this is an explicit test in the test suite. :)

Long update incoming.

[Matthew Ballard]

There are 5 different toolchains now

0. Status quo
1. Current content of lean4#2478
2. Implement left-to-right semantics with the previous test failing
3. Implement left-to-right semantics with the previous test working
4. 3 + reduce even more etas (explained below)

[Matthew Ballard]

If you want to play with them, here are the toolchains labels

1. leanprover/lean4:lean-pr-testing-2478
2. mattrobball/lean4:leftRight-24-01-18
3. mattrobball/lean4:leftRightDeep-24-01-20
4. mattrobball/lean4:leftRightDeepExtra-24-01-22-2

[Matthew Ballard]

We have working copies of mathlib for each

1. #9007
2. #9843
3. #9868
4. #9895

[Matthew Ballard]

To illustrate the difference in behavior, here is a test in 3 and 4

structure A where
  x : Nat

structure B where
  x : Nat
  y : Nat

def foo (a : A) (b : B) : B := {a, b with}

def boo (a : A) (b : B) : B := {b, a with}

structure C extends B

def baz (a : A) (b : B) : C := {a, b with}

def biz (a : A) (b : B) : C := {b, a with}

def faz (a : A) (c : C) : C := {a, c with}

def fiz (a : A) (c : C) : C := {c, a with}

[Matthew Ballard]

For status quo, we have

def foo : A → B → B :=
fun a b => { x := a.x, y := b.y }
def boo : A → B → B :=
fun a b => { x := b.x, y := b.y}
def baz : A → B → C :=
fun a b => { toB := { x := a.x, y := b.y } }
def biz : A → B → C :=
fun a b => { toB :=  {x := b.x, y := b.y} }
def faz : A → C → C :=
fun a c => { toB := c.toB }
def fiz : A → C → C :=
fun a c => {toB := c.toB }

[Matthew Ballard]

Things to note:

• biz has one extra eta expansion
• boo has two extra eta expansions
• fiz has one extra one
• foo satisfies the left to right semantics but only because of the eta expansion. faz doesn’t have the extra eta expansion and does not satisfy it

[Matthew Ballard]

For lean4#2478, we have

def foo : A → B → B :=
fun a b => { x := a.x, y := b.y }
def boo : A → B → B :=
fun a b => { x := b.x, y := b.y}
def baz : A → B → C :=
fun a b => { toB := {b }
def biz : A → B → C :=
fun a b => { toB :=  b }
def faz : A → C → C :=
fun a c => { toB := c.toB }
def fiz : A → C → C :=
fun a c => { toB := c.toB }

[Matthew Ballard]

We eliminate one source of eta expansion. When populating the structure fields, currently only fields of the supplied instances are used, not the instances itself. Left to right semantics are now completely broken.

[Matthew Ballard]

For 2, we have

def foo : A → B → B :=
fun a b => { x := a.x, y := b.y }
def boo : A → B → B :=
fun a b => { x := b.x, y := b.y}
def baz : A → B → C :=
fun a b => { toB := { x := a.x, y := b.y } }
def biz : A → B → C :=
fun a b => { toB :=  b }
def faz : A → C → C :=
fun a c => { toB := c.toB }
def fiz : A → C → C :=
fun a c => {toB := c.toB }

[Matthew Ballard]

We have full left to right semantics and eliminate the same source of eta expansion when possible

[Matthew Ballard]

3 is the same as 2. except the following works

structure A where
  x : Nat

structure B extends A where
  y : Nat

structure C where
  toA : A
  y : Nat

example (c : C) : B := {c with}

[Matthew Ballard]

4 gives

def foo : A → B → B :=
fun a b => { x := a.x, y := b.y }
def boo : A → B → B :=
fun a b => b
def baz : A → B → C :=
fun a b => { toB := { x := a.x, y := b.y } }
def biz : A → B → C :=
fun a b => { toB := b }
def faz : A → C → C :=
fun a c => { toB := { x := a.x, y := c.toB.y } }
def fiz : A → C → C :=
fun a c => c

[Matthew Ballard]

This eliminates the second source of eta expansions in boo and fiz Currently the algorithm is unable to correctly account for the case where a projection of a supplied instance (or a source instance itself) is a term whose type is the desired structure

[Matthew Ballard]

We could of course use the change from 3->4 with 1 or 2 also.

[Matthew Ballard]

The main (only?) concern about left to right semantics was the performance impact. Here are the changes in instructions over all of mathlib (you can find fuller reports from the bot on the PRs)

1. -4.3T
2. -3.8T
3. -3.8T
4. -3.9T

[Matthew Ballard]

1 indeed offers the greatest speed up while 3->4 is an improvement but not of the same magnitude.

[Matthew Ballard]

Some tests in the test suite need bumps to their heartbeat limit for 2-4. Sorry, I got things mixed up here. Bumps aren’t needed at all assuming the instances are ordered correctly.

[Matthew Ballard]

Another important difference is the diff size from the status quo for the 4 options.

[Matthew Ballard]

The relevant portion of the diff is src/Lean/Elab/StructInst.lean

[Matthew Ballard]

1. Diff this is effectively a one line change

[Matthew Ballard]

2. Diff We still try to fill the fields in a top down manner but we only allow us to use the first the list whose fields overlap with the field we are trying to fill.

[Matthew Ballard]

3. Diff In addition to 2, we need to consider fields of fields that are not subobjects. So we write a function that returns those and use that to compare fields instead

[Matthew Ballard]

4. Diff To remove the extra eta at the top of the desired structure, we add an argument to docs#Lean.Elab.Struct which we fill when one of the sources has a projection (or itself) that has the correct type and

• no instance before it overlaps in fields
• the user has not supplied any values for the fields after the with (eg x := 1)

[Matthew Ballard]

So these are progressively less surgical

[Matthew Ballard]

You can check the diffs for the mathlib PRs but 1 has the largest number of files touched by a decent margin. The change in 4 breaks some anti-patterns like

def one : One Nat := { one := 1 }

def one’ : One <| Option Nat := { one with }

[Matthew Ballard]

@Kyle Miller what do we want to pursue here?

[Kevin Buzzard]

Thanks so much for this very thorough examination of this subtle issue!

[Matthew Ballard]

Thanks! I should say I would like to hear perspectives from anyone who wants to share.

[Matthew Ballard]

One thought I forgot to state regarding performance. It is not that the concerns of orderings are un-warranted. Take a look at docs#NormedDivisionRing.induced

class NormedDivisionRing (α : Type*) extends Norm α, DivisionRing α, MetricSpace α where
  /-- The distance is induced by the norm. -/
  dist_eq : ∀ x y, dist x y = norm (x - y)
  /-- The norm is multiplicative. -/
  norm_mul' : ∀ a b, norm (a * b) = norm a * norm b

def NormedDivisionRing.induced [DivisionRing R] [NormedDivisionRing S] [NonUnitalRingHomClass F R S]
    (f : F) (hf : Function.Injective f) : NormedDivisionRing R :=
  { NormedAddCommGroup.induced R S f hf, ‹DivisionRing R› with
    norm_mul' := fun x y => by
      show ‖f (x * y)‖ = ‖f x‖ * ‖f y‖
      exact (map_mul f x y).symm ▸ norm_mul (f x) (f y) }

Here the fields of the first provided instance NormedAddCommGroup.induced go deep in the constructor for DivisionRing using the left to right semantics.

It seems that mathlib just doesn’t have as many such examples as one (I) might think. You can find more by looking for regressions in instructions in the benchmark results in the PRs for 2-4.

[Eric Wieser]

I have a refactor PR in progress that changes the definition of Normed* so as not to repeat dist_eq everywhere, which might make your comment above moot

[Matthew Ballard]

Maybe. Here it is taking the NormedAddCommGroup.toAddMonoid and using it to build a DivisionRing R instead of just using the DivisionRing R instance as it does now. Since AddMonoid is pretty deeply nested in DivisionRing this creates a much larger term.

[Eric Wieser]

This seems like an argument for a with_optimal_order or something instead of with

[Eric Wieser]

...which in mathlib is probably the order we always want anyway

[Sébastien Gouëzel]

If core goes for 2 or 3 or 4, will it be possible to implement a linter that would warn us of a suboptimal ordering in instance declaration?

[Kyle Miller]

Update: version 2 was just merged and should appear in the next Lean release. (Thanks @Matthew Ballard!)

[Kyle Miller]

One thing we're considering for a next step is to make structure instances better at trying to synthesize instances to fill in the remaining fields. Right now it only tries this for parent structures that end up with an actual subobject field, but we could try other parents too. Maybe this accounts for many uses of __ := in mathlib? If so, since typeclass instances are supposed to be canonical, this might be like some form of "with_optimal_order".

[Riccardo Brasca]

Sébastien Gouëzel said:

If core goes for 2 or 3 or 4, will it be possible to implement a linter that would warn us of a suboptimal ordering in instance declaration?

This seems like a key point: in practice order matters, right?

[Matthew Ballard]

The desire for a such a linter came up again (somewhere...search is failing me) recently. I am happy to write one but the main mental hurdle is that it is near trivial for me to tweak the core files and run a modified toolchain over the library to identify where things are "out of order". But I have little idea of how to plug this into the existing linter frameworks and not much time to figure it out.

[Yaël Dillies]

Here is one place it came up: https://github.com/leanprover-community/mathlib4/pull/11485#discussion_r1529867450