设计仿函数能够使用不同的模块

Question

我有两个不同的模块签名到两个不同的文件。他们有相同的字段名称但行为不同。

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

和

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. 

凡MonoType另一个文件例如Mono.v

里面这是我的情况。

我有另一个文件叫B.v里面我需要在文件PI.v和MI.v这两个文件中使用定义和引理。

和我需要使用它们的一个定义为例。

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

我在R有一个问题，因为pi_int R和mi_int R具有不同sig（签名），其中使用pi_int的trsInt模块签名TPI和mint_int使用trsInt的模块签名TMI内部内。

这里是我定义的方式：

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. 

我的问题是，在那里我可以有模块的结构好，我可以在定义redPair具有相同签名的方法吗？感谢您的帮助。

Answer 1

在实践中，在0123,的定义中，您不能保证P.sig和M.sig具有相同的类型，这就是您收到此错误消息的原因。

解决这类问题的方法是通过“共享约束”强制执行类型相等。这是类似于你展示我如何强制P.sig和M.sig等于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. 

你也可以选择离开P.sig不受约束，但随后执行M.sig是相同的：

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. 

---

既然提到了你的问题的解决方案，我会建议在Coq中使用模块和函数。大多数情况下，你实际上只需要依赖记录。模块和函子是复杂的每一个人，你必须关心的抽象，共享约束等

现状似乎是，你应该避免使用它们，除非你实际上他们需要为他们提供了相关的记录：抽象和/或子类型。

事实上，我现在对你的定义有点不安。例如，在PI内定义MI是否有意义？没有更多上下文，这似乎是任意的也许它的确如此，我只是说在使用模块时应该小心，并且确保你已经掌握了你正在做的事情，否则它可能会适得其反。 :)

但是，如果你只是试验，请做实验。了解各种可能性的范围和利弊是很好的。