The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-05-28 14:06 GMT+02:00 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.

​I mostly second that point of view.

The main advantages I see in Modules over Classes/Records are:

* Tactics​ (you cannot define a tactic inside of a record as far as I know)

* Notations and scopes (you need to reserve notations for records, and you have less control over them)

* Interactivity (you can define parts of the module as lambda terms, and part as proofs in the script language, inside modules, it is less convenient, although you can use the refine tactic for similar results)

There is also the inheritance with them (you can include the contents of an other module for instance), but I hardly see as it has the annoyance of building a true maze between modules (and module types). I mainly have the Ord (or Order, I don't remember) in mind for that: from time to time, someone asks help on the list to understand how to build a finite map. I don't remember having seen much help requests on other modules. Of course, library developpers have a lot less code to write, but users are often confused on what to provide to define the module.

I find these advantages often neglictable in front of the advantages carried by records/class (mainly the fact being first class citizen).

Thus in practice, I do not use modules (well beside the .v/.vo files which describe modules themselves).

 

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