3

Agda で代数構造の新しいレコード型を宣言する 2 つのスタイルを比較したいと思います。

標準の Agda パッケージで使用されているスタイルに従って、次のようにAlgebra定義できます。BoundedJoinSemilattice

record IsBoundedJoinSemilattice {a ℓ} {A : Set a}
                                (_≈_ : Rel A ℓ) (_∨_ : Op₂ A) (⊥ : A) : Set (a Level.⊔ ℓ) where
   field
      isCommutativeMonoid : IsCommutativeMonoid _≈_ _∨_ ⊥
      idem : Idempotent _≈_ _∨_

   open IsCommutativeMonoid isCommutativeMonoid public

record BoundedJoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 6 _∨_
   infix  4 _≈_
   field
      Carrier : Set c
      _≈_ : Rel Carrier ℓ
      _∨_ : Op₂ Carrier
      ⊥ : Carrier
      isBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ _∨_ ⊥

   open IsBoundedJoinSemilattice isBoundedJoinSemilattice public

   commutativeMonoid : CommutativeMonoid _ _
   commutativeMonoid = record {
         Carrier = Carrier;
         _≈_ = _≈_;
         _∙_ = _∨_;
         ε = ⊥;
         isCommutativeMonoid = isCommutativeMonoid
      }

このアプローチでは、 のフィールドは(名前の変更まで) 、、、およびなどの他のより抽象的な構造のフィールドBoundedJoinSemiLatticeと重複します。a をその「スーパータイプ」の 1 つとして表示するには、そのフィールドをスーパータイプのフィールドにマッピングする射影関数 (上記の関数など) を呼び出す必要があります。SetoidSemigroupMonoidCommutativeMonoidBoundedJoinSemiLatticeBoundedJoinSemiLatticecommutativeMonoid

ただし、このフィールドの重複は、あまり具体的でない代数構造からより具体的な代数構造を構築するコードの重要なボイラープレートにつながる可能性があります。より自然な定義は次のようになります (名前CommutativeMonoidを に変更CM):

record IsBoundedJoinSemilattice {c ℓ} (cm : CM c ℓ)
                                      (⊥ : CM.Carrier cm) : Set (c Level.⊔ ℓ) where
   field
      isCommutativeMonoid : IsCM (CM._≈_ cm) (CM._∙_ cm) ⊥
      idem : Idempotent (CM._≈_ cm) (CM._∙_ cm)

   open IsCommutativeMonoid isCommutativeMonoid public

record BoundedJoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
   field
      commutativeMonoid : CM c ℓ
      isBoundedJoinSemilattice : IsBoundedJoinSemilattice commutativeMonoid (CM.ε commutativeMonoid)

   open CommutativeMonoid commutativeMonoid public using (Carrier; _≈_) renaming (
         _∙_ to _∨_;
         ε to ⊥
      )
   open IsBoundedJoinSemilattice isBoundedJoinSemilattice public

ここでの考え方は、CommutativeMonoidintoのフィールドを複製するのBoundedJoinSemilatticeではなく、後者が type の単一のフィールドを宣言することCommutativeMonoidです。次に、 を使用して、open...publicそのサブフィールドを含むレコードに「継承」します。実際、これは の標準ライブラリの他の場所で使用されているイディオムとまったく同じですが、Algebra.Structuresここでは継承されたフィールドの名前も変更して、継承コンテキストで適切に名前が付けられるようにしています。

この 2 番目の方法は冗長性が低いだけでなく、 aBoundedJoinSemilatticeから aを作成したいクライアント コードは、作成CommutativeMonoid中のレコードに単純にそれを引数として渡すことができます。一方、BoundedJoinSemilatticeゼロから を構築したいクライアント コードは、中間の を構築する必要がありますCommutativeMonoid。

Algebraモジュールがこの継承スタイルを使用しない 理由はありAlgebra.Structuresますか? たぶん、私が見つけていない 2 番目のアプローチに問題があるか、またはおそらく大きな違いはないでしょうBoundedJoinSemiLattice。CommutativeMonoid、2番目のアプローチの利便性の多くを回復します。

4

1 に答える 1

4

2 番目のアプローチで見られる主な問題は、複数の構造を構成 (「継承」) できないことです。ポイントを で説明しましょう。CommutativeSemiringからの定義には 2 つのAlgebra.Structuresが必要です。IsCommutativeMonoid

record IsCommutativeSemiring
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (_+_ _*_ : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    +-isCommutativeMonoid : IsCommutativeMonoid ≈ _+_ 0#
    *-isCommutativeMonoid : IsCommutativeMonoid ≈ _*_ 1#
    distribʳ              : _*_ DistributesOverʳ _+_
    zeroˡ                 : LeftZero 0# _*_

  -- ...

ここで、提案されたソリューションを使用したと想像してください。次のようIsCommutativeSemiringになります。

record IsCommSemiring {c ℓ}
  (+-cm : CommutativeMonoid c ℓ)
  (*-cm : CommutativeMonoid c ℓ) : Set (c ⊔ ℓ) where
  open CommutativeMonoid +-cm
    using (_≈_)
    renaming (_∙_ to _+_; ε to 0#)
  open CommutativeMonoid *-cm
    using ()
    renaming (_∙_ to _*_; ε to 1#)
  open FunProps _≈_

  -- more stuff goes here

Carrierそして今、あなたは深刻な問題に直面しています:それぞれの の が何であるかはわかりませんCommutativeMonoidが、それらは同じ型である方がよいでしょう。したがって、すでにこの醜いステップを実行する必要があります。

record IsCommSemiring {c ℓ}
  (+-cm : CommutativeMonoid c ℓ)
  (*-cm : CommutativeMonoid c ℓ) : Set (suc (c ⊔ ℓ)) where
  open CommutativeMonoid +-cm
    using (_≈_)
    renaming (Carrier to +-Carrier; _∙_ to _+_; ε to 0#)
  open CommutativeMonoid *-cm
    using ()
    renaming (Carrier to *-Carrier; _∙_ to _*′_; ε to 1#′; _≈_ to _≈′_)
  open FunProps _≈_

  field
    carriers : *-Carrier ≡ +-Carrier

次に、 の助けを借りて、で動作するものをsubst定義する必要があります。_*_+-Carrier

  _*_ : (x y : +-Carrier) → +-Carrier
  _*_ = subst (λ A → A → A → A) carriers _*′_

そして最後に、分配性のためのフィールドを書くことができます:

  field
    distribʳ : _*_ DistributesOverʳ _+_

これはすでに非常にぎこちなく見えますが、さらに悪いことに、基礎となる等式も同じでなければなりません! これは最初はそれほど大きな問題ではないように思えるかもしれませんが、require するだけでよいのですが_≈_ ≡ _≈′_(まあ、_≈_ ≡ subst (λ A → A → A → Set ℓ) carriers _≈′_実際には)、誰かが証明を使おうとすると、驚きます。実際、これらの証明を使用する最初の人になることができることに驚くかもしれません。IsCommutativeSemiringfromを見るとAlgebra.Structures、次のコードが見つかります。

  distrib : _*_ DistributesOver _+_
  distrib = (distribˡ , distribʳ)
    where
    distribˡ : _*_ DistributesOverˡ _+_
    distribˡ x y z = begin
      (x * (y + z))        ≈⟨ *-comm x (y + z) ⟩
      ((y + z) * x)        ≈⟨ distribʳ x y z ⟩
      ((y * x) + (z * x))  ≈⟨ *-comm y x ⟨ +-CM.∙-cong ⟩ *-comm z x ⟩
      ((x * y) + (x * z))  ∎

あなたのバージョンでそれを書こうとすると、あちこちにあるでしょうsubst。この時点でできる唯一のことは、 を使用するすべての証明を_≈′_その_≈_形式 (これも大量のsubsts) に書き直すことです。

「コンストラクター」関数を使用したアイデアを考えると、これは確かに実行可能です。しかし、繰り返しますが、複数の構造を構成したい場合に問題が発生します。

Monoidaから aを作成する方法は次のSemigroupとおりです。

semigroup→monoid : ∀ {c ℓ} (s : Semigroup c ℓ) →
  let open Semigroup s
      open FunProps _≈_
  in (ε : Carrier) (identity : Identity ε _∙_) → Monoid c ℓ
semigroup→monoid s ε id = record
  { Carrier = Carrier
  ; _≈_ = _≈_
  ; _∙_ = _∙_
  ; ε   = ε
  ; isMonoid = record
    { isSemigroup = isSemigroup
    ; identity    = id
    }
  }
  where
  open Semigroup s

実際には、isSemigroupほとんどのレコード ( Carrier、_≈_および_∙_) を一意に決定し、idも決定するためε、次のように書くこともできます。

semigroup→monoid s ε id = record
  { isMonoid = record
    { isSemigroup = Semigroup.isSemigroup s
    ; identity    = id
    }
  }

これは実際には非常に簡潔です。

于 2014-01-09T18:35:26.223 に答える