有没有更方便的方法来使用嵌套记录？

Question

正如我所说，我在一家图书馆工作，内容涉及代数、矩阵和范畴论。我已经分解了 "tower" 记录类型中的代数结构，每个记录类型代表一个代数结构。例如，要指定一个幺半群，我们首先定义一个半群并定义一个交换幺半群，我们使用幺半群定义，遵循与 Agda 标准库相同的模式。

我的麻烦是，当我需要代数结构的属性时，它位于另一个代数结构的深处（例如 Monoid 的属性是 [=12 的一部分=]) 我们需要使用多个等于所需代数结构深度的投影。

作为我的问题的一个例子，请考虑以下 "lemma"：

open import Algebra
open import Algebra.Structures
open import Data.Vec
open import Relation.Binary.PropositionalEquality
open import Algebra.FunctionProperties
open import Data.Product

module _ {Carrier : Set} {_+_ _*_ : Op₂ Carrier} {0# 1# : Carrier} (ICSR : IsCommutativeSemiring _≡_ _+_ _*_ 0# 1#) where

csr : CommutativeSemiring _ _
csr = record{ isCommutativeSemiring = ICSR }

zipWith-replicate-0# : ∀ {n}(xs : Vec Carrier n) → zipWith _+_ (replicate 0#) xs ≡ xs
zipWith-replicate-0# [] = refl
zipWith-replicate-0# (x ∷ xs) = cong₂ _∷_ (proj₁ (IsMonoid.identity (IsCommutativeMonoid.isMonoid
                                                           (IsCommutativeSemiring.+-isCommutativeMonoid
                                                           (CommutativeSemiring.isCommutativeSemiring csr)))) x)
                                          (zipWith-replicate-0# xs)

请注意，为了访问幺半群的左恒等式属性，我需要从位于交换半环结构中的交换幺半群内的幺半群进行投影。

我担心的是，随着我添加越来越多的代数结构，这样的引理将变得不可读。

我的问题是：是否有可以避免这种 "ladder" 记录预测的模式或技巧？

非常欢迎任何关于此的线索。

Answer 1

如果您查看 Agda 标准库，您会发现对于大多数专用代数结构，定义它们的 record 具有不太专用的结构 open public。例如。在 Algebra.AbelianGroup 中，我们有：

record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
  -- ...  snip ...

  open IsAbelianGroup isAbelianGroup public

  group : Group _ _
  group = record { isGroup = isGroup }

  open Group group public using (setoid; semigroup; monoid; rawMonoid)

  -- ... snip ...

因此 AbelianGroup 记录不仅有 AbelianGroup/IsAbelianGroup 字段可用，还有 setoid、semigroup 和 monoid 和 rawMonoid 来自 Group。反过来，Group 中的 setoid、monoid 和 rawMonoid 来自类似的 open public-从 Monoid.

重新导出这些字段

类似地，对于代数属性 witnesses，他们重新导出不太专业的版本的字段，例如在 IsAbelianGroup 我们有

record IsAbelianGroup
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (∙ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
  -- ... snip ...
  open IsGroup isGroup public
  -- ... snip ...

然后IsGroup再导出IsMonoid，IsMonoid再导出IsSemigroup，依此类推。因此，如果您打开 IsAbelianGroup，您仍然可以使用 assoc（来自 IsSemigroup），而无需手动写出整个路径。

底线是您可以按如下方式编写函数：

open CommutativeSemiring CSR hiding (refl)
open import Function using (_⟨_⟩_)

zipWith-replicate-0# : ∀ {n}(xs : Vec Carrier n) → zipWith _+_ (replicate 0#) xs ≡ xs
zipWith-replicate-0# [] = refl
zipWith-replicate-0# (x ∷ xs) = proj₁ +-identity x ⟨ cong₂ _∷_ ⟩ zipWith-replicate-0# xs

有没有更方便的方法来使用嵌套记录？

Is there a more convenient way to use nested records?

record

agda