2

我在两个不同的文件中有两个不同的模块签名。它们具有相同的字段名称，但行为不同。

而里面的函子定义了另一个函子。

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模块签名内部使用。trsIntTPImint_inttrsIntTMI

这是我定义它的方式：

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？感谢您的帮助。

4

1 回答 1

3

实际上，在 的定义中redPair，您无法保证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 中使用模块和仿函数。大多数情况下，您实际上只需要依赖记录。模块和函子对每个人来说都很复杂，你必须关心抽象、共享约束等。

现状似乎是您应该避免使用它们，除非您确实需要它们来提供它们对依赖记录的功能：抽象和/或子类型化。

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

但如果你只是在做实验，请用它们做实验。很高兴了解各种可能性以及每种可能性的优缺点。

于 2013-04-04T04:06:13.967 回答