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

Question

正如我所说 before ，我在一家关于代数、矩阵和范畴论的图书馆工作。我已经将代数结构分解为记录类型的“塔”，每个记录类型代表一个代数结构。例如，要指定一个幺半群，我们首先定义一个半群，然后定义一个交换幺半群，我们使用幺半群定义，遵循与 Agda 标准库相同的模式。

我的问题是，当我需要一个深入另一个代数结构的属性时(例如 CommutativeSemiring 的一部分的 Monoid 的属性)我们需要使用多个等于所需代数结构深度的投影。

作为我的问题的一个例子，考虑以下“引理”:

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)

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

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

我的问题是:是否有一种模式或技巧可以避免这种记录预测的“阶梯”？

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

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，来自 Group 的 semigroup 和 monoid 和 rawMonoid。反过来，Group中的setoid、monoid和rawMonoid同样来自open public - 从 Monoid 中重新导出这些字段。

类似地，对于代数属性见证，它们重新导出不太特化版本的字段，例如在 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