The Coq mailing list

[Fran�ois Armand <armand AT iie.cnam.fr>]

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.

  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 ?