Design functor to be able to use different modules

Question

I have two different module signatures into two different files. They have the same field name but different behaviour.

And functor inside define another functor.

PI.v

Module Type TPI.
  Parameter sig : Signature.
  Parameter trsInt: forall f, pi f.
End TPI.

Module P (Export T: TPI).
   Lemma A...
    Module Export Mono <: MonoType.
End P.

and

MI.v

Module Type TMI.
   Parameter sig : Signature.
   Parameter trsInt : forall f, mi f.
End TMI.

Module M (Export TM: TMI).
   Lemma B ...
   Module Export Mono <: MonoType.
End M.

Where MonoType inside another file for example Mono.v

Here is my situation.

I have another file called B.v inside that file I need to use definitions and lemmas in both files PI.v and MI.v.

And one definition I need to use both of them for example.

 Definition redPair R is :=
   match is with
 | Type_PI => pi_int R is
 | Type_MI => mi_int R is
 end.

I have a problem at R because pi_int R and mi_int R has different sig (Signature), where pi_int used trsInt inside the module signature TPI and mint_int used trsInt inside the module signature TMI.

Here is the way I defined it:

Module PI (Import P : TPI).
Definition pi_int R is := P.trsInt ...

(* inside PI I define another functor for MI *)
  Module MI (Import M : TMI).
   Definition mi_int R is := M.trsInt ...

   Definition redPair R is :=  
     match is with
    | Type_PI => pi_int R is
    | Type_MI => mi_int R is  (* error here saying that it used the sig of 
                    P.sig but in this case mi_int used the sig of M.sig *)
    end.

End MI.
End PI.

My question is that is there a way that I can have a good structure of module that I can have the same signature at the definition redPair? Thank you for your help.

Answer 1

In practice, in the definition of redPair, you have no guarantee that P.sig and M.sig have the same type, which is why you get this error message.

What one can do to solve this kind of problem is to enforce the type equality via a "sharing constraint". Here is a code similar to yours demonstrating how I force P.sig and M.sig to be equal to nat:

Module Type TPI.
  Parameter sig : Type.
  Parameter x : sig.
End TPI.

Module Type TMI.
  Parameter sig : Type.
  Parameter x : sig.
End TMI.

Module PI (Import P : TPI with Definition sig := nat).
  Definition pi_int := x.

  Module MI (Import M : TMI with Definition sig := nat).
    Definition mi_int := x.

    Definition f (x : bool) :=
      if x
      then pi_int
      else mi_int.

  End MI.

End PI.

You could also choose to leave P.sig unconstrained, but then enforce M.sig to be the same:

Module PI (Import P : TPI).
  Definition pi_int := x.

  Module MI (Import M : TMI with Definition sig := P.sig).
    Definition mi_int := x.

    Definition f (x : bool) :=
      if x
      then pi_int
      else mi_int.

  End MI.

End PI.

---

Now that a solution to your problem is mentioned, I would advise to be wary of using modules and functors in Coq. Most often than not, you actually only need dependent records. Modules and functors are complicated for everyone, you have to care about abstraction, sharing constraints, etc.

The status quo seems to be that you should avoid using them unless you actually need them for what they offer over dependent records: abstraction and/or subtyping.

As a matter of fact, I am at a bit of unease with your definitions right now. For instance, does it make sense for MI to be defined inside of PI? That seems arbitrary without more context. Maybe it does, I'm just stating that you should be careful when using modules, and make sure you have a good grasp of what you're doing, or it might backfire on you! :)

But if you're just experimenting, please do experiment with them. It's good to know the range of possibilities and the pros and cons of each.