Recommended convention for declaring record types for algebraic structures

Question

I would like to contrast two styles for declaring new record types for algebraic structures in Agda.

Following the style used in the standard Agda package Algebra, one might define BoundedJoinSemilattice as follows:

record IsBoundedJoinSemilattice {a ℓ} {A : Set a}
                                (_≈_ : Rel A ℓ) (_∨_ : Op₂ A) (⊥ : A) : Set (a Level.⊔ ℓ) where
   field
      isCommutativeMonoid : IsCommutativeMonoid _≈_ _∨_ ⊥
      idem : Idempotent _≈_ _∨_

   open IsCommutativeMonoid isCommutativeMonoid public

record BoundedJoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 6 _∨_
   infix  4 _≈_
   field
      Carrier : Set c
      _≈_ : Rel Carrier ℓ
      _∨_ : Op₂ Carrier
      ⊥ : Carrier
      isBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ _∨_ ⊥

   open IsBoundedJoinSemilattice isBoundedJoinSemilattice public

   commutativeMonoid : CommutativeMonoid _ _
   commutativeMonoid = record {
         Carrier = Carrier;
         _≈_ = _≈_;
         _∙_ = _∨_;
         ε = ⊥;
         isCommutativeMonoid = isCommutativeMonoid
      }

With this approach, any fields of BoundedJoinSemiLattice that overlap (up to renaming) with those of other more abstract structures such as Setoid, Semigroup, Monoid and CommutativeMonoid are duplicated in BoundedJoinSemiLattice. In order to view a BoundedJoinSemiLattice as one of its "supertypes", one must call a projection function responsible for mapping its fields to those of the supertype, such as the commutativeMonoid function above.

However, this field duplication can lead to significant boilerplate in code that builds more specific algebraic structures out of less specific ones. A more natural definition might be something like this (renaming CommutativeMonoid to CM):

record IsBoundedJoinSemilattice {c ℓ} (cm : CM c ℓ)
                                      (⊥ : CM.Carrier cm) : Set (c Level.⊔ ℓ) where
   field
      isCommutativeMonoid : IsCM (CM._≈_ cm) (CM._∙_ cm) ⊥
      idem : Idempotent (CM._≈_ cm) (CM._∙_ cm)

   open IsCommutativeMonoid isCommutativeMonoid public

record BoundedJoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
   field
      commutativeMonoid : CM c ℓ
      isBoundedJoinSemilattice : IsBoundedJoinSemilattice commutativeMonoid (CM.ε commutativeMonoid)

   open CommutativeMonoid commutativeMonoid public using (Carrier; _≈_) renaming (
         _∙_ to _∨_;
         ε to ⊥
      )
   open IsBoundedJoinSemilattice isBoundedJoinSemilattice public

Here, the idea is not to duplicate the fields of CommutativeMonoid into BoundedJoinSemilattice, but rather for the latter to declare a single field of type CommutativeMonoid. We then use an open...public to "inherit" its sub-fields into the containing record. Indeed, this is exactly the idiom used elsewhere in the standard library in Algebra.Structures, except that here we also rename the inherited fields, so that they are appropriately named in the inheriting context.

Not only is this second approach less redundant, but now client code that wants to construct a BoundedJoinSemilattice from a CommutativeMonoid can simply pass it as an argument to the record being constructed. On the other hand, client code that wants to construct a BoundedJoinSemilattice from scratch must now construct an intermediate CommutativeMonoid.

Is there a reason that the Algebra module doesn't use this inheritance style, but Algebra.Structures does? Maybe there are problems with the second approach that I haven't spotted, or perhaps it doesn't make much difference: for example with the first approach, maybe one can simply define a "constructor" function which handles the construction of a BoundedJoinSemiLattice from a CommutativeMonoid, to recover much of the convenience of the second approach.

Answer 1

The main problem I see with the second approach is that you cannot compose ("inherit") more than one structure. Let me illustrate the point with CommutativeSemiring, the definition from Algebra.Structures requires two IsCommutativeMonoids:

record IsCommutativeSemiring
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (_+_ _*_ : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    +-isCommutativeMonoid : IsCommutativeMonoid ≈ _+_ 0#
    *-isCommutativeMonoid : IsCommutativeMonoid ≈ _*_ 1#
    distribʳ              : _*_ DistributesOverʳ _+_
    zeroˡ                 : LeftZero 0# _*_

  -- ...

Now imagine we used your proposed solution. Here's how IsCommutativeSemiring would look like:

record IsCommSemiring {c ℓ}
  (+-cm : CommutativeMonoid c ℓ)
  (*-cm : CommutativeMonoid c ℓ) : Set (c ⊔ ℓ) where
  open CommutativeMonoid +-cm
    using (_≈_)
    renaming (_∙_ to _+_; ε to 0#)
  open CommutativeMonoid *-cm
    using ()
    renaming (_∙_ to _*_; ε to 1#)
  open FunProps _≈_

  -- more stuff goes here

And now you are in serious trouble: you have no idea what the the Carriers of the respective CommutativeMonoids are, but they better be the same type. So you already have to make this ugly step:

record IsCommSemiring {c ℓ}
  (+-cm : CommutativeMonoid c ℓ)
  (*-cm : CommutativeMonoid c ℓ) : Set (suc (c ⊔ ℓ)) where
  open CommutativeMonoid +-cm
    using (_≈_)
    renaming (Carrier to +-Carrier; _∙_ to _+_; ε to 0#)
  open CommutativeMonoid *-cm
    using ()
    renaming (Carrier to *-Carrier; _∙_ to _*′_; ε to 1#′; _≈_ to _≈′_)
  open FunProps _≈_

  field
    carriers : *-Carrier ≡ +-Carrier

And then, with the help of subst, you must define _*_ which works in +-Carrier:

  _*_ : (x y : +-Carrier) → +-Carrier
  _*_ = subst (λ A → A → A → A) carriers _*′_

And finally, you can write the field for distributivity:

  field
    distribʳ : _*_ DistributesOverʳ _+_

This looks very awkward already, but it gets worse: the underlying equalities should be same as well! This might not seem to be a huge issue at first, you can just require _≈_ ≡ _≈′_ (well, _≈_ ≡ subst (λ A → A → A → Set ℓ) carriers _≈′_ in fact), but when someone tries to use the proofs, they're in for a surprise. You might also be surprised that you can, in fact, be the first person to use those proofs. Looking at IsCommutativeSemiring from Algebra.Structures, we find this code:

  distrib : _*_ DistributesOver _+_
  distrib = (distribˡ , distribʳ)
    where
    distribˡ : _*_ DistributesOverˡ _+_
    distribˡ x y z = begin
      (x * (y + z))        ≈⟨ *-comm x (y + z) ⟩
      ((y + z) * x)        ≈⟨ distribʳ x y z ⟩
      ((y * x) + (z * x))  ≈⟨ *-comm y x ⟨ +-CM.∙-cong ⟩ *-comm z x ⟩
      ((x * y) + (x * z))  ∎

If you tried to write that with your version, you'd have subst all over the place. The only thing you can do at this point is to rewrite all proofs that use _≈′_ into their _≈_ form (again, tons of substs) - and this raises a question: is it still worth it?

---

Considering your idea with "constructor" function: this is certainly doable. But then again, you'll run into issues when you want to compose more than one structure.

Here's how you can make a Monoid from a Semigroup:

semigroup→monoid : ∀ {c ℓ} (s : Semigroup c ℓ) →
  let open Semigroup s
      open FunProps _≈_
  in (ε : Carrier) (identity : Identity ε _∙_) → Monoid c ℓ
semigroup→monoid s ε id = record
  { Carrier = Carrier
  ; _≈_ = _≈_
  ; _∙_ = _∙_
  ; ε   = ε
  ; isMonoid = record
    { isSemigroup = isSemigroup
    ; identity    = id
    }
  }
  where
  open Semigroup s

Actually, isSemigroup uniquely determines most of the record (Carrier, _≈_ and _∙_) and id also determines ε, so we can even write:

semigroup→monoid s ε id = record
  { isMonoid = record
    { isSemigroup = Semigroup.isSemigroup s
    ; identity    = id
    }
  }

Which is actually very concise.