The Coq mailing list

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

Dear Lawrence,

I am still a beginner with Coq, but may be my observations help a bit. First 
I would say there are 3 mechanisms:

- records containing proof terms like classes but not using automatic 
instance resolution
- classes and instances with automatic instance resolution
- the module and module type system

The first two have the advantage that the records and classes are Gallina 
terms, which can be passed and returned to/from functions, stored in records 
and so on. You can pass a module only to a module function, but not to a 
Gallina function, which computes something. The latter gives a lot of 
flexibility, which is not easily possible with Modules.

In complicated cases I sometimes prefer simple records over classes. The 
automatic instance resolution is very handy, but if things get complicated, I 
found that it can be more work to find out why the instance resolution 
doesn't do what you want than doing the instance resolution manually. 

The main advantages of modules I see is that they have a lot syntactic sugar 
and comfort features to combine and organize modules.

So I see modules mostly as an elegant way to organize and to abstract 
libraries. For building up complex nested structures, classes or records are 
more useful.

Best regards,

Michael

-----Original Message-----
From: Scott Lawrence 
[mailto:bytbox AT gmail.com]
 On Behalf Of Scott Lawrence
Sent: Wednesday, May 27, 2015 9:50 PM
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Type Classes and Module Types

Hi all,

Many of the same things can be done via `Module Type` and `Module` as with 
`Class` and `Instance`. Are there any good rules of thumb for when to use 
which? For example, either could be used to define VectorSpace < 
NormedVectorSpace < BanachSpace -- is there a reason to pick one over the 
other?

(Somewhat pettily, I find the syntax resulting from using the module system 
to be far cleaner. I also note that the documentation declares type classes 
to be very experimental.)

Thanks,

--
Scott Lawrence