The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

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.