Блог

У меня есть интерфейс, который я хочу реализовать несколько раз:

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

Вы можете передать свои общие определения на аутсорсинг в глобальное определение (здесь 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.
  

Вы можете создавать экземпляры модулей внутри других модулей. Это вынуждает вас дублировать часть подписей модулей, но не доказательства, содержащиеся в модулях.

 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 and Parameter Inline .