默認實現

Question

我有我想要實現數倍的接口：

Module Type I. 
    Parameter a : A. 
    Parameter b : B. 
    Parameter c : C. 
End I. 

（並假設每個a，b和c實際上許多定義）。

的實現將是

Module Imp1 <: I. 
    Definition a : A := bar. 
    Definition b : B := foo a. 
    Definition c : C := baz a b. 
End I. 

現在事實證明，許多實現共享的b定義（這需要a），但有c不同的定義。

如何集中b的定義？最好不要改變I或重複大量的定義？

（我想編寫一個模塊仿BImp期待a:A爲某種參數，然後我可以Import (BImp a)。）

Answer 1

你可以外包你的共享定義爲參數的改變零件的全球化定義（這裏outsourced）你的模塊（這裏是a）。我不知道是否有像Haskell的默認實現。

Module Type I. 
    Parameter a : A. 
    Parameter b : B. 
    Parameter c : C. 
End I. 

Definition outsourced (a:A) := foo a. 

Module Imp1 <: I. 
    Definition a : A := bar. 
    Definition b : B := outsourced a. 
    Definition c : C := baz a b. 
End Imp1. 

Module Imp2 <: I. 
    Definition a : A := bar'. 
    Definition b : B := outsourced a. 
    Definition c : C := baz' a b. 
End Imp2. 

Answer 2

您可以在其他模塊內安裝模塊。這迫使您複製模塊的簽名的一部分，但不是模塊包含的證明。

Module Type PreorderSignature. 
Parameter Inline type : Type. 
Parameter Inline less : type -> type -> Prop. 
Parameter Inline reflexivity : forall x1, less x1 x1. 
Parameter Inline transitivity : forall x1 x2 x3, less x1 x2 -> less x2 x3 -> less x1 x3. 
End PreorderSignature. 

Module Preorder (PS : PreorderSignature). 
Import PS. 
(* Preorder facts. *) 
End Preorder. 

Module Type EquivalenceRelationSignature. 
Parameter Inline type : Type. 
Parameter Inline equal : type -> type -> Prop. 
Parameter Inline reflexivity : forall x1, equal x1 x1. 
Parameter Inline symmetry : forall x1 x2, equal x1 x2 -> equal x2 x1. 
Parameter Inline transitivity : forall x1 x2 x3, equal x1 x2 -> equal x2 x3 -> equal x1 x3. 
End EquivalenceRelationSignature. 

Module EquivalenceRelation (ERS : EquivalenceRelationSignature). 
Import ERS. 
Module PreorderSignatureInstance <: PreorderSignature. 
Definition type := type. 
Definition less := equal. 
Definition reflexivity := reflexivity. 
Definition transitivity := transitivity. 
End PreorderSignatureInstance. 
Module PreorderInstance := Preorder PreorderSignatureInstance. 
Import PreorderInstance. 
(* Now your equivalence relations will inherit all the facts about preorders. *) 
(* Other equivalence relation facts. *) 
End EquivalenceRelation. 

Module Type PartialOrderSignature. 
Parameter Inline type : Type. 
Parameter Inline less : type -> type -> Prop. 
Parameter Inline reflexivity : forall x1, less x1 x1. 
Parameter Inline antisymmetry : forall x1 x2, less x1 x2 -> less x2 x1 -> x1 = x2. 
Parameter Inline transitivity : forall x1 x2 x3, less x1 x2 -> less x2 x3 -> less x1 x3. 
End PartialOrderSignature. 

Module PartialOrder (POS : PartialOrderSignature). 
Import POS. 
Module PreorderSignatureInstance <: PreorderSignature. 
Definition type := type. 
Definition less := less. 
Definition reflexivity := reflexivity. 
Definition transitivity := transitivity. 
End PreorderSignatureInstance. 
Module PreorderInstance := Preorder PreorderSignatureInstance. 
Import PreorderInstance. 
(* Now your partial orders will inherit all the facts about preorders. *) 
(* Other partial order facts. *) 
End PartialOrder. 

並平整模塊層次一點，你可以使用Import和Parameter Inline命令。