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

Question

正如我之前所说,我正在一个关于代数,矩阵和范畴理论的图书馆工作.我已经在记录类型的"塔"中分解了代数结构,每个代表一个代数结构.例如,为了指定一个monoid,我们首先定义一个半群并定义一个可交换的monoid,我们使用monoid定义,遵循与Agda标准库相同的模式.

我的麻烦的是,当我需要的代数结构,它是内另一个深(例如的属性的属性Monoid是的一部分CommutativeSemiring),我们需要使用数量等于期望的代数结构深度的突起.

作为我的问题的一个例子,请考虑以下"引理":

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)

注意,为了访问monoid的左侧身份属性,我需要从位于交换半环结构中的交换幺半群内的monoid投影它.

我担心的是,随着我添加越来越多的代数结构,这样的引理会变得难以理解.

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

任何线索都非常受欢迎.

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.反过来,setoid,monoid并rawMonoid在Group来自同样open public来自-reexporting这些领域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