The Coq mailing list

[Kevin Hamlen <hamlen AT utdallas.edu>]

Dear Michael,

Thank you for your suggestion; it's enormously helpful.  I agree that 
it's the best solution I've seen.

As you pointed out, the only downside I've found so far is that one must 
still be very careful about any Module Type that defines/imports a 
Module (instead of a Module Type).  If any names from that Module leak 
into theorems or ltacs exported by the Module Type, then those theorems 
and ltacs sometimes aren't recognized by Coq as unifying with 
differently-named terms created by equivalent but distinct instances of 
the same Module.  But with sufficient care and avoidance of Modules in 
favor of Module Types, I think your approach works.

To answer your questions:  Our use of modules is driven by the need to 
parameterize our definitions by things that the Coq standard libraries 
define as modules (e.g., in Coq.Structures.Equalities). So although the 
module functor that receives one of these library-provided modules need 
not have a module-type that allows multiple implementations, the module 
it receives has a module-type and may indeed have various different 
implementations.  This seems to create a domino effect---all module 
functors in the inheritance hierarchy must apparently be implemented as 
module-types instead of modules, and all instantiations of those 
module-types are just dummy modules that include everything from the 
module-type.

Since we're targeting our project to eventually be open-source and 
hopefully valuable for general use, we were searching for an approach 
that is "accepted" by others.  This seems like a good one.

Best regards,
Kevin





On 8/19/2018 4:15 AM, Soegtrop, Michael wrote:
> Dear Samuel,
>
> I think I have shown how to fix this kind of issue in my post. I don't see 
> how your case is different. I would suggest to try the following:
>
> - put the inductive type definitions from module functor Imp into a module 
> type functor IMP
> - define module Imp as "Module Imp (P : ImpParameters) := Empty <+ IMP P."
> - give everything which needs Imp a parameter of type IMP and instantiate it 
> with Imp
> - possibly define combined module types and modules to avoid long parameter 
> lists
>
> The trick is that now the inductive definition is in the module type rather 
> than in the module instance and the type is the same for all instances, so 
> the inductive types are the same. At the end of the code I posted, you can 
> actually prove the following:
>
> Theorem Eq1: FD.bar = FDX.bar.
> Proof.
>    reflexivity.
> Qed.
>
> Theorem Eq2: FD.Bar = FDX.Bar.
> Proof.
>    reflexivity.
> Qed.
>
> although Coq still thinks FD.bar and FDX.bar are separate definitions as 
> Locate bar or Locate Bar shows.
>
> This might seem like a bizarre hack, but I think it is quite logical to do it 
> this way. My view is that whatever is needed by other modules must be defined 
> in a module type. Modules are there to define concrete implementations of 
> abstract definitions in a module type. Other modules should only use module 
> types and not concrete modules. When you cannot abstract away from what is in 
> a module, it is part of the interface and doesn't belong in a module but in a 
> module type.
>
> If you have an inductive definition and where you use this type you can 
> replace it with an abstract type (say a generic map data structure), the 
> inductive belongs in a module and the module type just provides an abstract 
> type. If you need the details of the inductive in modules using it, the 
> inductive belongs into a module type.
>
> Of cause if a module A just uses another module B to implement its 
> functionality in such a way that nothing of B is visible at the interface 
> (signature) of A, A can just use a module B. This typically applies to 
> modules just defining a bunch of lemmas, tactics or notations but also to 
> modules defining helper data structures like maps or sets, which are 
> abstracted away at the external interface of module A. But anything about 
> other modules which is somehow visible in the signature of A, must be defined 
> in a module type, and not in a module.
>
> In my experience the module system works quite well, if it is used in this 
> way.
>   
> I hope those who came up with the module system agree with this view.
>
> Best regards,
>
> Michael
>
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928