Zulip Chat Archive

Stream: general

Topic: type class inference system


Johan Commelin (Jun 05 2018 at 17:03):

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 (Jun 05 2018 at 17:08):

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 (Jun 05 2018 at 17:09):

Yes, I think it answers 1).

Gabriel Ebner (Jun 05 2018 at 17:09):

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 (Jun 05 2018 at 17:10):

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

Johan Commelin (Jun 05 2018 at 17:11):

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

Johan Commelin (Jun 05 2018 at 17:19):

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

Johan Commelin (Jun 05 2018 at 17:24):

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

Johan Commelin (Jun 05 2018 at 17:25):

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.


Last updated: Dec 20 2023 at 11:08 UTC