The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

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