The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

[Moving this discussion to Coq-club]

While the tabbed implementation appears to avoid exponential blowups in 
*time* for (failed) searches, the paper does not address the problem of 
the exponential *size* of terms generated by type class search. Ralf 
Jung has a nice blog post about this issue:

  https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html

Does anyone know if Lean solves this issue? For example, by having some 
better sharing mechanism?

On 14/01/2020 12.48, Gabriel Scherer wrote:
> Dear coqdev,
>
> The Lean implementers have a new arXiv submission on a "tabled" 
> typeclass-resolution engine that avoids exponential blowups in cases of 
> inheritance/implication diamonds. I thought this may be of interest to 
> coqdev, as the approach could presumably also be applied to Coq's 
> typeclasses. (See below for abstract.)
>
> The paper contains actual benchmarks that do exhibit bad behaviors of 
> previous versions of Lean and Coq (Figure 4, page 15). One minor detail 
> that I found interesting is that in the first "bad benchmark", the 
> running times for Coq and Lean3 are extremely close together, which 
> suggests that the Lean runtime is not noticeably faster by a not-1 
> constant factor (as one could maybe expect from the advertisement of a 
> performance-focused C++ implementation).  (In the second benchmark, 
> Lean3 is noticeably faster than Coq.)
>
> Title: Tabled Typeclass Resolution
> Authors: Daniel Selsam, Sebastian Ullrich, Leonardo de Moura
> Categories: cs.PL cs.LO
>    arXiv: https://arxiv.org/abs/2001.04301
>    PDF: https://arxiv.org/pdf/2001.04301
>
>        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.