The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I recently ran into a shortcoming of typeclasses: that they do not 
provide multiple successes for use by backtracking proof search 
(roughly, this means that "typeclasses eauto" = "once typeclasses 
eauto").   I didn't bother to examine canonical structures - might they 
be different in this regard?


-- Jonathan


On 04/26/2016 05:08 AM, Guillaume Melquiond wrote:
> On 25/04/2016 23:41, Gregory Malecha wrote:
>
> > My personal advice is to use type classes but there are definitely
> > people on this list that will tell you that canonical structures are
> > much better. From a future-looking point of view, it seems like there is
> > some current work in making type classes work better, while, to the best
> > of my knowledge, canonical structures are not actively being developed
> > anymore. My hope is that some of the downsides of type classes will be
> > mitigated by this work which will lead to fewer reasons not to use type
> > classes.
> That is the core of the matter. On the one hand, the typeclass mechanism
> is a full-blown Prolog system, which makes it easy to (powerfully) use.
> But it also means that it needs a constant stream of new fixes so that
> it works efficiently. On the other hand, the canonical structure
> mechanism is a single forward rule, which means that it is harder to use
> since you have to understand how to achieve the desired result. But it
> also means that the mechanism doesn't need any active development since
> it is so simple.
>
> As far as I am concerned, I started with typeclasses, since they were
> easier to use. Then I switched to canonical structures once I was no
> longer able to debug where I got my typeclass instances wrong.
>
> Best regards,
>
> Guillaume