[Agda] practical integer/rational arithmetic?

[wren ng thornton]

On 5/9/12 11:55 AM, Nils Anders Danielsson wrote:
> On 2012-05-09 17:28, Jacques Carette wrote:
>> I can't help you with how to make Agda faster, but I can at least show
>> you what the bar ought to be. In Maple, on a 3 year old machine,
>> computing gcd(3!!!^5, 2^26892+1) [which is 1446241] takes 0.015
>> seconds.
>
> In GHCi, on an older machine:
>
> Prelude> let fac n = product [1..n] in gcd (fac (fac (fac 3)) ^ 5)
> (2^26892 + 1)
> 1774001
> (0.10 secs, 39859272 bytes)

FWIW, with numbers this large it's worth using a sophisticated 
implementation of factorial. Using the one in exact-combinatorics[1] I 
get less than half that time in ghci:

     Prelude> :m +Math.Combinatorics.Exact.Factorial
     Prelude Math.Combinatorics.Exact.Factorial>
         gcd (factorial (factorial (factorial 3))^5) (2^26892 + 1)
     Loading package exact-combinatorics-0.2.0 ... linking ... done.
     1774001
     (0.04 secs, 41337232 bytes)

GHC  = 6.12.1 (32-bit because of OSX)
OS   = OSX 10.5.8
ARCH = 2.8 GHz Intel Core 2 Duo


[1] http://hackage.haskell.org/package/exact-combinatorics

-- 
Live well,
~wren