The Coq mailing list

[James Lottes <jlottes AT gmail.com>]

Presumably primitive projections and avoiding the "super unbundled" approach goes a long way to keeping the term size more manageable. I do not understand the assertion in Ralf's post re super unbundling being necessary to support diamonds, as the original paper seemed to support diamonds just fine without it. (Is the issue the non-uniqueness of the inhabitant observing the structure predicate?)

Regarding the search time issues, I've recently had a lot of success exploiting coercions for this. Specifically, I changed, e.g.,

  Class LatticeOrder L : Prop :=
    { lattice_order_meet :> MeetSemiLatticeOrder L
    ; lattice_order_join :> JoinSemiLatticeOrder L
    }.

to

  Record LatticeOrder L : Prop :=
    { lattice_order_meet :> MeetSemiLatticeOrder L
    ; lattice_order_join :> JoinSemiLatticeOrder L
    }.
  Existing Class LatticeOrder.

(Or sometimes use "Class" but declare the Coercions explicitly, leaving out the ":>"). To make this actually work, I added a tactic that is invoked during resolution for any typeclass living in Prop that effectively tries (exact H) on every hypothesis H (which takes coercions into account, unlike the way normal typeclass resolution checks the context). There's a fair bit of hackery involved to make the tactic efficient in the face of backtracking, and it's not perfect, but I'm quite happy with the result. I effectively have extremely fast typeclass resolution for the subset of the inheritance graph that can be mapped to the coercion mechanism (no diamonds, uniform inheritance), which covers a huge amount actually, yet am still free to add the usual backward-reasoning typeclass hints. It's also important that, like normal typeclass hints, coercions can be added after definition time, when the inclusion is a nontrivial theorem.

For different reasons, I had already switched to a different way of handling diamonds. In the above example, I've defined

  Definition JoinSemiLatticeOrder (L:set A) := MeetSemiLatticeOrder L ᵒᵖ.
  Existing Class JoinSemiLatticeOrder.

and I have a similar strategy for rings, with separate "Additive" and "Multiplicative" versions of the various group-like structures:

  Definition AdditiveMonoid (R:set A) := CommutativeMonoid (AdditiveGroupOps R).

Here "AdditiveGroupOps" is the identity function, but serves to guide typeclass resolution to pick the right monoid ops. (There are many downsides to this approach, but I feel like it "scales" better in the long run.)

Another common diamond is the set of projections from a homomorphism predicate to the two structure predicates for the domain and codomain. Currently I have a rather boilerplate-heavy strategy for dealing with these, though I think there's room for improvement.

Cheers,
James Lottes

On Wed, Feb 5, 2020 at 11:08 AM Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:
>
> [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.
> >