[Agda] Nat arithmetic properties

[Sergei Meshveliani]

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.

My current state is that I am stuck with the memory expense of the type
checking. 
DoCon-A-0.04  can be released as it is. It fits into 14 Gb, and I hope,
it will fit even in 7 Gb.

But I am stuck with continuing it, with adding more notions/methods on
the top of existing hierarchy. Parametric modules import each other, and
the memory explodes after a certain level in reached
(so that 26 Gb is not enough).

Probably something needs to be seriously optimized in Agda
implementation.
I need to decide/investigate of what to do with this all.
But I greatly doubt in that I could understand the implementation
principles, so that to fix there anything. 

Regards,

------
Sergei