The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Hi,

why has Coq a special module system with signatures, functors and
implementations? This doubles types, functions and values. An inductive
type (aka structure or record) can do the same. E.g.:

Structure Foo : Set := Build_Foo {
   x : nat ;
   x_val : x = 42 ;
   y : nat -> nat
   }.

Note that the component x_val implements a translucent definition.

In cayenne, cf. <http://www.cs.chalmers.se/~augustss/cayenne/>, the
record is reused for the module system.

Only the hiding of inductive types etc. is not possible without
signatures afaik. (Opaque seems to become transparent at discharges.)

Are there plans to join modules and structures in future releases of
Coq?

Regards,
-- 
Stefan Karrmann