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

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)

请注意，为了访问单子群的左单位属性，我需要从交换半环结构中的交换单子群中投影出它。

我的担忧是，随着我添加越来越多的代数结构，这些引理将变得难以阅读。

我的问题是：是否有一种模式或技巧可以避免这种“梯子”记录投影？

对此的任何线索都非常欢迎。

- Rodrigo Ribeiro

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字段，还具有来自Group的setoid、semigroup和monoid以及rawMonoid字段。反过来，在Group中，setoid、monoid和rawMonoid来自类似地从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

- Cactus