There are 2 extensions of Coq that look similar: type classes and canonical structures.

Both ask one to define a record _(or structure, which is the same according to the reference)_ template, and then a bunch of record values. Then eventually implicit variables may be filled with these values — perhaps automatically, perhaps by hand.

So what is the difference? When should I use one or the other? Apparently the same concepts may be formalized either way — looking at `mathcomp`

and `stdpp`

I think I see some overlap, but the former uses canonical structures and the latter type classes.

Both ask one to define a record

not typeclasses. see the Existing Class command

Let us make this question more specific.

What I want to do is develop the theory of rings, ideals and factorization from scratch and attach it to concrete canonically represented entities like ℚ and ℚ[X]. My understanding is that I can choose either type classes or canonical structures to perform this attachment. What should I go with?

I am no stranger to type classes, thanks to experience with Haskell. I am presently reading the Mathematical Components book, and it seems to me so far that they are doing with canonical structures exactly the same things as I would do with type classes in Haskell. So, I find it hard to see how canonical structures are different from type classes and why both exist in the official distribution of Coq.

There is a book in the making with a chapter about that, but I'm afraid I can't share it (yet). The short answer is: yes, CS and TC are the same, but because of implementation details they forces your record to have the "search key" as a field (CS) or as a parameter (TC). In Coq TC are easier to start with, they allow for overlapping instances and multiple search keys, but you have to set Hint Modes and carefully pick your instances to have a reliable behavior. Moreover TC search is a bit more "blind sided" that the CS one when it comes to relate two structures in the same hierarchy, and that can lead to performance problem. CS are simpler, less flexible, but more reliable.

What I want to do is develop the theory of rings, ideals and factorization from scratch

This is the worst mistake you can do. Use what is there, if it does not fit your needs work the authors of what is there to change it.

Thanks Enrico! I cannot wait to see that book published, godspeed!

[Ad] https://github.com/math-comp/hierarchy-builder

@Enrico Tassi Interesting! What book ?

I don't know how much is public right now... I can tell I'm writing chapter 7, topic elaboration, with Freek Wiedijk. ETA should be this year.

At some point, soonish, we will need help proofreading...

Last updated: Jun 16 2024 at 01:42 UTC