3

我想对比两种在 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、和。为了将 a视为其“超类型”之一，必须调用一个投影函数，该函数负责将其字段映射到超类型的字段，例如上面的函数。SemigroupMonoidCommutativeMonoidBoundedJoinSemiLatticeBoundedJoinSemiLatticecommutativeMonoid

但是，这种字段重复可能会导致代码中出现大量样板，这些样板会从不太具体的代数结构中构建出更具体的代数结构。更自然的定义可能是这样的（重命名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。然后我们使用 anopen...public将其子字段“继承”到包含记录中。事实上，这正是标准库中其他地方使用的惯用语Algebra.Structures，除了这里我们还重命名了继承的字段，以便在继承上下文中适当地命名它们。

第二种方法不仅不那么冗余，而且现在想要BoundedJoinSemilattice从 a构造 a 的客户端代码CommutativeMonoid可以简单地将其作为参数传递给正在构造的记录。另一方面，想要BoundedJoinSemilattice从头构造 a 的客户端代码现在必须构造一个中间CommutativeMonoid.

Algebra模块不使用这种继承风格 是有原因的Algebra.Structures吗？也许第二种方法存在我没有发现的问题，或者它没有太大区别：例如，对于第一种方法，也许可以简单地定义一个“构造函数”来处理BoundedJoinSemiLattice从 a 构造 a CommutativeMonoid，恢复了第二种方法的很多便利。

4

1 回答 1

4

我在第二种方法中看到的主要问题是您不能组合（“继承”）多个结构。让我用 来说明这一点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

现在你遇到了严重的麻烦：你不知道Carrier各个CommutativeMonoids 的 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 _≈′_实际上），但是当有人尝试使用证明时，他们会感到惊讶。您可能还会惊讶于您实际上可以成为第一个使用这些证明的人。查看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）——这就提出了一个问题：它仍然值得吗？

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

以下是Monoid从 a制作 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 回答