The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Samuel,

thanks for working this out! One question: from the link you sent before I 
guess that you also experimented with records instead of modules. Could you 
comment on your experience? 

I agree that including module types in modules is a strange concept, but 
since it supports the idea of putting the interface of a module into a module 
type, I wouldn't call it heretic ;-) What would be cleaner is if a module is 
declared to have some module type, that then it includes all definitions from 
the module type automatically (both with transparent and opaque ascription, 
since it is part of the interface). This is how I mentally interpret what I 
am doing, even though I do the import explicitly.

Regarding your questions in the "module type functor method section":

(* Question: We could also have declared "L: Lang", and then do
      Module Import LInst := L P.
      instead of "Import L". What's the difference? *)

I think it is the same (but I didn't check the module typing rules). I would 
do the partial module type functor application of LANG only if P would not be 
an argument of the module but be a module which is instantiated in the body 
of the module. That is if P would not be part of the interface of the module, 
but an abstractable implementation detail. Such things do happen in practice. 
But in this case I would clearly say L : LANG P.

(* Quirk/Question: Can we avoid having one module instantiation

Yes, you can write:

Module Combination(Import P: PARAMETERS_NAT_NAMES)(Import L: LANG P).

 (* Quirk/Question: Why do I have to repeat all these definitions? 
     There's nothing unknown or unspecified. *)

As I wrote before, it would be nice if the module type ascription would 
automatically include definitions. This would solve this.

Following my rules the definitions wouldn't belong in a module type, since 
they are not part of a non abstractable module interface. What happens is 
that by specialization you split a module type into a part which should still 
be a module type and a part which should be a module. If I have such cases, I 
split them up in two module types, so that by specialization one can stay a 
module type and the other can become a module.

I have to think about if there is a more elegant solution.

Maybe we should do a feature request to have the "include definitions in 
module type ascription". I guess not that many people are using definitions 
in module types, so likely it would break little code.

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