The Coq mailing list

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

Dear Russel,

an alternative to modules is Structure (aka Record). They give you first
class values. I use the modules only to split the namespace. (Note that each
file is a module on its own - try: Require Bool. Print Bool. !)
Then your example looks like:

(** new file Field.v *)
Structure Field : Type :=
   { K :> Set
   ; plus : K -> K -> K
   (* ... *)
   }.

(** coqc Field.v *)
(** new file VectorSpace.v *)
Require Import Field. (* You may choose Export instead of Import. *)

Structure VectorSpace (F:Field) : Type :=
   { V :> Set
   ; plus : V -> V -> V
   ; scale : K F -> V -> V
   (* ... *)
   }.

(** coqc VectorSpace.v *)
(** new file DualSpace.v *)
Require Import Field.
Require Import VectorSpace.

Definition DualSpace (F:Field) (X:VectorSpace F) : VectorSpace F :=
   Build_VectorSPace F { f:V X -> K F | linear f } (* ... *)
   .

PS: A nice scheme for structures is imho:

Record is_X (...) : Prop := { x : Prop ... }.
Structure > X : Type := { C :> Type ; functions ; proof : is_X ... }.

It separates the consistency proof from the types and functions of the
structure.

E.g.:

Set Implicit Arguments.

Record is_setoid (C:Type) (Ceq : relation C) : Prop :=
   { refl : reflexive C Ceq
   ; sym  : symmetric C Ceq
   ; trans : transitive C Ceq
   }.

Structure > setoid : Type :=
   { C :> Type
   ; Ceq : relation C
   ; proof : is_setoid Ceq
   }.

Note the indications for coercions, i.e. `>' and `:>'. This allows us to
write:

Let x : is_setoid Ceq := Build_is_setoid C_refl C_sym C_trans.
Let y : setoid := x.
Let z (c:y) : Prop := Ceq y c c.

After the commands:

Implicit Arguments Ceq [s]. (* Make the setoid implicit! *)
Infix "[=]" := Ceq (at level 70, no associativity).

We can even write:

Let z' (c:y) : Prop := c [=] c.

roconnor AT theorem.ca
 (Sat, Mar 12, 2005 at 12:58:20PM -0500):
> I am trying to understand Coq's Module system.  I want to do something
> analogous to having a Module Type for fields.  Having a Module Type for
> vector spaces with a field parameter, and having a Fuctor taking a vector
> space to the dual vector space.
> 
> Module Type Field.
> Parameter K:Set.
> Parameter plus: K -> K -> K.
> (*...*)
> End Field.
> 
> Module Type VectorSpace (F:Field).
> Parameter V:Set.
> Parameter plus: V -> V -> V.
> Parameter scale: F.K -> V -> V.
> (*...*)
> End VectorSpace.
> 
> Module DualSpace (F:Field) (V:VectorSpace F) : VectorSpace F.
> Definition V := {f:V.V->F.K | linear f}
> (*...*)
> End DualSpace.
> 
> Coq complains at my definition of DualSpace.  It is entirely possible I
> have no idea what I am doing.

Best regards,
-- 
Stefan Karrmann