ordering of parents

Stream: mathlib4

[Matthew Ballard]

One thing I’ve noticed from looking at regressions with the left to right semantics is the following pattern

class NonUnitalSeminormedRing (α : Type*) extends Norm α, NonUnitalRing α,
  PseudoMetricSpace α where
  /-- The distance is induced by the norm. -/
  dist_eq : ∀ x y, dist x y = norm (x - y)
  /-- The norm is submultiplicative. -/
  norm_mul : ∀ a b, norm (a * b) ≤ norm a * norm b

which itself is ok. But becomes problematic when using existing instances to construct new ones.

Here many instances come from “Analysis-land” which means they involve Norm and PseudoMetricSpace fields and often involve some algebraic fields (e.g. Add)

When one builds the instance as

{ mainlyAnalysisButSomeAlg, purelyAlg with }

we end up doing some deep eta expansions on NonUnitalRing to use the algebraic fields from the first instance.

What should be done here?

• Be more disciplined?
• Move the algebra instances to the front? (for the class itself also?)
• Something else?

[Matthew Ballard]

Probably the depth of the nesting for a class should play a large factor in the ordering of parent classes (unless it is all data)

[Matthew Ballard]

Has anyone written a tool for listing the classes in mathlib by depth of extension?

[Matthew Ballard]

Here is some positive evidence for this ordering - from #10287

[Jireh Loreaux]

Matthew Ballard said:

• Something else?

One thing I've been keen on, but has met with some resistance in the past, is to separate the data fields in the algebraic hierarchy from those in the analysis hierarchy (almost) entirely, and then have mixins for the interactions between the two.

I think @Sébastien Gouëzel's usual rejoinder is something like (please forgive me if I get it wrong): but (Nontrivially)NormedFields are soooo common that it's better if we have an explicit class for these. In that case, I agree, and we can have a few overlaps (primarily just NormedField and variations thereof). But I think having all the duplication of {NonUnital}{Semi}Normed{Comm}Ring is overkill (especially because at some point I'm sure we'll want NonAssoc variants), and it certainly makes it harder to change assumptions.

This would have the benefit that you should in general be able to build these instances as:

{ purelyAnalysisData, purelyAlgData, interactionProps with }

[Yaël Dillies]

A more general approach would be to separate the data fields from the prop fields. Within a hierarchy, the data fields basically never change (eg in the algebraic hierarchy we get at most zero, one, add, sub, neg, mul, div, inv, nsmul, zsmul, qsmul, natCast, intCast, ratCast) while the prop fields accumulate in complicated ways.

[Yaël Dillies]

I'm claiming it's more general because if you apply this principle to analytic algebraic objects, you get something like (purelyAnalyticData, purelyAlgebraicData), (purelyAnalyticProps, purelyAlgebraicProps, interactionProps) and I think the resulting classes will be small enough that inference will be fast. If they are not, we can split them up into purelyAnalyticData, purelyAlgebraicData, (purelyAnalyticProps, purelyAlgebraicProps, interactionProps) or even purelyAnalyticData, purelyAlgebraicData, purelyAnalyticProps, purelyAlgebraicProps, interactionProps (this last case is like an "unbundled mixin" and has the advantage of not forcing us to write tons and tons of classes about all possible interactions).

[Yaël Dillies]

The problem with this approach of course is that variable declarations become longer. But since any given purelyAlgebraicProps class requires exactly one specific purelyAlgebraicData (by which I mean it's defined as class purelyAlgebraicProps (α) [purelyAlgebraicData α] ...), the variable declaration could automagically figure out the supremum of all purelyAlgebraicData assumptions needed by the purelyAlgebraicProps present within it, and add that supremum as an assumption.

[Yaël Dillies]

Probably for simplicity we'll need to tag purelyAlgebraicProps classes with the purelyAlgebraicData class they need.

[Kevin Buzzard]

We might be able to make more use of variable! to hide the issues, if this ends up spiraling out of control

[Moritz Doll]

Or notation for a collection of variables, i.e., instanceNotation Foo A := {Bar A, Baz A} and that variable [Foo A] is internally unfolded to variable [Bar A] [Baz A] (but printed as [Foo A] in the info view). That would also make something like [IsROrC k] [HilbertSpace k E] possible.

[Kyle Miller]

variable! supports something like that, but it eliminates itself: https://github.com/leanprover-community/mathlib4/blob/49212605e40e9d9fcbcd9968ce362f91dad303ca/test/Variable.lean#L149-L160

Core has something called class abbrev that's sort of like what you're saying, and it's implemented as a class that can synthesize instances itself from instances for everything it extends.

[Matthew Ballard]

#7873 seems to follow the “Deeper structure first” philosophy and does clearly improve performance

[Jireh Loreaux]

Is there any way to do a small-ish test to see whether separating the data and prop fields as mentioned above would help or hinder performance? It would likely be a ton of work to do it across the whole library, but I'm not sure what a reliable proxy would be.

[Matthew Ballard]

We probably want a slim mathlib repo for testing things like this

[Kyle Miller]

In the draft lean4#5770, incidentally there's a feature behind a flag for making sure all parents are in a (locally) consistent ordering. It's computing the C3 linearization (as seen in languages like Python with it's MRO — method resolution order). If you're not familiar, if you imagine the set of all structures/classes as forming a poset with the has-parent relation, then it is trying to find a total order of the transitive closure of the parents of a given structure/class with the property that each list of direct parents are in order. The algorithm is a little more restrictive than that, but that's the idea.

This feature was motivated by getting dot notation to work reliably for structures with diamond inheritance, but if it helps mathlib get its parent classes in order, all the better.

In https://arxiv.org/pdf/2401.12740, Hivert and Thiéry note that for SageMath, maintaining parent orders that C3 can linearize is unscalable when you have thousands of classes. They have some tips though to make it work nonetheless. For example, we could support adding global constraints for some key classes (Add always comes after Mul, Module always comes after Ring, things like that) that would help. They also describe some tools for an algorithm to add in "non-direct parents" to guide C3 to a solution. We could also make our C3 suggest putting Prop parents after non-Prop parents.