RFC: `@[flat]` annotation for names in the `extend` clause of a structure

[eric-wieser]

Proposal

What?

When working with a structure hierarchy like

structure A where a : Unit
structure B extends A where b : Unit
structure C extends A where c : Unit
structure D extends B, C where

the type of D.mk is asymmetric:

D.mk (toB : B) (c : Unit) : D

More precisely, the representation of D is to embed an entire B structure, but then only take the parts of the C structure that do not overlap with B, namely c : Unit.

I have no doubt that this behavior is useful in some circumstances, but in situations where a symmetric API is more important than performance, this behavior is annoying.

Let's imagine that the symmetric API we want is D.mk (toA : A) (b c : Unit). Right now, there are the following workarounds to achieve that

1. Write the type of D manually without extends:

   structure A where a : Unit
   structure B extends A where b : Unit
   structure C extends A where c : Unit
   structure D extends A where
     b : Unit
     c : Unit
   
   -- user has to write this boilerplate
   def D.toB (d : D) : B := { toA := d.toA, b := d.b }
   def D.toC (d : D) : C := { toA := d.toA, c := d.c }

   This boilerplate can be rather a burden, epsecially since the naive := { d with } approach performs unwanted eta-expansion
2. Use the hack from https://arxiv.org/abs/2306.00617 §4.2, which exploits the 'avoid overlaps' rule to our advantage, as

   structure DFlatHack where
   
   structure A where a : Unit
   structure B extends DFlaHack , A where b : Unit
   structure C extends DFlatHack, A where c : Unit
   structure D extends DFlatHack, B, C where

   which gives us D.mk (toDFlatHack : DFlatHack) (toA : A) (b c : Unit) : D, where the first argument is vacuous and can always be passed as ⟨⟩.

In Lean 3 we had set_option old_structure_cmd true; but this was a bad design because it did not allow parent structures to selectively be flattened (among other reasons).

The proposal is to remove the need for a hack here, such that the user can write

structure A where a : Unit
structure B extends A where b : Unit
structure C extends A where c : Unit
structure D extends @[flat] B, @[flat] C where

or any other reasonable syntax.

How?

The presence of flat simply means "skip the overlapping fields check, and behave as if the fields overlap"; that is, a check for the syntactic marker would be added to the conditions here:

lean4/src/Lean/Elab/Structure.lean

Lines 423 to 428 in 57e2391

	if (← findExistingField? infos fieldParentStructName).isSome then
	-- See comment at `copyDefaultValue?`
	let expandedStructNames := expandedStructNames.insert fieldParentStructName
	copyFields infos expandedStructNames fieldType fun infos nestedFieldMap expandedStructNames => do
	let fieldVal ← mkCompositeField fieldType nestedFieldMap
	copy (i+1) infos (fieldMap.insert fieldName fieldVal) expandedStructNames

lean4/src/Lean/Elab/Structure.lean

Lines 479 to 483 in 57e2391

	if let some existingFieldName ← findExistingField? infos parentStructName then
	if structureDiamondWarning.get (← getOptions) then
	logWarning s!"field '{existingFieldName}' from '{parentStructName}' has already been declared"
	copyNewFieldsFrom view.declName infos parentType fun infos => go (i+1) infos (copiedParents.push parentType)
	-- TODO: if `class`, then we need to create a let-decl that stores the local instance for the `parentStructure`

Why?

• Nested structures are involved in frequent peformance issues in mathlib (for example, RFC: tweak structure instance elaboration to avoid un-needed eta expansion #2451)
• Nested structures break symmetries in unfortunate ways for things like RingHom, which has to pick between MonoidHom and AddMonoidHom as it's "main" parent. This affects the shape of the constructor, the simp lemmas about it, and adds ugly additional angle brackets to anonymous constructors

In both cases, having a @[flat] attribute would make it vastly easier to perform performance and API experiments in mathlib to work out where nested structures help, and where they're a hindrance.

Community Feedback

Mario originally proposed this syntax here.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[mattrobball]

Having concrete data on which patterns help where in mathlib would be very helpful.

[eric-wieser]

In both cases, having a @[flat] attribute would make it vastly easier to perform performance and API experiments in mathlib to work out where nested structures help, and where they're a hindrance.

In #2940, I add a flat keyword (easier than new @[flat] notation), which allows us to investigate the effect of this in Mathlib.
A mathlib toolchain that builds against this version can be found in leanprover-community/mathlib4#8977.

[eric-wieser]

Some initial data: used on only the HomClass classes (a minimally invasive change), this provides a 2.5% wall clock boost for Mathlib.