The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> Having first-class modules might radically improve how we can organize 
> mathematical theories (although as always with this type
> of statement, one cannot be sure until it is tried out). Could anybody 
> on the development team comment on this issue, whether there
> are plans to resolve it, etc. ?

  I can only confirm that Coq modules are basically here for modular
development of theories. They are not designed for abstracting over
algebraic structures.

  Coq modules are not purely logical structures. Especially, they
carry non logical informations such as notations, proof search hints
or rewrite rules. Having first-class modules would require to give a
status to these non-logical informations inside the logical theory of
Coq, what I don't think we want.

  So, as emphasized by Stefan Karmann, the standard way to define
algebraic structure in Coq is through records, using coercions to
implement subtyping. To my knowledge, there is no ongoing work on
implementing direct (non coercitive) subtyping for Coq records.

  Hugo Herbelin