[Agda] practical integer/rational arithmetic?

[Noam Zeilberger]

On Wed, May 9, 2012 at 5:19 PM, Daniel Peebles <pumpkingod at gmail.com> wrote:
> I haven't considered using the FFI, but using James Deikun's new Fast
> natural arithmetic (including a new fast GCD implementation) we can actually
> get reasonable performance out my code, even during compile-time
> normalization. James can probably give you more details on that.

Thank you for the link (and thank you James!).  Just by plugging this
in for gcd I was able to get a slightly larger program I was
interested in to terminate in a few seconds, whereas before it was
taking unknown (>10 minutes) time.  Whether this will be efficient
enough for larger examples remains to be seen, but it keeps me going
for now.

(I still think it would be great if there were a way to use the FFI in
interactive mode and thus take advantage of Haskell's fast
implementation of arithmetic.)

> I've mostly focussed on non-negative rationals so far, so most of the
> reasonable code is
> in https://github.com/copumpkin/rational/blob/master/Rational/Nonnegative.agda

Thank you.  I haven't tried to prove anything yet about the rationals
(only compute with them), but when I do this could be helpful.

Noam