The Coq mailing list

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

On Fri, Jun 04, 2004 at 03:07:42PM +0000, François Armand wrote:
> Hello,
> 
> I wonder how to use Functor signature in Coq ?
> 
> This is my problem :
> I want to define a module in which some type are parameterized by type 
> defined in another module. I need to write signature for each module 
> because these sgnatures are used in an other signature.
>  From now, I've solved the problem like this :
> 
> <-- signature and functor definition -->
> Module Type MODULE_PARAMS.
> 
>    Parameter param1 param2 : Set.
> 
> End MODULE_PARAMS.
> 
> 
> Module Type SIG_MODULE.
> 
>    Declare Module P : MODULE_PARAMS.
> 
>    Record E : Set := {
>      e1 : P.param1 ;
>      e2 : P.param2
>    }.
> 
> End SIG_MODULE.
> 
> (* a functor to automatize creation of a module whose signature is 
> SIG_MODULE *)
> 
> Module MakeSigMod (X:MODULE_PARAMS) <: SIG_MODULE with Module P := X.
> 
>    Module P := X.
> 
>    Record E : Set := {
>      e1 : P.param1 ;
>      e2 : P.param2
>    }.
> 
> End MakeSigMod.
> <--- end signature and functor definition --->
> 
> And an implementation of SIG_MODULE is done like that, for example :
> 
> <--- implementation --->
> Require Import List.
> 
> Module Impl_params <: MODULE_PARAMS.
>    Definition param1 := nat.
>    Definition param2 := list nat.
> 
> End Impl_params.
> 
> Module Impl_sigmod := MakeSigMod Impl_params.
> <--- end implementation --->
> 
> This works quite fine, but I think that SIG_MODULE should be a functor's 
> signature, to be cleaner.
> So, I attempted to write this, and it does not work :
> 
> <--- sigfunct --->
> Module Type SIG_FONCTEUR (X:MODULE_PARAMS).
> 
>    Record E : Set := {
>      e1 : X.param1 ;
>      e2 : X.param2
>    }.
> 
> End SIG_FONCTEUR.
> 
> (* Implementation... *)
> 
> Module MakeSigFonct (X:MODULE_PARAMS) <: SIG_FONCTEUR.

The thing you put after <: is (expected) signature of the _result_ and not
the whole functor.

> 
>    Record E : Set := {
>      e1 : X.param1 ;
>      e2 : X.param2
>    }.
> 
> (* End in the following line, I got a Coq error : "User error: 
> Incompatible module types" *)
> 
> End MakeSigFonct.
> <--- end sigfunct --->
> 
> What is the rigth way to define functor signature ?
> 

The definition is rigth, but the way you use it is not...

There is no direct way to do what you want, but there are two work-arounds:

1. define signature for the _result_ and write it after <: (may-be using
   with Definition to let it use parts of the functor parameters)

2. define the functor MakeSigFonct' (...) without <: ...
   and then write Module MakeSigFonct <: SIG_FUNCTOR := MakeSigFonct'.

And the functor type verification will happen then.

Jacek

> --------------------------------------------------------
> 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

--