Ignat Insarov (Jun 27 2021 at 10:37): Ignat Insarov (Jun 27 2021 at 10:37):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.
Gaëtan Gilbert (Jun 27 2021 at 10:56):Both ask one to define a record
not typeclasses. see the Existing Class command
Ignat Insarov (Jun 27 2021 at 11:51):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?
Ignat Insarov (Jun 27 2021 at 11:56):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.
Enrico Tassi (Jun 27 2021 at 13:23):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.
Enrico Tassi (Jun 27 2021 at 13:24):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.
Ignat Insarov (Jun 27 2021 at 13:33):Thanks Enrico! I cannot wait to see that book published, godspeed!
Enrico Tassi (Jun 27 2021 at 14:24):[Ad] https://github.com/math-comp/hierarchy-builder
Bas Spitters (Jun 28 2021 at 05:54):@Enrico Tassi Interesting! What book ?
Enrico Tassi (Jun 28 2021 at 06:09):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.
Enrico Tassi (Jun 28 2021 at 06:12):At some point, soonish, we will need help proofreading...
Last updated: Sep 23 2023 at 13:01 UTC