coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Leveraging the module system

From: Elie Soubiran <soubiran AT lix.polytechnique.fr>
To: "M. Scott Doerrie" <mdoerri AT cs.jhu.edu>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Leveraging the module system
Date: Sun, 1 Feb 2009 12:08:30 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=FZaHPcwM7AGtVz8ozd1tRUolIfHqhuX2zAAAu3lfC7vNM8iuR5wgRzcLpmmHJGlDAS iWMm7FAcEPr4FXkkkGug5f2+JvZU+OShWVd2VO3MjB2kx3jxF4WGc+gbELOTG698KXle x9LEr0H8ieBQUar4sE0rXI9d+Ej8imtuDIvI8=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

> My original example required that SIG be a signature of a functor over SIG2.

Ok then you should do:

Module Type SIG ( P : SIG2 ).

Parameter foo : P.t -> Prop.

End SIG.

Module Impl' ( P : SIG2' ).

Definition foo (P:t) : Prop := (* implementation *).

End Impl'.

Module Impl : SIG := Impl'.

Remark: The subtyping relation for module is contravariant for functor
parameter, i.e. in this example SIG2 must be a more "precise"
signature than SIG2'. If in your development SIG2 is equal to SIG2'
then it's useless to seal (:) the whole functor with the signature
SIG, and you should only seal your functor with an output signature as
presented in previous mails.

Elie.

Re: [Coq-Club] Leveraging the module system, Elie Soubiran