The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Robert Dockins 
<robdockins AT fastmail.fm>:

Hi Robert,

> In the declaration for Module DualSpace you have 'VectorSpace with
> Module F:=G'  and then 'Module F:=G' again in the body.  Why is that
> necessary?
>

The first occurrence of "Module F := G" is part of the signature with
manifest definition. The second occurrence is part of the module itself
(its implementation). So it is logical to repeat this clause.
It is similar to OCaml's module system.


> More generally, is there a good place to learn how to use Coq modules?
> The documentation is less than helpful, and I haven't got the cash for
> Coq'Art just now.


In the book site you will find an implementation in Coq  of an example from
Paulson's "ML for the working programmer" (totally ordered sets and
dictionnaries)



  http://www.labri.fr/Perso/~casteran/CoqArt/modules/


Pierre


>
> On Sat, 2005-03-12 at 19:52 +0100, 
> anoun AT labri.fr
>  wrote:
> > Hi Russel,
> > The problem comes from using type functors, we can replace that by
> declaring a
> > Module F inside the signature VectorSpace like the following:
> >
> > Module Type Field.
> > Parameter K:Set.
> > Parameter plus: K -> K -> K.
> > (*...*)
> > End Field.
> >
> > Module Type VectorSpace.
> > Declare Module F:Field.
> > Parameter V:Set.
> > Parameter plus: V -> V -> V.
> > Parameter scale: F.K -> V -> V.
> > (*...*)
> > End VectorSpace.
> >
> > Module DualSpace (G:Field) (V:VectorSpace with Module F:=G) : VectorSpace
> with
> > Module F:=G.
> >
> > Module F:=G.
> > Definition V := {f:V.V->F.K | linear f}
> > (*...*)
> > End DualSpace.
> >
> >
> > Regards,
> > Houda
> >
> >
> >
> > Quoting 
> > roconnor AT theorem.ca:
> >
> > > 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.
> > >
> > > --
> > > Russell O'Connor                                      <http://r6.ca/>
> > > ``All talk about `theft,''' the general counsel of the American
> Graphophone
> > > Company wrote, ``is the merest claptrap, for there exists no property in
> > > ideas musical, literary or artistic, except as defined by statute.''
> > > --------------------------------------------------------
> > > Bug reports: http://coq.inria.fr/bin/coq-bugs
> > > Archives: http://pauillac.inria.fr/pipermail/coq-club
> > >           http://pauillac.inria.fr/bin/wilma/coq-club
> > > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> > >
> >
> >
> >
> >
> > ----------------------------------------------------------------
> > This message was sent using IMP, the Internet Messaging Program.
> > --------------------------------------------------------
> > Bug reports: http://coq.inria.fr/bin/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >           http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.