The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Yao Li,

> 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?

since all the competent people seem to work on the next release let me 
answer. Part of it might be historical (canonical structures existed before 
type classes). One advantage of using canonical structure is that the 
mathcomp library has in my opinion a better design and documentation than the 
type class based Coq standard library. I don't want to blame or insult 
anybody - it is just my impression that the Coq standard library was not 
really designed but more or less happened over time while math components 
look like someone really thought about it upfront. To be fair the standard 
library is definitely improving, also due to increased and more consistent 
use of type classes. For the mathcomp library a very well written open book 
exists for documentation (https://math-comp.github.io/mcb/)

To make it short: if you want to use math components, you will use canonical 
structures. If you base your work on something that is based on the type 
classes in the standard library, you will use type classes. If you start on a 
blank sheet without much need for a library (very unlikely) you have the pain 
of choice, but I would upfront look at which library looks more useful for 
whatever you are up to from a functionality point of view. If you really 
don't need much of a library at all, I would suggest type classes - I also 
find it a bit easier to debug and to work with, although this disadvantage is 
I think well compensated by the better documentation of math components.

Regarding modules: I use modules for large things which get unwieldy with 
type classes or canonical structures. I wouldn't write down the specification 
or implementation of a larger software entity as a type class. If you say 
have 100 requirements or implementation functions / theorems which you cannot 
easily bundle or factorize into independent groups you would end up with a 
type class constructor with 100 arguments and in some places you might end up 
giving these 100 arguments in the right order. Modules are more suitable for 
such things. Until you get into this situation you should be fine with type 
classes or canonical structures. A small anecdote on this: when my wife got a 
child we went to an information session in a hospital. One of the women asked 
how she knows that she has contractions and should come to the hospital. The 
doctor answered: "if you can still think about if you have contractions or 
not, you don't have contractions". It is similar here.

I only use OCaml export (no Haskell) and there exporting modules works well 
(the module systems of Coq and OCaml are very similar).

Hope it helps.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928