inefficient projections

Stream: mathlib4

[Floris van Doorn]

When using the multiplication in a monoid, the current instance search chooses to go through MulOneClass, as can be shown by clicking on the * in the output of the following print:

import Mathlib.Algebra.Group.Defs

def foo {α} [Monoid α] (a b : α) : α := a * b

#print foo

This is not great. Monoid is declared as follows:

class Monoid (M : Type u) extends Semigroup M, MulOneClass M [...]

Since Semigroup and MulOneClass share a field (multiplication), this means that Semigroup is an actual field of Monoid, but MulOneClass is not: the One field and others are inlined (as can be seen with #print Monoid). This means that Monoid.toMulOneClass is not a projection, but an actual function that unpackages and repackages data. This could have performance issues for both unification and compilation of definitions. I have no idea whether we're talking about a 0.1% or a 10+% performance issue, but it's probably worth trying to fix it.

I think the easiest way to fix it is to make sure that all instance priorities are compatible with the order classes extend other classes. In this case, it would mean that Semigroup.toMul has a higher priority than MulOneClass.toMul (so that when looking for a Mul we're going in the SemiGroup path before trying the MulOneClass path). We can probably fix all cases by giving some instances manual priorities and maybe shuffling around some extend lines. It's probably best to ensure that this property holds using a linter (that checks for each structure whether the corresponding instances have compatible priorities), which I'm happy to write.

[Eric Rodriguez]

I wonder if this is related to the Ring.toNonAssocRing issue

[Eric Wieser]

This means that Monoid.toMulOneClass is not a projection, but an actual function that unpackages and repackages data. This could have performance issues for both unification and compilation of definitions.

Of course, in Lean3 old-style structure every typeclass instance through extend worked this way; so this is more of a possible optimization than a regression

[Floris van Doorn]

Oh, I think a linter like this will also solve the issues in lean4#2074, so this seems quite useful. Let me work on this.

[Eric Wieser]

My hunch is that no amount of extends reordering /priority tweaking can fully solve lean4#2074, and that we really need eta turned on for TC resolution.

[Eric Wieser]

Isn't there always going to be a diamond inheritance path that's possible, through which different constructions will necessarily take different paths around the diamond, which in turn unfold inner structures to a different depth?

[Eric Wieser]

For instance, IIRC for docs4#Semiring.toModule we require that everything that extends semiring "truly" inherits from Semiring, else we end up needing structure eta. But we have the same for docs4#Algebra.Id with CommSemiring, and could quite conceivably end up with something similar for Ring; and we can only make CommRing "truly" extend one of CommSemiring and Ring.

[Eric Wieser]

Maybe with your suggestion the performance implications of enabling TC eta in lean4#2074 are much less though.

[Floris van Doorn]

I maybe shouldn't have used the word "solve", but I think this can mitigate some of the issues.

[Floris van Doorn]

You're probably right that we also want to have structure eta turned on in many cases.

[Floris van Doorn]

Except that I don't think there is a way to change the instance priorities of automatically generated instances by the structure command.
The structure command adds the instances with default priority (here and here), and I don't think that there is a way to change the instance priority afterwards. In particular, running attribute [instance 10] ... doesn't affect the instance priority:

class A (α : Type) where
  (one : α)

class B (α : Type) extends A α where
  (two : α)

class C (α : Type) extends A α where
  (three : α)

class D (α : Type) extends B α, C α

attribute [instance 10] C.toA
def foo [D α] : A α := inferInstance -- still uses `C.toA`
#print foo

(to be more precise, the command attribute [instance 10] C.toA doesn't change the discrimination tree used to find instances).

[Floris van Doorn]

I opened lean4#2115 to track this.