RFC: Naming structure parent projections

[kmill]

Summary

Modify the structure syntax to be in the form

structure IDENT BINDER* [: TYPE]? [extends [[IDENT :]? TYPE]*]? where FIELDS

1. The structure resultant type is moved to before the extends clause.
2. The ident prefixes in the extends clause are used to override the default parent projection names.

Motivation

Currently, there is no way to control the field names used for parent projections. Lean tries to automatically name parent projections using the following algorithm: if the parent has type S .., then it uses the first name among toS, toS_1, toS_2, toS_3, ... that is unused. The parent projections are not meant to be pure implementation details, so the fact that projection might use a number is less-than-ideal.

Furthermore, is possible to get into situations where this naming scheme fails. For example, suppose we have two structures with the same name in different namespace and then define

structure B extends NS1.A, NS2.A

This gives parent projections B.toA and B.toA_1. If you also have

structure C extends NS2.A
structure D extends B, C

then there's a field conflict on the C parent:

parent field type mismatch, field 'toA' from parent 'C' has type
  NS2.A : Type
but is expected to have type
  NS1.A : Type

A way to fix this is to let users specify the name of the parent projection:

structure B extends toA1 : NS1.A, toA2 : NS2.A

However, there is a syntax ambiguity with this solution. Another parse is that toA2 is a parent and NS2.A is the resultant type of B. This is clearer in the following:

structure S2 extends S1 : Type

Changing the syntax so that the resultant type comes before the extends clause would fix this.

structure S2 : Type extends S1

Proposal

First, we move the resultant type to come before the extends clause. For migration purposes, we can insert an additional resultant type parser into the the end of the extends clause itself, which we can use to detect uses of the old syntax (when the parent is not an ident) and raise a warning with migration suggestions.

Second, we modify the parent field naming algorithm. For parent S .., we now use toS as the default name for the projection. If this name is already in use, we throw an error suggesting that the user use the toCustomS : S .. syntax.

In the structure elaborator, we also add checks that the projection matches the name of the projection as given by other parent classes.

User experience

Putting the resultant type before extends is its natural place. The elaboration order for structures are binders, resultant type, parents, and then fields. The parents have no bearing on the type of the type constructor, and they are more like fields.

This location of the resultant type is also less confusing, since we can read off the binders and resulting type and know what the type constructor's type is, without needing to ignore the extends clause.

This change also opens up the possibility to write structure declarations in forms such as

structure S (x : X) : Type
extends P where
  a : Nat

Having the ability to name parent projections is a positive change. Having projection names also makes the extends clause closer to the syntax for fields.

Beneficiaries / Maintainability

This RFC comes from core Lean development. The primary purpose is to simplify the parent projection naming algorithm, so that it does not depend on random details of how parents are represented in the structure: now it's simply toS (without a number) or the user-supplied name.

A benefit will be that it should be easier to make all parents provide instances when elaborating the fields of a structure. Currently only subobject fields are available.

Drawbacks

• This is a breaking change to the syntax.
• Some parent projections will now need explicit names now.

Unresolved questions

This RFC does not add modifiers to the extends syntax. It makes sense making parent projections be protected or private, but it is unclear whether these modifiers are meant to apply to the fields being included as well.

Community Feedback

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Naming.20.60structure.60.20parent.20projections/near/499989993

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.

[nomeata]

I'd indent it like

structure S (x : X) : Type
extends
  P
  Q
where
  a : Nat

The arguments for putting the resultant type first are quite convincing.

Did you encounter cases in the real where there are multiple parent objects with the same base name?

[kmill]

Did you encounter cases in the real where there are multiple parent objects with the same base name?

Yes, there are a few cases of it in mathlib. For example, there's Hom that appear in a few namespaces, each extending the last.

[david-christiansen]

This syntax seems like a clear improvement, especially because it enables naming parent projections.

Do we have a sense of the impact on actual code in the wild? Can we provide a quickfix to update the syntax with a single click for a release or two, at least for many cases? After all, neither Type u nor Prop is a structure, so it should be fairly straightforward to catch instances of the old syntax.

[kmill]

@david-christiansen You can see the mathlib impact here: leanprover-community/mathlib4@nightly-testing...lean-pr-testing-7100

The PR has code to look for p : T where T isn't a structure, and it gives an error with an expanded error message. It also has a fallback parser in case p isn't an identifier. The errors aren't fully enabled yet, since I need a stage0 update. A 'try this' would be nice.

[david-christiansen]

I'm totally convinced - this is great!

[kmill]

Completed by #7100