forward inference in typeclass

Stream: lean4

[Kenny Lau]

Currently, typeclass inferences take the form F x -> G x, and this practically means that whenever we want an instance of G x, Lean automatically searches for F x.

As a result, inference rules need to be "decreasing" (i.e. G should be more complex than F), otherwise the performance will have an impact.

Could we potentially make the typeclass system stronger by adding forward inferences to typeclass searching as well? i.e. in this proposal, we would be able to tag inferences F x -> G x with @[forward], and this would mean the whenever the current context contains F x, then Lean would automatically infer G x. Then, we can have increasing complexity as well, and for example we could have the rule [Module R M] -> [AddCommMonoid M]?

[Jovan Gerbscheid]

Note that to be able to meaningfully write down Module R M, there must already be an instance of AddCommMonoid M available.

[Kenny Lau]

Yes, so my proposal includes restructuring Module R M to include AddCommMonoid M, which we were not able to do because of this exact reason.

[Jovan Gerbscheid]

To be more precise, you are proposing:

• a @[forward_instance] attribute that applies to declarations of the form [F x] -> G x.
• For each global instance of F x, we also add the corresponding global instance G x
• For each local instance of F x, we also add the corresponding local instance G x
• declarations tagged with @[forward_instance] are not tagged with @[instance], because this search is now redundant.

[Jovan Gerbscheid]

I think this would be a good idea.

I would also be very curious to see the performance impact of replacing the @[instance] tag with @[forward_instance] in all instance of the right form. The consequence would be that adding an instance becomes slower, but looking up an instance becomes faster. And of course looking up instances is done much more often than adding instances.

[Jovan Gerbscheid]

Some more points

• For an instance of type [F x] -> G x to be in the correct form, we need F x to be a constant applied to only variables. And these variables need to be exactly the arguments that the instance takes. In this way, the forward instances are always applicable without a need for a potentially expensive unification or type class search.
  Does that sound reasonable?

• The process of computing the forwards instances from a given instance can give the same result in different forms, e.g. CommGroup -> Group -> Monoid vs CommGroup -> CommMonoid -> Monoid. So we will need to use unification here to avoid an exponential blowup. (Note that this blowup also arises in backwards type class search, which is dealt with properly)
  Maybe this algorithm could also give a warning if it thinks that it found a diamond :grinning:

[Kenny Lau]

@Jovan Gerbscheid why would you want to refactor the current backward instances CommGroup -> etc. to using forward?

[Kenny Lau]

I don't want to blow up the forward instances, I think we should use them sparingly

[Jovan Gerbscheid]

I do want to blow up the forwards instances, for improving performance :). The reason why type class search is slow is that the backwards instances have to search through the whole algebra library every time when you ask for an instance of e.g. Add, Sub or Monoid. If we can stop this "wild goose chase" from happening, then that would be a big performance win.

So what would happen is that if you declare that you favourite type is a NormedField, then it would automatically add all the weaker type class instances to the instances discrimination tree, meaning that they can be found much much quicker.

[Kenny Lau]

I suppose that's how mathematicians work too

[Jovan Gerbscheid]

After thinking a bit more, I think that the forward instance you suggest, [Module R M] -> AddCommMonoid M may be problematic. It works fine if Module R M is directly available in the local context. But if things get more complicated I'm afraid we could get into trouble.

Imagine that there is some funny global instance [Prime p] -> Module (R p) M that is different for all p. Then if we want to search for AddCommMonoid M, there is no way of knowing which p prime to pick.

[Jovan Gerbscheid]

(This is not an obstacle for the performance improvement I described above. Though I think that would better be named "shortcut instances" than "forward instances")

[Kenny Lau]

well, [Prime p] -> Module (R p) M would be a backward instance...

[Kenny Lau]

I'm not very well-versed in instances, so I'll trust what whatever you think is better is probably better

[Jovan Gerbscheid]

Kenny Lau said:

well, [Prime p] -> Module (R p) M would be a backward instance...

Exactly, what I'm worried about is that we cannot compose this backwards instance with your forwards instance. Because to find your instance, you need to reason forwards from the Module instance. And to find my instance, you need to reason backwards from the Module instance. So there is to way to get to the point of even considering the Module instance.

[Kenny Lau]

Could someone provide more examples of "non-decreasing inferences" so that we can be more informed?

[Kenny Lau]

I'll be the first one,

theorem PrimeSpectrum.nontrivial {R : Type u} [CommSemiring R] (p : PrimeSpectrum R) : Nontrivial R

is not an instance currently.

[Jovan Gerbscheid]

This is not an instance because PrimeSpectrum isn't a class (I think). So there is no way to infer p

[Patrick Massot]

This is an interesting discussion, but please keep in mind it is extremely unlikely to lead to any modification to Lean in the near future. The core team has already a lot of work, and what you are discussing is a huge modification of a critical core component of Lean.

[Jovan Gerbscheid]

That makes sense. My hope is though that if this kind of change gives a 50% speedup of type class search in mathlib, they will have to care..

[Kevin Buzzard]

Unfortunately the last time we tried to minimise the JacobiZariski problem we were saying "this is clearly a universe issue" and Ullrich said "well what about this issue, here is a speed-up, maybe that's your problem" (and he was right, it was one of our problems). But since then I have decided that there are several problems with this file and universes is definitely still one of them. The problem is we didn't yet write the correct mathlib-free MWE. It's been on my job list forever but right now there is so much low-hanging fruit in FLT that it might take me forever to get there. But tl;dr I think we need a reliable mathlib-free repro of "changing universe names makes a substantial difference".

[Jovan Gerbscheid]

Yes, the universes are another problem. But here I'm talking about typeclass search in general being slower than necessary.

And I think we can have a much stronger point towards core if we come with a: here is a fix that makes everything faster.

[Kevin Buzzard]

(sorry, I think I'm conflating two different threads here)

[Kyle Miller]

Backward chaining is fairly well understood and has a long history in logic programming. We know how to design our instances in ways that guarantee termination.

Forward chaining is has been long studied as well, but I'm not sure what the literature is on doing this in the context of typeclass inference. It reminds me of some of the things that show up in SMT solvers, in congruence closure I think.

I'm not speaking on behalf of the core developers here, but my feeling is that this has entered open-research-problem territory. Maybe with with some papers that prove the concept and develop the theory it might lead to a new typeclass inference system in Lean, but without that I would hesitate making fundamental changes to this system even if there is a proof of concept that shows better performance. Fundamental questions: "how can forward and backward instances compose in a performant way", "how can we design instances that don't cause inference to diverge", "how do we design math libraries when we have this tool", etc.

Regarding the proposal to add shortcut instances, haven't people found that removing shortcut instances has had positive effects on performance? The issue is that these shortcut instances provide more paths for typeclass inference to consider and then fail on.

One thing I know that does need to be addressed, and which isn't as big of an open research problem, is how to make sure typeclass inference respects the resolution order (i.e. how to make it prefer earlier parent projections, lean4#2325), which is important for isDefEq efficiency with the way instances are encoded. I think we could learn something from SageMath here, using some priority system where priorities are put on the classes themselves, rather than just on instances, and then doing a lot of work to try to get mathlib to compile with structure.strictResolutionOrder enabled (if that's possible at all!)

[Jovan Gerbscheid]

Yes, adding more shortcut instances without removing anything from the type class search will in general slow things down. But if we (automatically) add enough shortcut instances that the general instances can be completely ignored, then that would be a win. Here I define a general instance as an instance saying that one class (applied to only free variables) implies another class (applied to the same free variables), e.g. CommGroup α → Group α. So basically when syntesizing Add α, I want to never even get to the goals Ring α and Field α; I want that all the instances for that have shortcut variants that have the conclusion Add ..

[Jovan Gerbscheid]

Note that I have an RFC for type class abbrevs, which addresses the Module inconvenience in a different way: lean#8279

[Jovan Gerbscheid]

The idea of having automatic shorcut instances would also obviate the need for PRs such as #25358 by @Yaël Dillies. I'll try to implement and !bench this when I find the time.