[Agda] BFLib for standard

[Matthew Daggitt]

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?

 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?


"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.

There are much more questions to ask. But I try to follow the rule
> "a small item at a time".
>

Thank you I appreciate it.
Matthew

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190330/272424e1/attachment.html>