實施模塊中從模塊簽名導入符號

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的==表示法的定義。