Есть ли более удобный способ использовать вложенные записи?

Как я уже говорил ранее, я работаю в библиотеке по алгебре, матрицам и теории категорий. Я разложил алгебраические структуры в "башне" типов записей, каждый из которых представляет собой алгебраическую структуру. Например, чтобы определить моноид, мы сначала определяем полугруппу, а для определения коммутативного моноида мы используем определение моноида, следуя той же схеме, что и стандартная библиотека Agda.

Моя беда в том, что когда мне нужно свойство алгебраической структуры, которое глубоко в рамках другого (например, свойства a Monoid, являющегося частью a 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)
Обратите внимание, что для того, чтобы получить доступ к свойству левого тождества моноида, мне нужно спроецировать его из моноида, который находится внутри коммутативного моноида, лежащего в структуре коммутативного полукольца.

Меня беспокоит то, что, по мере того как я добавляю все больше и больше алгебраические структуры, такие леммы он станет нечитабельным.

Мой вопрос: есть ли какая-то схема или трюк, который может избежать этой "лестницы" рекордных проекций?

Любая подсказка по этому вопросу очень приветствуется.

1 2
agda

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-реэкспортируя эти поля из 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
5