The Coq mailing list

[Jacek Chrzaszcz <chrzaszc AT mimuw.edu.pl>]

Hello,


On Tue, Jul 01, 2003 at 03:13:45PM +0100, Randy Pollack wrote:
> Hello,
> 
> I'm playing with modules for the first time.  Here are some questions.
> 
> Is it possible to have a hypothetical module?  
> ...

The only way to do that is to construct a functor, with a parameter of type 
Id.

Module F[Var:Id].
  (* Here you can use Var *)
End F.
(* Here, you can't any more *)


> Since I don't see how to do that, I instantiated the signature with a
> ground module:
> 
...
> 
> However, I was surprised to see that I can also write
> 
>  Module Par: Id := Var
> 
> and still have Var.X <> Par.X.  Since modules have strengthening, this
> is against my intuition.  What is the explanation?
> 

It is exactly like in Caml...

If you write 

Module Par: Id ....

than no matter how you implement your module (either directly or with :=Var), 
you always get Par.X <> Var.X

However, if you write

Module Par := Var.

then (thanks to strengthenning) you get Par.X=Var.X.

If you want the signature Id to appear in your declaration, you can also
write

Module Par <: Id := Var.

This way you make sure that Par is of type Id and you do not put any
restrictions on the interface of Par.


I hope it answers your question.




Jacek