实施模块中从模块签名导入符号

Question

如何在HomCategory中提供Category中定义的符号？

Module Type Category. 

    Parameter Object : Type. 
    Parameter Arrow : Object -> Object -> Type. 

    Infix "~>" := Arrow (at level 25) : category_scope. 
    Open Scope category_scope. 
    Delimit Scope category_scope with category. 
    Bind Scope category_scope with Object Arrow. 

    Variable id : forall a : Object, a ~> a. 
    ... 
End Category. 

Module HomCategory <: Category. 

    Definition Object := Type. 
    Definition Arrow(a b : Object) := a -> b. 

    Print Scope category_scope. (* Error: Scope category_scope is not declared. *) 
    ... 
End HomCategory. 

Answer 1

恐怕没有办法做到这一点。 Coq中模块的状态很奇怪，这意味着Module Type与此类型之间的唯一连接是Coq检查定义与签名是否兼容。模块中的Arrow声明并不是真正的一流实体。因此，应该没有办法在签名中定义的符号与您的实现之间建立联系。有两种选择让我浮想联翩：

• 每当你想用新的东西来重新声明你的符号。

• 不要将模块用于ad-hoc多态性。通过规范结构或类型类，多态操作确实在理论上具有一流的地位，从而更容易定义这种通用符号。在ssreflect：http://ssr.msr-inria.inria.fr/~jenkins/current/eqtype.html中查看eqtype的==表示法的定义。