为代数结构声明记录类型的推荐约定

Question

我想对比两种在 Agda 中为代数结构声明新记录类型的风格。

按照标准 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 和 @987654328 @ 在BoundedJoinSemiLattice 中重复。为了将BoundedJoinSemiLattice 视为其“超类型”之一，必须调用一个投影函数，负责将其字段映射到超类型的字段，例如上面的commutativeMonoid 函数。

但是，这种字段重复可能会导致代码中出现大量样板文件，这些样板文件会从不太具体的代数结构中构建出更具体的代数结构。更自然的定义可能是这样的（将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 使用这种继承风格有什么原因吗？也许第二种方法存在我没有发现的问题，或者它没有太大区别：例如，对于第一种方法，也许可以简单地定义一个“构造函数”来处理 @987654346 的构造@来自CommutativeMonoid，以恢复第二种方法的大部分便利。

Answer 1

我看到第二种方法的主要问题是您不能组合（“继承”）多个结构。让我用CommutativeSemiring来说明这一点，Algebra.Structures的定义需要两个IsCommutativeMonoids：

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

现在你遇到了严重的麻烦：你不知道各个CommutativeMonoids 的Carriers 是什么，但它们最好是同一类型。所以你已经不得不迈出这丑陋的一步了：

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 _≈′_），但是当有人试图使用证明时，他们会感到惊讶。您可能还会惊讶于您实际上可以成为第一个使用这些证明的人。从Algebra.Structures查看IsCommutativeSemiring，我们发现了这段代码：

  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）——这就提出了一个问题：它仍然值得吗？

---

用“构造函数”函数考虑你的想法：这当然是可行的。但是话又说回来，当您想要组合多个结构时会遇到问题。

以下是如何从Semigroup 生成Monoid：

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
    }
  }

其实很简洁。