<div dir="ltr"><div><span class="gmail-im" style="color:rgb(80,0,80)"><br></span><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Concerning Data.Digit.toDigits and Data.Nat.Show.show of standard: the latter function is implemented via the former one, and both are `exponentially' slow.</blockquote></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I suggest to change the implementation for toDigits by using _%_ and _div_. This will make Digit.toDigits, Nat.Show.show and Integer.Show.show<br>exponentially faster than the existing ones. The code is ready.<br></blockquote><div><br></div><div>Okay sounds good. Feel free to open a PR with the changes. </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">No, this part is not about the division _function_. This is about the definition of the divisibility relation _∣_.<br></blockquote><div><br></div><div>Thank you for explaining, I got confused, but I understand now. Yes a generic notion of divisibility would be a useful addition to the library.</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">And the notion of divisibility is via RightQuotient: <br></blockquote><div><br></div><div>The RightQuotient notion looks useful. I believe the right place for it would be in `Algebra.FunctionProperties` (where it doesn't need to parameterised by a setoid, but simply the equality relation instead). </div><div><br></div><div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On the other hand, as the approach to divisibility is so greatly<br>generalized, may be, we can ignore the backwards compatibility at this<br>point?</blockquote><div> </div></div><div>Whether or not to replace the existing divisibility relation with the new one can be decided at a later date.</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">I doubt about the word `Properties'. For example, consider the relation<br>_|_ under Magma, and the function _^_ for powering an element in an<br>arbitrary Monoid. Can they be called `properties' of Magma or a Monoid ?<br></blockquote><div><br></div><div>So we also have `Algebra.Operations.CommutativeMonoid` which has operation like `_^_`. Conceivably we could add a `Algebra.Relations` as well. The discussion for how this stage of the changes should be laid out should really be continued in an issue on Github. If you'd like to open an issue there?</div><div>Best,<br></div><div>Matthew <br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Mar 31, 2019 at 3:13 AM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">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-30 at 22:40 +0800, Matthew Daggitt wrote:<br>
> Hi Sergei,<br>
> I'll try and answer all your questions. Apologies if I miss one.<br>
> <br>
> <br>
> Can you, please, advise about possible way to propose?<br>
> (probably, by pull resquests).<br>
> <br>
> Matthew wrote about pulling-request somewhat "a single item at<br>
> a time".<br>
> <br>
> <br>
> Yes, a single pull request (PR) per change is the right way to go. <br>
> <br>
> <br>
> >`compare' and `show' for Nat<br>
> > ============================<br>
> ><br>
> > Nat.<-cmp as compareFast (via _≟_, _∸_),<br>
<br>
> Yup feel free to open a PR with this.<br>
<br>
<br>
>> toDecimalChars : ℕ → List Char (via _%_, _div_),<br>
<br>
> A function very much like this already exists in `Data.Digit`. Have<br>
> you seen it?<br>
<br>
>> show : ℕ → String<br>
<br>
> Again this already exists in `Data.Nat.Show`. I take it the current<br>
> implementation isn't fast enough?<br>
<br>
<br>
Concerning Data.Digit.toDigits and Data.Nat.Show.show of standard:<br>
the latter function is implemented via the former one,<br>
and both are `exponentially' slow.<br>
This is demonstrated in my recent letter, somewhat a week ago, to which<br>
the test code is attached.<br>
Can you, please, run it and see that Data.Nat.Show is exponentially<br>
slow?<br>
(and hence Data.Digit.toDigits is as slow).<br>
Or may be, their implementation has changed last 2-3 weeks?<br>
<br>
I suggest to change the implementation for toDigits by using _%_ and<br>
_div_.<br>
This will make Digit.toDigits, Nat.Show.show and Integer.Show.show<br>
exponentially faster than the existing ones. The code is ready.<br>
<br>
><br>
>> The division relation<br>
>> =====================<br>
<br>
>><br>
>> Now, the property proofs in Nat.Divisibilty can be replaced with <br>
>> the instances of the generic proofs. For example,<br>
>> x ∣ y → x ∣ z → x ∣ (y + z) is proved in Semiring-pack.<br>
>><br>
>> But what to do with the divisibility definition in <br>
>> Nat.Divisibility ?<br>
<br>
> I'm a bit confused about this. As I understand it, performance is<br>
> quite important for you? Replacing the existing implementation of<br>
> division for Nat (that uses built-ins) with a generic implementation<br>
> is going to result in much worse performance. Is this really what<br>
> you're after? <br>
> <br>
<br>
No,this part is not about the division _function_. This is about the<br>
definition of the divisibility relation _∣_.<br>
There is nothing to evaluate, no performance matters here.<br>
This about defining the relation _∣_ for a generic case.<br>
Then, by using the instance of *-magma for ℕ, one obtains the instance<br>
of _∣_ for ℕ, by using the instance of *-magma for ℤ, one obtains the<br>
instance of _∣_ for ℤ, by using the instance of *-magma for Bin, one<br>
obtains the instance of _∣_ for Bin, and so on.<br>
And in standard, there are only special definitions of _∣_: for ℕ and<br>
for ℤ.<br>
The question is about how to introduce a generic notion of _∣_ with<br>
preserving backwards compatibility.<br>
Please, read once more the corresponding place in my original letter<br>
below (to which you are responding). This is the section <br>
"The division relation" -- which is better to title <br>
"The divisibility relation".<br>
<br>
<br>
> > "Packages"<br>
> > ==========<br>
<br>
> > In each `pack' there are gathered most useful functions and lemmata<br>
> > (`items', theory) relating to a particular generic _standard_ <br>
> > structure:<br>
> > Magma, Semigroup, Group, Ring and so on.<br>
<br>
<br>
> Such "packages" as you call them already exist in the standard library<br>
> as "Properties" file. For instance all lemmata and functions for<br>
> "Ring" live in "Algebra.Properties.Ring". Any extra lemmas and<br>
> functions should be added there. Such files don't exist for all<br>
> structures (e.g. magmas) but they can be added.<br>
<br>
<br>
I doubt about the word `Properties'. For example, consider the relation<br>
_|_ under Magma, and the function _^_ for powering an element in an<br>
arbitrary Monoid. Can they be called `properties' of Magma or a Monoid ?<br>
<br>
But if you are against "packages", all right, let them be<br>
Algebra.Properties.Magma, Algebra.Properties.Semigroup, and so on.<br>
Only they need to be presented as the modules parametrized respectively<br>
by (magma : Magma), (semigroup : Semigroup), and so on.<br>
I look now into Algebra.Properties.CommutativeMonoid, and see that this<br>
module is declared this way. <br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
> On Sat, Mar 30, 2019 at 9:39 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>><br>
> wrote:<br>
> <br>
> Dear standard library developers,<br>
> <br>
> I have a certain BFLib library for Agda: <br>
> a regular-performance, complete, and certified<br>
> * binary arithmetic for integer numbers,<br>
> * and the arithmetic of fractions in the general case of<br>
> fractions over arbitrary GCDRing.<br>
> <br>
> It has been tested under Agda 2.6.0-candidate, MAlonzo,<br>
> ghc-8.6.3.<br>
> I want to propose it as a replacement for the Bin part and<br>
> Rational<br>
> part in Standard library lib-0.18.<br>
> <br>
> First, I am going to put BFLib-0.01 to public as an<br>
> application<br>
> library, after it appears an official Agda 2.6.0.<br>
> <br>
> But then, I am going to propose its parts to standard, with<br>
> modifying<br>
> them, when necessary.<br>
> <br>
> BFLib suggests the three improvements.<br>
> (I) Essentially faster implementation for `compare', show, gcd<br>
> for Nat,<br>
> for arithmetic of rational numbers.<br>
> (II) Totally new Bin part (similar to binary-4 visible on<br>
> GitHub).<br>
> (III) Generic Fraction domain constructor to replace the<br>
> Rational part.<br>
> In particular, its instance works also for rational<br>
> number <br>
> arithmetic in binary representation. <br>
> <br>
> <br>
> Can you, please, advise about possible way to propose?<br>
> (probably, by pull resquests).<br>
> <br>
> Matthew wrote about pulling-request somewhat "a single item at<br>
> a time".<br>
> <br>
> <br>
> I try the following plan, and have questions related to most<br>
> its parts.<br>
> <br>
> <br>
> `compare' and `show' for Nat<br>
> ============================<br>
> <br>
> Pull-request<br>
> Nat.<-cmp as compareFast (via _≟_, _∸_),<br>
> <br>
> toDecimalChars : ℕ → List Char (via _%_, _div_),<br>
> <br>
> show : ℕ → String<br>
> show = String.fromList ∘ toDecimalChars -- fast `show` for<br>
> ℕ, for ℤ.<br>
> <br>
> These three look easy to make the implementation replacement,<br>
> it is<br>
> backwards compatible.<br>
> <br>
> <br>
> The division relation<br>
> =====================<br>
> <br>
> This is a large thing.<br>
> In standard, it is only for ℕ and ℤ (the latter is by <br>
> "on absoluteValue"):<br>
> <br>
> record _∣_ (m n : ℕ) : Set where<br>
> constructor divides<br>
> field quotient : ℕ<br>
> equality : n ≡ quotient * m<br>
> open _∣_ using (quotient) public<br>
> <br>
> <br>
> I think, standard library needs generic Fraction over a<br>
> GCDRing,<br>
> this needs a generic GCD notions. And this needs, in its turn,<br>
> a generic<br>
> divisibility notion. I particular, it will serve also for ℤ,<br>
> for pairs,<br>
> for polynomials, and so on.<br>
> <br>
> If the library administrators do not want to consider such a<br>
> proposal,<br>
> then I would skip its pull request, in order to save effort.<br>
> In this case there will remain only the Bin part to try (with<br>
> special<br>
> divisibility and gcd for Bin), and Fraction will be removed.<br>
> <br>
> BFLib defines the divisibility for Magma.<br>
> First, the notion of a quotient is related to any _≈_; _∙_ :<br>
> <br>
> module _ {α α=} (A : Setoid α α=) (_∙_ : Op₂ (Setoid.Carrier<br>
> A))<br>
> where<br>
> open Setoid A using (_≈_) renaming (Carrier to C)<br>
> <br>
> RightQuotient : C → C → Set (α ⊔ α=)<br>
> RightQuotient a b = ∃ (\q → (b ∙ q) ≈ a)<br>
> <br>
> And the notion of divisibility is via RightQuotient: <br>
> <br>
> -------------------------------------------------------<br>
> module Magma-pack {α α=} (M : Magma α α=) <br>
> where<br>
> open Magma M using (_≈_; _∙_; ∙-cong; ∙-congˡ; setoid)<br>
> renaming (Carrier to<br>
> C)<br>
> module FP≈ = FuncProp _≈_<br>
> <br>
> open Setoid-pack setoid public<br>
> <br>
> _∣_ _∤_ : Rel C (α ⊔ α=)<br>
> x ∣ y = RightQuotient setoid _∙_ y x -- `x divides y' <br>
> <br>
> _∤_ x = ¬_ ∘ _∣_ x<br>
> <br>
> open EqR setoid<br>
> <br>
> ∣cong : _∣_ Respects2 _≈_<br>
> ∣cond = ...<br>
> <br>
> ...<br>
> --------------------------------------------------------<br>
> <br>
> Various properties of _∣_ are derived for Magma, Semigroup,<br>
> (Commutative)Monoid, Semiring, Ring, DecCommutativeRing<br>
> (there is also introduced _∣?_ for some structures).<br>
> <br>
> The properties of _∣_ for ℕ are expressed as the instances of<br>
> the above<br>
> generic properties for *-monoid, *-+-semiring in<br>
> Nat.Properties.<br>
> Similarly this is done for the instances for ℤ.<br>
> <br>
> Now, the property proofs in Nat.Divisibilty can be replaced<br>
> with the<br>
> instances of the generic proofs. For example, <br>
> x ∣ y → x ∣ z → x ∣ (y + z) is proved in Semiring-pack.<br>
> <br>
> But what to do with the divisibility definition in<br>
> Nat.Divisibility ?<br>
> <br>
> I can try to generalize the standard<br>
> record _∣_ (m n : ℕ) : Set where<br>
> constructor divides<br>
> field quotient : ℕ<br>
> equality : n ≡ quotient * m<br>
> <br>
> for Magma, and then to try to agree the things so that old<br>
> applications<br>
> like<br>
> <br>
> open Data.Nat.Divisibilty <br>
> open _∣_<br>
> ...<br>
> <br>
> will remain workable but will be done as an instance of the<br>
> generic _∣_<br>
> (if this is ever possible).<br>
> <br>
> On the other hand, as the approach to divisibility is so<br>
> greatly<br>
> generalized, may be, we can ignore the backwards compatibility<br>
> at this<br>
> point?<br>
> <br>
> Another question: does the definition<br>
> <br>
> RightQuotient a b = ∃ (\q → (b ∙ q) ≈ a)<br>
> <br>
> x ∣ y = RightQuotient setoid _∙_ y x <br>
> <br>
> look simpler and nicer? Really do we need a record here?<br>
> <br>
> <br>
> "Packages"<br>
> ==========<br>
> <br>
> The above implementation introduces several modules of this<br>
> kind:<br>
> <br>
> module Magma-pack {α α=} (M : Magma α α=),<br>
> module Semigroup-pack {α α=} (H : Semigroup α α=),<br>
> ...<br>
> module Ring-pack {α α=} (R : Ring α α=)<br>
> <br>
> In each `pack' there are gathered most useful functions and<br>
> lemmata<br>
> (`items', theory) relating to a particular generic _standard_<br>
> structure:<br>
> Magma, Semigroup, Group, Ring and so on.<br>
> For example, divisibility in CommutativeRing has more proved<br>
> properties <br>
> than in Semigroup, many useful things can be proved for<br>
> DecIntegralRing<br>
> that are not possible for Semiring. And we cannot include<br>
> these items to<br>
> the records of the classical structures, because these records<br>
> are<br>
> intended to be classical definitions, and not a related theory<br>
> containers.<br>
> <br>
> The minimality is provided: there are included only those<br>
> items that are<br>
> used in this proposal for standard.<br>
> <br>
> Can we, say, put Packages.agda to the Algebra/ folder and<br>
> to put<br>
> there the above 'pack' parametrized modules?<br>
> Can a pull request introduce a new .agda file?<br>
> <br>
> There are much more questions to ask. But I try to follow the<br>
> rule<br>
> "a small item at a time".<br>
> <br>
> Regards,<br>
> <br>
> ------<br>
> Sergei<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>
</blockquote></div>