should nsmul have a default value?

Stream: mathlib4

[Floris van Doorn]

In #6262 @Eric Wieser removed the default values for the fields nsmul and zsmul, and @Patrick Massot and I have been unhappy about this. The PR description doesn't provide a good reason for doing so, but the PR does provide some nice speedups (was this because of giving a better value of these fields in some of the structures?)

I am happy to have a linter in Mathlib that forces users to write these fields. I just think that when teaching new users about structures, it is a giant distraction to have to explain them why nsmul is a field of an abelian group and what nsmulRec is. I don't want to explain what diamond issues are minutes after I explained what type-class inference is.

I'm starting a discussion here because of the open PR #12608. Related links: #11262 and Zulip thread

[Eric Wieser]

The speedups are likely because previously default values for nsmul were computed in terms of other fields, and this meant the definition of add and zero ended up duplicated in every instance.

[Eric Wieser]

If this is a burning issue causing immediate frustration in a course, I don't mind if we temporarily restore the default value while we work this out

[Eric Wieser]

(but let's not revert the PR, since that also added some TODOs downstream of things we actually want to fix)

[Eric Wieser]

Eric Wieser said:

the definition of add and zero ended up duplicated in every instance.

A demo of that:

structure Foo where
  foo : Nat

structure Bar extends Foo where
  bar : Nat
  foo := bar + 1

def demo : Bar where
  bar := 2 + 3 + 4 + 5 + 6

#print demo -- `2 + 3 + 4 + 5 + 6` is repeated

[Yaël Dillies]

Does that mean we need a structure Group.Core/Group.MinimalAxioms that does not contain any default field, and which is then extended by Group?

[Eric Wieser]

I suspect that makes things more confusing

[Eric Wieser]

What we could do is refactor docs#Group.ofMinimalAxioms to be instance Group.MinimalAxiomatization.toGroup, with the idea that instance : Group.MinimalAxiomatization G where ... is much nicer notation-wise than instance : Group G := Group.ofMinimalAxioms _ _ _ _

[Yaël Dillies]

Actually nevermind my solution does not help:

structure Foo where
  foo : Nat

structure Bar.Core where
  bar : Nat

structure Bar extends Bar.Core, Foo where
  foo := bar + 1

def demo : Bar where
  bar := 2 + 3 + 4 + 5 + 6

#print demo -- `2 + 3 + 4 + 5 + 6` is repeated

[Eric Wieser]

I think the gain arises from giving the repeated term a name, rather than elaborating it twice

[Eric Wieser]

In #6262, this manifests as declaring lots of Zero and Add instances before declaring the AddMonoid instance. It's possible this change is a performance improvement irrespective of whether a default is used for nsmul.

[Eric Wieser]

Certainly, restoring the default value will not affect performance in mathlib, as the performance increase was gained at the locations which relied upon this default; and all such locations no longer rely on it.

[Eric Wieser]

(it may of course result in worse future performance as new code is written to rely upon it again)

[Yaël Dillies]

Eric Wieser said:

I think the gain arises from giving the repeated term a name, rather than elaborating it twice

Indeed

import Mathlib.Tactic.Common

structure Foo where
  foo : Nat

structure Bar.Core where
  bar : Nat

structure Bar extends Bar.Core, Foo where
  foo := bar + 1

def demo : Bar.Core where
  bar := 2 + 3 + 4 + 5 + 6

def demo2 : Bar where
  __ := demo

#print demo2 -- `2 + 3 + 4 + 5 + 6` is not repeated

[Yaël Dillies]

Eric Wieser said:

What we could do is refactor docs#Group.ofMinimalAxioms to be instance Group.MinimalAxiomatization.toGroup, with the idea that instance : Group.MinimalAxiomatization G where ... is much nicer notation-wise than instance : Group G := Group.ofMinimalAxioms _ _ _ _

This sounds like a solution worth trying, except for the fact that

1. We're effectively giving up on default field values (maybe not so bad given that their design seems fundamentally broken)
2. This only works if there are not too many default fields in your structure. In general, if there are $n$ default fields (added by the typeclass, ie that are not in parent typeclasses), you need $2^n - 1$ "MinimalAxioms" typeclasses

[Eric Wieser]

I think my claim is that actually there are only two extremes we care about:

• Make things as simple as possible for pedagogical reasons (the minimal axioms)
• Make things as verbose as possible for instance coherence reasons (the mathlib "what are all these fields for?" approach)

[Yaël Dillies]

I tend to agree

[Eric Wieser]

Obviously the ideal situation is that we only have one spelling for the two extremes, and a linter to enforce the strict one