The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Andreas Kägi wrote:
> Thanks four your help, Yves.
> I was probably too much thinking in a Java analogy of interfaces and classes.
> I thought I only had to produce a value A of type Set and a module M1sub
> satisfying the signature of MT1. But apparently, I cannot use the
> definitions/module types defined in a module type within the corresp. module
> implementation?
>
>
>
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/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
>   
The module / interface mechanisms make that there are three "moments" of 
usage:

- when you are defining a module type,

- when you are defining a module (satisfying --or instantiating-- a 
module type),

- when you are using a module.

When you are defining a module (2nd moment of usage), you cannot assume 
that all
the fields of the module type are already provided, on the contrary you 
have to show
that you know how to construct them.

When you are defining a module type, you make promises, when you define 
a module
satisfying a module type, you claim that you will fulfill all the 
promises (so, you make
promises again).  The claim is checked when you type "End ...".

Normally, when you use a module, you can only use what was promised for 
in the
module type.  This discipline makes it possible to replace the module 
with another
one providing a different implementation for the same functionality.

I am not sure about your Java analogy, but if you can use what you 
should be defining
before it is completely defined, you enter a domain of recursive 
definitions where it
becomes difficult to know when things are really defined.  We are 
accustomed to this
in conventional programming language, where recursive values sometimes are
unusable (because a recursive function loops, for instance), but theorem 
provers are usually
more careful about having a definite value for everything that is 
encountered (and
for instance, theorem provers provide a restricted form of recursion, 
with guaranteed
termination).

Yves