The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

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'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06