Tabled Typeclass Resolution
Daniel Selsam, Sebastian Ullrich, Leonardo de Moura
cs.PL
Jan 13, 2020 · v1
TL;DR
Implements tabled typeclass resolution for Lean 4 to handle diamonds and cycles efficiently.
Abstract
Typeclasses provide an elegant and effective way of managing ad-hoc polymorphism in both programming languages and interactive proof assistants. The increasingly sophisticated uses of typeclasses within proof assistants have turned theoretical limitations 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 for typeclass resolution, 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 implemented the procedure for the upcoming version (v4) of Lean and 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.
Problem
Typeclass resolution in proof assistants suffers from two major limitations: exponential running times in the presence of diamonds and divergence in the presence of cycles. These theoretical limitations have become practical impediments as typeclasses are used in increasingly sophisticated ways.
Approach
The authors present tabled typeclass resolution, a new procedure that solves both problems through tabling (a generalization of memoization to goals with unification variables). The approach adapts techniques from logic programming to the typeclass resolution setting, handling the complications introduced by unification variables.
Results
Tabled typeclass resolution eliminates exponential blowup from diamonds and divergence from cycles. The procedure has been implemented and addresses the two most devastating limitations of existing typeclass resolution procedures in proof assistants.
