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