algebraic hierarchy

Stream: general

[Jeremy Avigad]

I am picking up here on the discussion in visualizations (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/visualizations/near/177991983) but I renamed the thread. I'd like to expand on my concerns about our coding of the algebraic hierarchy.

Recently I went back to look at the Mathematical Components library, and I was struck by how carefully the library is designed to avoid any search at all when it comes to working with structures. The algebraic hierarchy is mostly here:

https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v
https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssrnum.v

Not even notation is overloaded. When the "nat scope" is in effect, * means multiplication on nat. When the "ring scope" is open, * means multiplication in a ring structure. There are gadgets that make it more palatable to use natural numbers and rings at the same time. But whenever you want to use multiplication in something that has a ring structure, there is always a one step path (a "canonical structure" hint) that will get you there from the type in hand to the relevant ring structure.

The same is true of associativity. If you say mulnA, you are referring to multiplication on nats. If you say mulrA, you are referring to multiplication on a ring. In either case, a one-step canonical structure hint will find it.

Of course, when we do group theory, we want multiplication in groups. You guessed it: there is a group scope, and there is a mulgA. But unless you are doing group theory, these aren't even loaded. You certainly don't have to worry about semigroups, monoids, and groups when doing a calculation on the integers.

I am not saying we have to be that hard core. It is nice to use has_mul to disambiguate notation. But we can come closer to the Mathematical Compoments approach by making sure there are short paths nat -> has_mul and ring -> has_mul and group -> has_mul. This is a trivial search through a few common instances. Similarly, a genericmul_assoc can replace mulnA, mulrA, and mulgA.

I am also not saying that the solution is to add shortcuts for every instance in the current hierarchy. Rather, we could design the hierarchy so that it works better for type class inference. Unless someone is working on monoid theory (an age-old, venerable branch of mathematics) there is no need to have the monoid structure playing an essential role every time a user types *.

Mathematical components is evidence that something along these lines is possible. I also made some suggestions here: https://leanprover.zulipchat.com/#narrow/stream/180721-mathlib-maintainers/topic/Redesigning.20Lean.20classes.20-.20call.20for.20problematic.20examples/near/176877491.)

My concern is that having long paths from complex structure down to notations causes problems:
- elaboration gets slower
- unification gets slower: if in an instance of reflexivity, a * one each side is represented differently (because they are build up by applying generic lemmas in different settings), the system potentially has to do a lot of unfolding to recognize that they are the same
- error messages become more opaque and problems become harder to debug
- automation: e.g. we want the simplifier to find relevant generic facts very quickly

That said, I don't have any hard data that says that these are problems, and others don't seem to be complaining about them much. So maybe I am worrying for no reason. It might be that a technical fixes and improvements -- caching, better class inference algorithms, etc. -- will sustain mathlib in the future. But the problem with performance problems is that they creep in slowly and only become unbearable when the library gets really large, at which point, it becomes harder to deal with them. So the move to Lean 4 may be an opportunity to get things right.

So my question to @Daniel Selsam and @Sebastian Ullrich is not a rhetorical one. Is this something we should think about when we start moving the library to Lean 4, or should we just port the library as is and stay the course? I am o.k. with continuing with the current style, but I would like to hear at least a bit of discussion from people working at the outer limits of our structure hierarchy and people involved in the implementation to make sure we are doing this deliberately, not blindly.

[Mario Carneiro]

I really wish we could add shortcuts through the hierarchy, but shortcuts mean more paths and everything gets worse

[Daniel Selsam]

@Jeremy Avigad @Kevin Buzzard I recommend against pre-emptively refactoring the hierarchy without evidence that it will still be problematic in Lean4. @Sebastian Ullrich is working on automatically porting typeclass queries from Mathlib to Lean4 in order to assess this. Also, as Kevin points out, in the unlikely case that there is still a problem, it might be addressable by some very simple heuristics.

[Jeremy Avigad]

Sounds good. I am happy to know that you guys are on it!