The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hi, Igor --

There are trade-offs to your choice. Here is my opinion, but you should note that I am not an avid user of canonical structures.

In my opinion, type classes are both easier to read and use. Part of this is due to the pattern where the relevant information is made manifest in the type. For example, if you want a type that is both a [Foo] and a [Bar], then you just have two arguments [Foo a] and [Bar a]. This makes a lot of sense to me and it doesn't require a lot of boiler plate to construct a [FooBar] structure that carries both of these.

There are two main downsides to type classes.

1/ They do not have as predictable of a resolution mechanism (it is essentially [eauto with typeclass_instances]), and it is invoked later. My understanding is that (morally) the entire term is constructed with holes and then type class resolution tries to solve each hole that exists and has a type that is declared as a class (either using 'Class xxx := ...' or 'Existing Class xxx.'). In addition typeclass resolution has a tendency to loop infinitely when things go wrong which can be very annoying.

2/ They can be less efficient. This is especially true when you do not enable primitive projections (not enabled by default in 8.5). The reason that primitive projections can be important is because they give you a limited for of bi-directional type checking. For example if you look at all of the implicit arguments that arise in an _expression_ such as:

Class MyClass (T U V : Type) : Type :=

{ op : T -> U -> V -> bool }.

op true false nat

is actually represented internally as:

@op bool bool nat MyInstance_bool_bool_nat true false nat

That is the parameters of the type class are written as explicit arguments to [op]. When these arguments are large or there are a lot of them, this can lead to a performance problem. My understanding is that this is part of the reason that math-comp uses canonical structures. Following the canonical structures approach, this is never a problem because you tend to pack everything together so canonical structures do not take arguments.

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.

On Sun, Apr 24, 2016 at 6:09 AM, Igor Zhirkov <igorjirkov AT gmail.com> wrote:

Hello,

So far I have seen two ways of implementing typeclasses (iirc): through mixins and canonical instances and the Classes as told in reference manual.

Why would you pick on over another? 

BR

Igor

--

gregory malecha

gmalecha.github.io