[Agda-dev] Fwd: [coqdev] Tabled typeclass resolution

[Guillaume Allais]

This may be of interest to us too!


-------- Forwarded Message --------
Subject: [coqdev] Tabled typeclass resolution
Date: Tue, 14 Jan 2020 12:48:08 +0100
From: Gabriel Scherer <gabriel.scherer at gmail.com>
Reply-To: Gabriel Scherer <gabriel.scherer at gmail.com>
To: Coqdev <coqdev at inria.fr>

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.