Type class search

Stream: lean4

[Jason Rute]

I have some naive questions about type class search, especially since it is the slowest part of compiling Lean. (I put my five questions in italics.) My understanding is that type class search is roughly a search through a graph. I also understand that lean 3 just did DFS and the new lean 4 tables that search to avoid loops and speed up searching through diamonds. Still it is slow. Since the search happens every time say mathlib is compiled, does it make sense to cache successful paths that the search takes? Then type class search can use those cached paths as a hint. If the code changes, then those hints might fail, but still it can fall back on regular search. Or possibly better, could one use a light-weight machine learning algorithm (obviously not GPT-4 :smiley:) to learn a heuristic for the search? This could then be used to memorize previous searches and also to guide new searches to be faster. However, this sort of thing might lead to a bit of non-determinism (or more specifically the search order would depend on the heuristic). Is this a problem? I don’t know if this is a problem in practice if we assume all diamonds are defeq. If it is a problem, and we need the search to be systematic, is knowing one path still better than not? Does it help in pruning branches for the systematic search? Last, since we require diamonds to be defeq (I think), is there any kind of linting for this in Lean 4?

[Henrik Böving]

1. Slowest part of compiling Lean...that highly depends on what type of Lean you are doing, if you are talking about mathlib4 you are right, if you are talking about writing normal application software in Lean the typeclass time will probably be overtaken by the code generator
2. Practically speaking we are already effectively caching the search paths, if you do a lake exe cache get you download all the .oleans for your mathlib4 build, those .oleans already contain all the type class stuff that was inferred. Obviously if you change a file that a cached .olean was built from (or a dependency of such a file) the .olean will have to be rebuild which right now basically means going completely from scratch. I guess we could store information about how the type class search went in a seperate location and attempt to use that in some way or form. I don't know how stable such an approach would be, there would certainly have to be some clever cache invalidation involved.
3. There are definitely cases where the type class resolution does have to make a choice between several instances to continue on and I guess we might see a speedup if we were very smart about picking those instances? But I don't have numbers or an intuition on that, it should however be possible to collect information on how much time we waste due to taking wrong branches in the search.
4. As I understand it type class resolution will eventually backtrack to previous decision points once it fails so if the alternative procedure chooses wrong the algorithm should still be able to recover from that. There might be other issues with a non deterministic search though but I don't know that. If this ends up being an issue: There are already attributes such as priority and default_instance for type class instances to influence the way that your instances are treated. Maybe we could use a machine learning approach that analyzes the way that a large amount of instance searches currently work and suggest more optimal priorities for your instances? Seems like an interesting optimization problem in any case^^
5. I don't know
6. I don't know

[Reid Barton]

My impression is that instance search is slow mostly not for any search-related reason, but because of some defeq problems that Lean takes a long time to solve.

[Henrik Böving]

Yes that was my impression as well, all the time that people complain about type class slowness it is because isDefEq is taking crazy amounts of time. But as I said I don't have numbers on how much time the type class synthesis wastes due to failing branches so I didn't want to make a guess.

[Henrik Böving]

In the end if we maybe end up having small speed ups for a ton of instances it might accumulate to some significant time!

[Sebastian Ullrich]

There should also be a good amount of time (on both the defeq and TC level) we can save with improved accurate/per-file caching before we go into nondeterministic caching

[Tomas Skrivan]

How much time is spent on classes in Prop and on classes in Type? Am I correct that caching for Prop` classes won't have the nondeterminism problems?

[Yury G. Kudryashov]

What part of time spent on TC search in mathlib4 is spent on

• all isDefEq calls?
• failing isDefEq calls?