[Agda] algebra hierarchy in library

[Matthew Daggitt]

1. Why `Raw' structures?

Sometimes you only need the raw operators without assuming any properties
over them. See for example the coefficient ring for the ring solver
<https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Solver/Ring.agda>.
You could of course change this to require the full ring axioms but this is
a) more work for the user and b) unnecessary. The raw versions aren't
widely used but they don't affect the hierarchy in anyway so there's no
harm in having them.

2. Why putting `Is' structures into a different file?

This was an inherited design decision. I know it differs from the way the
library is laid out in `Relation.Binary`. The advantage of having them
separately is that the module can be parameterised by the equality. See
`Data.Nat.Properties` for a use of this. I agree it's a little irritating
having to open both `Algebra` and `Algebra.Structures`. It may be that
`Algebra` should re-export `Algebra.Structures`. I'm unsure of how to
standardise this with `Relation.Binary`.

3. Why Magma declares the fields  Carrier and _≈_  by new?

You've answered your own question here with your magma product example.
It's exactly as you describe. If you have two structures of the type `IsX`
and you want to combine them, you can specify exactly how the parameters of
the two interact to form the 3rd `IsX` type. This wouldn't be possible (or
much harder anyway) using Version II. Version I requires a little more
boiler plate code (written by the library maintainers) but it makes the
hierarchy much easier to use in practice (on the user end).




On Fri, Mar 8, 2019 at 3:00 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> Dear standard library developers and supporters,
>
> can you please answer in (simple words) several questions about the
> representation of the algebraic hierarchy in standard library?
>
>
> 1. Why `Raw' structures?
>
> There are classical generic algebraic structures (call them GAS):
> Magma, Semigroup, Monoid, and so on.
>
> Those of them having some new field respectively to previous structures
> are accompanied with the corresponding `Raw' record. For example, Magma
> is preceded with RawMagma, Monoid with RawMonoid. Each `Raw' structure
> expresses only the signature of the corresponding GAS.
>
> What the `Raw' structures serve for?
>
>
> 2. Why putting `Is' structures into a different file?
>
> For example, the reader looks into Algebra.agda to find what is
> Semigroup:
>
> -------------------------------------------------------
>   record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
>     ...
>     field Carrier     : Set c
>           _≈_         : Rel Carrier ℓ
>           _∙_         : Op₂ Carrier
>           isSemigroup : IsSemigroup _≈_ _∙_
>
>     open IsSemigroup isSemigroup public
>     ...
>     magma = record { isMagma = isMagma }
>     ...
>
> Now, one needs to find a declaration for IsSemigroup.
> And it resides in a different file of
>                                    Algebra/Structures.agda :
>
>   record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
>     field
>       isMagma : IsMagma ∙
>       assoc   : Associative ∙
>
>     open IsMagma isMagma public
> ---------------------------------------------------------
>
> And all this implements the meaning of a small sentence:
> ``Semigroup is Magma in which multiplication _∙_ is associative''.
>
> Why not put ``record IsSemigroup'' before ``record Semigroup'' in the
> same file  Algebra.agda ?
>
> Similarly other `Is' GAS decls can join. So that Algebra.agda and
> Algebra/Structures.agda will merge into  Algebra.agda   in which each
> GAS will be defined in one place.
> For example, to see what is a group will need to look into one file, not
> in two files.
> ?
>
>
> 3. Why Magma declares the fields  Carrier and _≈_  by new?
>
> Similarly, why other GAS re-declare many fields?
>
> In theory, we have
> ``Magma is a setoid with an operation _∙_ congruent with respect to the
> equality _≈_''.
>
> So, Magma inherits Setoid. And it is natural for its representation in
> Agda to have  setoid  somewhere inside it. So, it opens this setoid and
> uses its fields in further definitions. For example, like this:
>
> -- Version II ---------------------------------------------------------
>
> record IsMagma {α α=} (S : Setoid α α=) (_∙_ : Op₂ (Setoid.Carrier S)) :
>                                                            Set (α ⊔ α=)
>   where
>   open Setoid S using (_≈_; Carrier)
>   field
>     ∙cong : _∙_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
>
> record Magma α α= :  Set (suc (α ⊔ α=))
>   where
>   field  setoid : Setoid α α=
>
>   open Setoid setoid public
>   infixl 7 _∙_
>
>   field  _∙_     : Op₂ Carrier
>          isMagma : IsMagma setoid _∙_
> ------------------------------------------------------------------------
>
> And let us call  Version I  the approach of Standard library lib-0.17.
>
> Both versions use an `Is' structure, but II does not re-declare fields.
> Is not II more natural?
>
>
> Another question may be:
> ``why splitting each GAS into proper structure and `Is' structure?''.
>
> My guess is that this approach allows us to express two GAS-s that are
> over the same inherited GAS. For example, a programmer can express a
> product of two Magmae over the same Setoid:
> ------------------------------------------------------------
> module _ {α α=} (S : Setoid α α=)
>   where
>   open Setoid S using (Carrier; _≈_)
>   SS = ×-setoid S S
>   open Setoid SS using () renaming (Carrier to CC; _≈_ to _=p_)
>
>   magmaProduct' :
>     (_*₁_ _*₂_ : Op₂ Carrier) → IsMagma _≈_ _*₁_ →
>                                 IsMagma _≈_ _*₂_ → Magma α α=
>   magmaProduct' _*₁_ _*₂_ insM₁ isM₂ =
>                        <define coordinate-wise multiplcation on CC;
>                         prove ...;  return the Magma record
>                        >
> ------------------------------------------------------------
>
> (is there any other purpose to introduce `Is' -structures?).
>
> This is equally easy to set both in Version I and Version II.
>
> But note that both approaches still deviate, a bit, from the theory.
> Because in theory, it is
> \ (mg1 : Magma_ _) (mg2 : Magma _ _) (HaveCommonSetoid mg1 mg2) →
> product-magma,
> while magmaProduct' takes certain parts of the two magmae.
>
> So, there remain somewhat three and a half questions.
>
> Thank you in advance for your possible explanation.
>
> ------
> Sergei
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190308/d1d05768/attachment.html>