[Agda] Nat arithmetic properties

[Wolfram Kahl]

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! ;-)


Cheers,

Wolfram