The Coq mailing list

[Scott Lawrence <srl AT umd.edu>]

Thanks both of you for your insight! This all mostly meshes with my 
impressions, but it's good to know that I'm on the right track.

(I just realized last night that `Class A` lives in `Type` rather than `Prop`; 
this will make things considerably easier. Oops.)

On Thu, 28 May 2015, Cedric Auger wrote:

> 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

--
Scott Lawrence