[Agda] Nat arithmetic properties

[Sergei Meshveliani]

Another reason for necessity of n-ary provable arithmetic:

  _≤?_  of Data.Nat.decTotalOrder  is slow.

Probably this is because it is not built-in
(and how can it? assuming that the result may contain a proof made of
many certain constructors).

This leads, for example, to that sorting of the list  [10000 ... 1]  is
done many times faster when the numbers are binary-coded
(and it is applied _≤?_ of DecTotalOrder for Bin).

------
Sergei



On Thu, 2016-09-22 at 22:30 +0400, Sergei Meshveliani wrote:
> On Thu, 2016-09-22 at 12:38 -0400, Wolfram Kahl wrote:
> > Sergei,
> > 
> > On Wed, Sep 21, 2016 at 02:34:28PM +0200, Ulf Norell wrote:
> > > How is this better than what we do at the moment? It seems to me that
> > > your postulated properties of the macro digit operations are going to be
> > > more
> > > complicated than what we postulate right now (namely that Haskell Integer
> > > arithmetic implement the expected functions on natural numbers).
> > 
> > Indeed.
> > 
> > One possibly interesting avenue to expore in this direction,
> > and requiring no modification of Agda, would be starting from the fact
> > that GHC supports two implementations of Haskell Integer:
> > 
> >  * The default implementation calls the GPL-licenced GMP library via the FFI
> > 
> >  * An alternative implementation (called SimpleInteger?)
> >    for GPL-averse contexts is, if I remember correctly, implemented in Haskell.
> >    (So that would be some kind of lists of Macrodigits already.)
> > 
> > You could go and implement your lists of Macrodigits in Agda, and
> > use Agda's reverse FFI to export this to Haskell to replace SimpleInteger.
> > 
> > And try to be faster! ;-)
> 
> 
> 1) In principle:  Agda Standard library needs a proved arithmetic for
> Nat which is several times faster that the existing one of Data.Bin. 
> 
> 2) For example, Bin._+_ is  2^n times  faster than Nat._+_ (unary), 
> and can be supplied with all the necessary proofs
> (mainly: a proof for that the ring of Nat is isomorphic to the ring of
> Bin, this is enough).
> 
> 3) Further, _+_ for the  Hexa -coded naturals is can be programmed in
> Agda, so that it will be several times faster than Bin._+_, and will be
> supplied with the proof for that the ring of Nat is isomorphic to the
> ring of Hexa).
> And this does not need any built-ins (no postulates) for digits.
> But it will be about 8 times slower than Integer._+_ in GHC
> (because 4-Hexa-digit numbers are summed by one macrodigit operation in
> GHC, and because a digit operation in Hexa in Agda is not in one step).
> 
> 4) As to doing the same for lists of large macrodigits (say 64 bit
> digit), there it will have sense to make the digit operations built-in
> (with several postulated properties) an all the rest written in Agda,
> with proofs.
> 
> 
> But  I am not currently going to implement any of these things.
> These are only my notes, comments.
> 
> []