Gibt es eine bequemere Möglichkeit, verschachtelte Datensätze zu verwenden?

Question

Wie ich before erzählte, arbeite ich in einer Bibliothek über Algebra, Matrizen und Kategorientheorie. Ich habe die algebraischen Strukturen in einem "Turm" von Datensatztypen zerlegt, von denen jeder eine algebraische Struktur darstellt. Um zum Beispiel ein Monoid zu spezifizieren, definieren wir zuerst eine Halbgruppe und definieren ein kommutatives Monoid. Wir verwenden eine Monoiddefinition, die dem gleichen Muster folgt wie die Agda-Standardbibliothek.

Mein Problem ist, dass, wenn ich eine Eigenschaft einer algebraischen Struktur benötigen, das innerhalb eines anderen (zB Eigenschaft eines Monoid, die Teil eines CommutativeSemiring ist) tief ist, dass wir eine Nummer eines Vorsprüngen gleich gewünschten algebraische Struktur verwenden müssen Tiefe.

Als Beispiel für mein Problem, betrachten Sie das folgende „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) 

Beachten Sie, dass, um die linke IDENTITY einer Monoid zuzugreifen, muss ich es aus dem Monoid projizieren, die in ist das kommutative Monoid, das in der Struktur eines kommutativen Semirings liegt.

Meine Sorge ist, dass, wenn ich mehr und mehr algebraische Strukturen hinzufügen, solche Lemmas wird es unlesbar werden.

Meine Frage ist: Gibt es ein Muster oder einen Trick, die diese "Leiter" von Rekordprojektionen vermeiden können?

Jeder Hinweis darauf ist sehr willkommen.

Answer 1

Wenn Sie sich die Agda-Standardbibliothek anschauen, sehen Sie, dass für die meisten spezialisierten algebraischen Strukturen die record Definition die weniger spezialisierte Struktur open public hat. Z.B. in Algebra.AbelianGroup, haben wir:

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 ...  

So ein AbelianGroup Rekord nicht nur die AbelianGroup/IsAbelianGroup Felder zur Verfügung haben, aber auch setoid, semigroup und monoid und rawMonoid von Group. Im Gegenzug kommen , monoid und rawMonoid in Group von ähnlich open public -reexporting diese Felder von Monoid.

Ähnlich, für Zeugen der algebraischen Eigenschaft, reexportieren sie die Felder der weniger spezialisierten Version, z. in IsAbelianGroup haben wir

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

und dann IsGroup Reexporte IsMonoid, IsMonoid Reexporte IsSemigroup, und so weiter. Und so, wenn Sie IsAbelianGroup geöffnet haben, können Sie immer noch assoc (kommend von IsSemigroup) verwenden, ohne den ganzen Pfad dazu von Hand schreiben zu müssen.

Unterm Strich ist, dass Sie Ihre Funktion schreiben können wie folgt:

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