The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Sat, 16 Jan 2010 13:36:47 +0100, Stéphane Lescuyer  
<stephane.lescuyer AT inria.fr> a écrit:

> On Sat, Jan 16, 2010 at 1:23 PM, Adam Chlipala 
> <adamc AT hcoop.net>
>  wrote:
> > Chris Dams wrote:
> > > It seems writing records like list_type is about the same as writing
> > > Modules. Moreover, they are first class citizens in the Coq language,
> > > being Inductives with some extra destructor names for convenience. So,
> > > why was the basic Coq language polluted with the seemingly useless
> > > concept of modules?
> >
> > There are certainly ways to make Coq's module system more useful, but I
> > wouldn't call it useless.  You get the automatic support for "subtyping"
> > that comes from module signature ascription.  It's also useful to work  
> > with
> > second-class constructs in many cases; they are intrinsically easier to
> > understand, because the reader knows you can do fewer things with them.
> >  Finally, there are commands like [Import] that only work on modules,  
> > though
> > a similar command could certainly be implemented for records.
>
> And it should also be mentioned that each module has its own
> namespace, while records don't. And modules (and interfaces) can
> contain notations, hints, etc.

I also discussed of it with some people, and modules should be more  
efficient
as they define top-level objects.

Furthermore files are seen as modules and not records and as Stephane said,
we can define tactics in module types and call them with dot notation.

For example, if you want to extract some code, it is rather wise to use  
modules instead
of records, for performances; for proofs, it is less important.

But other things in Coq seem not very useful (and in fact they can be):
Classes (as they just are Records, but have automation for certain things)
Records (as they just are Inductives, and cannot be used inside mutual  
inductives for stupid reasons)
a lot of tactics are redundant,
use of Lemmas, Theorem, Corollary in one hand and Variable, Hypothesis,  
Parameter in the other hand.

I agree that these features lack some kind of unification.

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay