type class inference system

Stream: general

[Johan Commelin]

Two (classes of) related questions:
1) Is there some reference for the type class inference algorithm that Lean uses? Is it ad hoc, or does it follow some established algorithm? Is it documented in some paper?
2) How will Lean 4 impact the type class system? Is it planned to remain the same, or will it go through a major revision?

[Gabriel Ebner]

Is there some reference for the type class inference algorithm that Lean uses? Is it ad hoc, or does it follow some established algorithm? Is it documented in some paper?

I think the canonical answer is that it's a λProlog interpreter, which synthesizes instances by essentially backchaining. We typically cite [1].

[1] D. Miller and G. Nadathur. Programming with Higher-Order Logic. Cambridge, 2012.

(Not entirely sure if this is helpful.)

[Johan Commelin]

Yes, I think it answers 1).

[Gabriel Ebner]

How will Lean 4 impact the type class system? Is it planned to remain the same, or will it go through a major revision?

I don't expect any significant changes, but Sebastian can probably speak more authoritatively on this topic.

[Sebastian Ullrich]

There are no changes to the type class system planned right now

[Johan Commelin]

Maybe I have a newbie question 3): Are coercions and type class inferences somehow two avatars of some underlying common principle?

[Johan Commelin]

/me just realises that the Miller--Nadathur reference is a 300 page book...

[Johan Commelin]

Once Lean 4 is ready, someone should write "The Leanbook". Alas, I hear that Don Knuth's todo list is non-empty ;-)

[Johan Commelin]

I would love to understand the inner workings of Lean. But I'm not a very proficient source reader. In that regard I found the TeXbook very enlightening.