Recommended convention for declaring record types for algebraic structures
-
21-12-2019 - |
Вопрос
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.
Решение
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 IsCommutativeMonoid
s:
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 Carrier
s of the respective CommutativeMonoid
s 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 subst
s) - 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.