The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Yao,

  If you understand well the way canonical structures operate then you can do many things similarly to type classes (e.g. overlapping and priorities, and more generally proof-search), but you have to do a non-trivial amount of massaging of definitions (see Ziliani's et al ICFP paper and Mahboubi and Tassi's paper on "Canonical Structures for the working Coq user" for some expositions of what is involved). Mainly the ability of type classes to be driven by Hint Extern give them kind of unbounded (and sometimes hard to control) expressivity.

  There is a kind of informal continuum between type classes and canonical structures: type classes allow indexing by parameters of the record type while canonical structures allow indexing by their fields. In particular canonical structures avoid a combinatorial explosion in term size, type-checking and unification/reduction time when your class has many indexes that is due to the naïve representation of record projections as defined constants taking all parameters of the record as argument. The primitive projections feature hopefully alleviates most of this problem (you still get larger proof contexts/typeclass binders in the "unpacked"/"unbundled" style), but I don't think a proper study of the performance differences on practical, at least medium sizes examples has been pursued yet. The Mathematical Components team has refined the canonical structure usage to an art, after hitting problems that only appear in really large developments. 

  The fact that canonical structures are mixed with unification can also help in some cases where "cascading"/nested resolutions are necessary and relying on just the dependency order followed by type class resolution is not enough.

Hope this helps,

-- Matthieu

On Fri, Apr 13, 2018 at 5:07 PM Yao Li <liyao AT seas.upenn.edu> wrote:

That is a very good argument. Thanks!

Still I wonder what’s the reason that some libraries like mathcomp choose to use canonical structures? What are the advantages of them comparing with type classes?

Best,
Yao

> On 12 Apr 2018, at 3:05 PM, John Wiegley <johnw AT newartisans.com> wrote:
>
>>>>>> "YL" == Yao Li <liyao AT seas.upenn.edu> writes:
>
> YL> 2. How do people usually choose among canonical structures, type classes,
> YL> and module systems? Do you have some specific use cases that only one of
> YL> them is most suitable? Or do you think people should only use one of them
> YL> (and which one would it be)?
>
> I usually choose type classes because: The errors I get from misusing
> canonical structures continue to mystify me, and module functors do not
> extract to Haskell. Type classes are at least familiar, allow for setting
> priorities, and come with Show Typeclasses Debug.
>
> --
> John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
> http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2