<div dir="ltr">Hi Sergei,<div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">(I wonder, why people, - and standard library, - call provers solvers).<br></blockquote><div><br></div><div>Unsure.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">If this is the only reason, then it occurs that `Is' structure is needed<br>only in few cases.<br></blockquote><div><br></div><div>I think your examples miss the point. For example take any binary operator. That binary operator may form many different Semigroups/Monoids/Groups etc. depending on what the underlying equality is. The `Is` structures allow you to expose which equality you're using at a particular point, whereas your suggestion would hide it.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Version II looks more natural to me. But I may be missing something.<br>To make sure, I could rewrite a part of the library for Version II and<br>demonstrate. And what if it occurs better? It will be late to consider<br>for standard. <br></blockquote><div><br></div><div>As I mentioned to you in an issue on Github, non-backwards compatible changes will only be considered where either i) the implementation is incorrect (clearly not the case here) or ii) there's a compelling reason why the current version isn't good enough. "Looking more natural" unfortunately isn't such a reason and as mentioned above Version II doesn't allow you to expose the underlying equality.</div><div>Best,</div><div>Matthew</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Mar 9, 2019 at 6:28 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Sat, 2019-03-09 at 19:08 +0300, Sergei Meshveliani wrote:<br>
> On Sat, 2019-03-09 at 17:08 +0300, Sergei Meshveliani wrote:<br>
> > On Sat, 2019-03-09 at 14:35 +0300, Sergei Meshveliani wrote:<br>
> > <br>
> > > <br>
> > > If this is the only reason, then it occurs that `Is' structure is needed<br>
> > > only in few cases.<br>
> > > For example, <br>
> > > (1) There does not exist different semigroups that inherit ("are over")<br>
> > > the same Magma. The difference can be in a _proof_ for associativity,<br>
> > > but I doubt of whether this feature can be taken here in account. <br>
> > > <br>
> > > Let people correct me if I mistake in the following statements.<br>
> > > <br>
> > > (2) There does not exist different monoids over the same Semigroup.<br>
> > > (3) There does not exist different commutative monoids over the same  <br>
> > >     Monoid.<br>
> > > (4) There does not exist different groups over the same Monoid.<br>
> > > (5) There does not exist different Abelian groups over the same Group.<br>
> > > (6) There does not exist different rings over the same Semiring.<br>
> > > (7) There does not exist different commutative rings over the same <br>
> > >     Ring.<br>
> > [..]<br>
> > <br>
> > <br>
> > Sorry for a silly error. I discover a mistake in (2), (4) (6).<br>
> > <br>
> > For example,  Nat1 = Nat\0  is a semigroup by _+_,  and zero can be<br>
> > joined in different ways, so that (Nat1 U 0) and (Nat1 U 0') occur<br>
> > different monoids. They are isomorphic, but they have different<br>
> > carriers. <br>
> > A similar effect with carrier may be in (4) and (6).<br>
> > <br>
> > So that there remain (1), (3) and (7).<br>
> <br>
> <br>
> No, again an error. <br>
> <br>
> A monoid in _this library_ is on the same carrier C as its inherited<br>
> semigroup. So that to implement a monoid on a given semigroup means to<br>
> choose any e in C which satisfy the law  \forall x (e*x == x*e == x)<br>
> and to prove this law.<br>
> And it is proved above that such  e  is unique.<br>
> <br>
> So, I think that similarly, all the points (1) -- (7) are true<br>
> -- if I am not missing something.<br>
<br>
<br>
<br>
We need one more step towards truth :-)<br>
<br>
Having a Monoid instance, how many different group instances can be<br>
defined on this monoid (hence, on the same carrier C) ? Possible<br>
inversion map on C is unique, as shown in one of previous letters. But<br>
it can be implemented by different algorithms, and this can be used by<br>
programmers. Algorithms matter in the library. And according to Agda,<br>
different algorithms for inversion give different groups. <br>
So that there remain the above statements (1), (3), (7), and may be (2).<br>
<br>
--<br>
SM<br>
<br>
<br>
> <br>
> <br>
> > > <br>
> > > > <br>
> > > > On Fri, Mar 8, 2019 at 3:00 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>><br>
> > > > wrote:<br>
> > > > <br>
> > > >         Dear standard library developers and supporters,<br>
> > > >         <br>
> > > >         can you please answer in (simple words) several questions<br>
> > > >         about the<br>
> > > >         representation of the algebraic hierarchy in standard library?<br>
> > > >         <br>
> > > >         <br>
> > > >         1. Why `Raw' structures?<br>
> > > >         <br>
> > > >         There are classical generic algebraic structures (call them<br>
> > > >         GAS):<br>
> > > >         Magma, Semigroup, Monoid, and so on.<br>
> > > >         <br>
> > > >         Those of them having some new field respectively to previous<br>
> > > >         structures<br>
> > > >         are accompanied with the corresponding `Raw' record. For<br>
> > > >         example, Magma<br>
> > > >         is preceded with RawMagma, Monoid with RawMonoid. Each `Raw'<br>
> > > >         structure<br>
> > > >         expresses only the signature of the corresponding GAS.<br>
> > > >         <br>
> > > >         What the `Raw' structures serve for?<br>
> > > >         <br>
> > > >         <br>
> > > >         2. Why putting `Is' structures into a different file?<br>
> > > >         <br>
> > > >         For example, the reader looks into Algebra.agda to find what<br>
> > > >         is<br>
> > > >         Semigroup:<br>
> > > >         <br>
> > > >         -------------------------------------------------------<br>
> > > >           record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where<br>
> > > >             ...<br>
> > > >             field Carrier     : Set c<br>
> > > >                   _≈_         : Rel Carrier ℓ<br>
> > > >                   _∙_         : Op₂ Carrier<br>
> > > >                   isSemigroup : IsSemigroup _≈_ _∙_<br>
> > > >         <br>
> > > >             open IsSemigroup isSemigroup public<br>
> > > >             ...<br>
> > > >             magma = record { isMagma = isMagma }<br>
> > > >             ...<br>
> > > >         <br>
> > > >         Now, one needs to find a declaration for IsSemigroup.<br>
> > > >         And it resides in a different file of<br>
> > > >                                            Algebra/Structures.agda :<br>
> > > >         <br>
> > > >           record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where<br>
> > > >             field<br>
> > > >               isMagma : IsMagma ∙<br>
> > > >               assoc   : Associative ∙<br>
> > > >         <br>
> > > >             open IsMagma isMagma public<br>
> > > >         ---------------------------------------------------------<br>
> > > >         <br>
> > > >         And all this implements the meaning of a small sentence:<br>
> > > >         ``Semigroup is Magma in which multiplication _∙_ is<br>
> > > >         associative''.<br>
> > > >         <br>
> > > >         Why not put ``record IsSemigroup'' before ``record Semigroup''<br>
> > > >         in the<br>
> > > >         same file  Algebra.agda ?<br>
> > > >         <br>
> > > >         Similarly other `Is' GAS decls can join. So that Algebra.agda<br>
> > > >         and<br>
> > > >         Algebra/Structures.agda will merge into  Algebra.agda   in<br>
> > > >         which each<br>
> > > >         GAS will be defined in one place.<br>
> > > >         For example, to see what is a group will need to look into one<br>
> > > >         file, not<br>
> > > >         in two files.<br>
> > > >         ?<br>
> > > >         <br>
> > > >         <br>
> > > >         3. Why Magma declares the fields  Carrier and _≈_  by new?<br>
> > > >         <br>
> > > >         Similarly, why other GAS re-declare many fields?<br>
> > > >         <br>
> > > >         In theory, we have<br>
> > > >         ``Magma is a setoid with an operation _∙_ congruent with<br>
> > > >         respect to the<br>
> > > >         equality _≈_''.<br>
> > > >         <br>
> > > >         So, Magma inherits Setoid. And it is natural for its<br>
> > > >         representation in<br>
> > > >         Agda to have  setoid  somewhere inside it. So, it opens this<br>
> > > >         setoid and<br>
> > > >         uses its fields in further definitions. For example, like<br>
> > > >         this:<br>
> > > >         <br>
> > > >         -- Version II<br>
> > > >         ---------------------------------------------------------<br>
> > > >         <br>
> > > >         record IsMagma {α α=} (S : Setoid α α=) (_∙_ : Op₂<br>
> > > >         (Setoid.Carrier S)) :<br>
> > > >                                                                    Set<br>
> > > >         (α ⊔ α=)<br>
> > > >           where<br>
> > > >           open Setoid S using (_≈_; Carrier)<br>
> > > >           field<br>
> > > >             ∙cong : _∙_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_<br>
> > > >         <br>
> > > >         record Magma α α= :  Set (suc (α ⊔ α=))<br>
> > > >           where<br>
> > > >           field  setoid : Setoid α α=<br>
> > > >         <br>
> > > >           open Setoid setoid public<br>
> > > >           infixl 7 _∙_<br>
> > > >         <br>
> > > >           field  _∙_     : Op₂ Carrier<br>
> > > >                  isMagma : IsMagma setoid _∙_<br>
> > > >         ------------------------------------------------------------------------<br>
> > > >         <br>
> > > >         And let us call  Version I  the approach of Standard library<br>
> > > >         lib-0.17.<br>
> > > >         <br>
> > > >         Both versions use an `Is' structure, but II does not<br>
> > > >         re-declare fields.<br>
> > > >         Is not II more natural?<br>
> > > >         <br>
> > > >         <br>
> > > >         Another question may be:<br>
> > > >         ``why splitting each GAS into proper structure and `Is'<br>
> > > >         structure?''.<br>
> > > >         <br>
> > > >         My guess is that this approach allows us to express two GAS-s<br>
> > > >         that are<br>
> > > >         over the same inherited GAS. For example, a programmer can<br>
> > > >         express a<br>
> > > >         product of two Magmae over the same Setoid:<br>
> > > >         ------------------------------------------------------------<br>
> > > >         module _ {α α=} (S : Setoid α α=)<br>
> > > >           where<br>
> > > >           open Setoid S using (Carrier; _≈_)<br>
> > > >           SS = ×-setoid S S<br>
> > > >           open Setoid SS using () renaming (Carrier to CC; _≈_ to<br>
> > > >         _=p_)<br>
> > > >         <br>
> > > >           magmaProduct' :<br>
> > > >             (_*₁_ _*₂_ : Op₂ Carrier) → IsMagma _≈_ _*₁_ →<br>
> > > >                                         IsMagma _≈_ _*₂_ → Magma α α=<br>
> > > >           magmaProduct' _*₁_ _*₂_ insM₁ isM₂ =<br>
> > > >                                <define coordinate-wise multiplcation<br>
> > > >         on CC;<br>
> > > >                                 prove ...;  return the Magma record<br>
> > > >                                ><br>
> > > >         ------------------------------------------------------------<br>
> > > >         <br>
> > > >         (is there any other purpose to introduce `Is' -structures?).<br>
> > > >         <br>
> > > >         This is equally easy to set both in Version I and Version II.<br>
> > > >         <br>
> > > >         But note that both approaches still deviate, a bit, from the<br>
> > > >         theory.<br>
> > > >         Because in theory, it is <br>
> > > >         \ (mg1 : Magma_ _) (mg2 : Magma _ _) (HaveCommonSetoid mg1<br>
> > > >         mg2) →<br>
> > > >         product-magma,<br>
> > > >         while magmaProduct' takes certain parts of the two magmae.<br>
> > > >         <br>
> > > >         So, there remain somewhat three and a half questions.<br>
> > > >         <br>
> > > >         Thank you in advance for your possible explanation.<br>
> > > >         <br>
> > > >         ------<br>
> > > >         Sergei<br>
> > > >         <br>
> > > >         <br>
> > > >         <br>
> > > >         <br>
> > > >         _______________________________________________<br>
> > > >         Agda mailing list<br>
> > > >         <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> > > >         <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> > > <br>
> > > <br>
> > > _______________________________________________<br>
> > > Agda mailing list<br>
> > > <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> > > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> > <br>
> > <br>
> > <br>
> <br>
> <br>
> <br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>