爲代數結構聲明記錄類型的推薦約定

Question

我想對比兩種樣式來爲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是重疊（最多重命名）與其他任何領域更抽象的結構如Setoid,Semigroup,Monoid和CommutativeMonoid是重複在BoundedJoinSemiLattice。爲了將BoundedJoinSemiLattice作爲它的「超類型」之一來查看，必須調用投影函數來負責將其字段映射到超類型的字段，例如上面的​​函數。

但是，這種字段重複可能會導致代碼中的重要樣板文件，這些代碼構建更具體的代數結構。而更自然的定義可能是這樣的（重命名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 

這裏，想法是不重複的CommutativeMonoid領域爲BoundedJoinSemilattice，而後者申報類型的單場CommutativeMonoid。然後，我們使用open...public將其子字段「繼承」到包含的記錄中。事實上，這正是Algebra.Structures中標準庫中其他地方使用的成語，除了這裏我們也重命名了繼承的字段，以便它們在繼承上下文中被適當地命名。

這不僅是第二種方法不那麼多餘，但是現在想要從CommutativeMonoid構造一個BoundedJoinSemilattice的客戶端代碼可以簡單地將它作爲參數傳遞給正在構建的記錄。另一方面，想要從零開始構建BoundedJoinSemilattice的客戶端代碼現在必須構建中間CommutativeMonoid。

是否有一個原因Algebra模塊不使用這種繼承風格，但Algebra.Structures呢？也許第二種方法存在問題，我還沒有發現，或者它沒有太大的區別：例如，第一種方法，也許可以簡單地定義一個「構造函數」函數，它可以處理構建BoundedJoinSemiLattice一個CommutativeMonoid，以恢復第二種方法的許多便利。

Answer 1

我用第二種方法看到的主要問題是，您不能編寫（「繼承」）多個結構。讓我說明與CommutativeSemiring點，從Algebra.Structures定義需要兩個IsCommutativeMonoid S：

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 S上的各個CommutativeMonoid S的，但它們最好是同一類型。所以，你已經使這個醜陋的一步：

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ʳ _+_ 

這看起來很尷尬，但它變得更糟：底層的平等也應該是一樣的！起初這似乎不是一個大問題，你可以只需要_≈_ ≡ _≈′_（實際上，_≈_ ≡ subst (λ A → A → A → Set ℓ) carriers _≈′_），但是當有人試圖使用這些證明時，他們會感到驚訝。事實上，您可能會第一個使用這些證明，但您也可能會感到驚訝。看着IsCommutativeSemiring從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所有的地方。在這一點上你唯一能做的就是重寫所有使用_≈′_到_≈_表格（再次，噸數爲subst s）的證明 - 這就產生了一個問題：它還值得嗎？

---

考慮到你的想法與「構造函數」函數：這當然是可行的。但是，當你想編寫多個結構時，你會遇到問題。

這裏是你如何做一個Monoid從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 
    } 
    } 

這實際上非常簡潔。