The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

And the key aspect is actually that the records are *dependent*: not only can you package types and (higher order) values but also properties and proofs. In a dependently typed setting there is arguably no need for a meta mechanism like modules (although modules may provide more meta things like notations, private definitions etc). 

Type classes and canonical structures are dependent records + some dedicated pre-typing procedures. They are currently much more used than modules as a structuring mechanism.

Best

P

Le lun. 14 mars 2022 à 09:29, Meven LENNON-BERTRAND <Meven.Bertrand AT univ-nantes.fr> a écrit :

To add to Adam’s answer, the key tool to packaging structures in the Mathematical Components project (or, actually, the Hierarchy Builder tool, which is now a standalone project) are record types. They are quite similar to modules, but with a somewhat different trade-off in the precise functionalities. In particular, they are first-class types. The best reference I know of to compare the different forms of "packaging" available in Coq is this short abstract for the Types conferences, it might be of interest to you, although it’s quite short…

Meven LENNON-BERTRAND
Doctorant, Équipe Gallinette – LS2N – Université de Nantes
www.meven.ac

Le 13/03/2022 à 13:43, Adam Chlipala a écrit :

On 3/12/22 11:10 PM, Constantine Plotnikov wrote:

  Module Type AbelianGroup.
    Include Group.
    Axiom comutative : forall a b : T, operation a b = operation b a.
  End AbelianGroup.

  [...]

    Theorem plus_group : AbelianGroup with T := T, operation := plus, identity = zero, inverse = unary_minus).
      (* proof that it exists with specified operators *)
    End plus_group.

As you've discovered here, modules are not first-class in Coq.  There is no way to define a module from within a Gallina term, just to reference module members.  I suppose technically the Coq vernacular language could allow use of the tactic mode to define a complete module (albeit with the complication that the goal is no longer a Gallina term), but I don't think that support exists either.

You may not be aware that the style of definition you are pursuing is already one of the standard uses of Coq, rather than a fully novel experiment.  The Mathematical Components project may be the most extensive work with algebraic hierarchies.  They use canonical structures (a relative of type classes) instead of modules.