Ancillary-file links:
Ancillary files (details):
References & Citations
Computer Science > Programming Languages
Title: Tabled Typeclass Resolution
(Submitted on 13 Jan 2020 (v1), last revised 21 Jan 2020 (this version, v2))
Abstract: Typeclasses provide an elegant and effective way of managing ad-hoc polymorphism in both programming languages and interactive proof assistants. However, the increasingly sophisticated uses of typeclasses within proof assistants, especially within Lean's burgeoning mathematics library, mathlib, have elevated once-theoretical limitations of existing typeclass resolution procedures into major impediments to ongoing progress. The two most devastating limitations of existing procedures are exponential running times in the presence of diamonds and divergence in the presence of cycles. We present a new procedure, tabled typeclass resolution, that solves both problems by tabling, which is a generalization of memoizing originally introduced to address similar limitations of early logic programming systems. We have implemented our procedure for the upcoming version (v4) of Lean, and have confirmed empirically that our implementation is exponentially faster than existing systems in the presence of diamonds. Although tabling is notoriously difficult to implement, our procedure is notably lightweight and could easily be implemented in other systems. We hope our new procedure facilitates even more sophisticated uses of typeclasses in both software development and interactive theorem proving.
Submission history
From: Daniel Selsam [view email][v1] Mon, 13 Jan 2020 14:40:59 GMT (326kb,D)
[v2] Tue, 21 Jan 2020 15:09:43 GMT (676kb,AD)
Link back to: arXiv, form interface, contact.