The Coq mailing list

[harke AT cs.pdx.edu]

I'm glad Adam mentioned ascription, because I have a question about
it.  IIUC, a key benefit of a module system is ascription, which
restricts implementation details.

I want to (morally, metatheoretically) justify the use of the following
axiom outside of the module body that defines [MyType].

  Axiom setoid_eq_eq: forall (a b:MyType), a == b -> a = b.

The equivalence relation [==] is also defined in the same module as
[MyType], and all consumers of elements of MyType are either
 1. setoid morphisms, or
 2. hidden by ascription

Can [setoid_eq_eq] be justified on the grounds that points 1 and 2
so severely restrict the contexts that can examine a and b that [==]
is the same as [=]?

On Sat, Jan 16, 2010 at 07:23:12AM -0500, Adam Chlipala 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.

-- 
Tom Harke