[Agda] practical integer/rational arithmetic?

[James Deikun]

On Wed, 2012-05-09 at 11:37 -0400, Daniel Peebles wrote:
> Granted, Maple doesn't need to compute a witness of GCD-ness along the
> way :)
> 
> 
> I think James's new witness-carrying GCD takes about 5 seconds to
> normalize the GCD of 14303480934 and 44934319042, which seems pretty
> respectable. If you want to see the code, it's
> at https://github.com/xplat/potpourri/tree/master/Fast

A computation like that should really be more like the aforementioned
0.015 seconds than 5 seconds, but I haven't been able to prevent
call-by-name evaluation from making the extended Euclid's algorithm
exponential in its recursion depth.  (At least it's no longer
exponential in anything else.)  Rather than continue trying to
micromanage evaluation for these particular functions, I decided to
focus my efforts on improving Agda's evaluation strategy in general, so
that's probably the next improvement that will appear.