<div dir="ltr">Hi Sergei,<div> I'll try and answer all your questions. Apologies if I miss one.</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">Can you, please, advise about possible way to propose? (probably, by pull resquests).<br><br>Matthew wrote about pulling-request somewhat "a single item at a time".<br></blockquote><div><br></div><div>Yes, a single pull request (PR) per change is the right way to go. </div><div><br></div><div>`compare' and `show' for Nat<br>============================<br></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">Nat.<-cmp as compareFast (via _≟_, _∸_),<br></blockquote><div><br></div><div>Yup feel free to open a PR with this.</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">toDecimalChars : ℕ → List Char (via _%_, _div_),<br></blockquote><div> </div><div>A function very much like this already exists in `Data.Digit`. Have you seen 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">show : ℕ → String<br></blockquote><div><br></div><div>Again this already exists in `Data.Nat.Show`. I take it the current implementation isn't fast enough?</div><div><br></div><div> The division relation</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">Now, the property proofs in Nat.Divisibilty can be replaced 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 Nat.Divisibility ?<br></blockquote><div><br></div><div>I'm a bit confused about this. As I understand it, performance is quite important for you? Replacing the existing implementation of division for Nat (that uses built-ins) with a generic implementation is going to result in much worse performance. Is this really what you're after? </div><div><br></div><div><br>"Packages"<br>==========<br></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">In each `pack' there are gathered most useful functions and lemmata<br>(`items', theory) relating to a particular generic _standard_ structure:<br>Magma, Semigroup, Group, Ring and so on.<br></blockquote><div><br></div><div>Such "packages" as you call them already exist in the standard library as "Properties" file. For instance all lemmata and functions for "Ring" live in "Algebra.Properties.Ring". Any extra lemmas and functions should be added there. Such files don't exist for all structures (e.g. magmas) but they can be added.</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">There are much more questions to ask. But I try to follow the rule<br>"a small item at a time".<br></blockquote><div><br></div><div>Thank you I appreciate it.</div><div>Matthew </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Mar 30, 2019 at 9:39 PM 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">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, ghc-8.6.3.<br>
I want to propose it as a replacement for the Bin part and Rational<br>
part in Standard library lib-0.18.<br>
<br>
First, I am going to put BFLib-0.01 to public as an 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 modifying<br>
them, when necessary.<br>
<br>
BFLib suggests the three improvements.<br>
(I) Essentially faster implementation for `compare', show, gcd for Nat,<br>
for arithmetic of rational numbers.<br>
(II) Totally new Bin part (similar to binary-4 visible on GitHub).<br>
(III) Generic Fraction domain constructor to replace the Rational part.<br>
In particular, its instance works also for rational 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 a time".<br>
<br>
<br>
I try the following plan, and have questions related to most 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 ℕ, for ℤ.<br>
<br>
These three look easy to make the implementation replacement, 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 GCDRing,<br>
this needs a generic GCD notions. And this needs, in its turn, a generic<br>
divisibility notion. I particular, it will serve also for ℤ, for pairs,<br>
for polynomials, and so on.<br>
<br>
If the library administrators do not want to consider such a 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 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 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 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 the above<br>
generic properties for *-monoid, *-+-semiring in Nat.Properties.<br>
Similarly this is done for the instances for ℤ.<br>
<br>
Now, the property proofs in Nat.Divisibilty can be replaced 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 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 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 generic _∣_<br>
(if this is ever possible).<br>
<br>
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?<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 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 lemmata<br>
(`items', theory) relating to a particular generic _standard_ structure:<br>
Magma, Semigroup, Group, Ring and so on.<br>
For example, divisibility in CommutativeRing has more proved properties <br>
than in Semigroup, many useful things can be proved for DecIntegralRing<br>
that are not possible for Semiring. And we cannot include these items to<br>
the records of the classical structures, because these records 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 items that are<br>
used in this proposal for standard.<br>
<br>
Can we, say, put Packages.agda to the Algebra/ folder and 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 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>
</blockquote></div>