Tabled Typeclass Resolution
share
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 has exposed two critical problems with existing typeclass resolution procedures: the diamond problem, which causes exponential running times in both theory and practice, and the cycle problem, which causes loops in the presence of cycles and so thwarts many desired uses of typeclasses. We present a new typeclass resolution procedure, called tabled typeclass resolution, that solves these problems. We have implemented our procedure for the upcoming version (v4) of the Lean Theorem Prover, and we confirm empirically that our implementation is exponentially faster than existing systems in the presence of diamonds. Our procedure is sufficiently lightweight that it 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.
READ FULL TEXT