[Agda] Data.Rational

[Sergei Meshveliani]

On Wed, 2014-03-12 at 14:20 +0100, Noam Zeilberger wrote:
> For what it's worth (which granted is not much given my limited
> experience), the performance issues I ran into really had more to do
> with Agda in general than with a specific strategy for rationals
> (hence my eventual approach of giving up and calling the FFI).  In
> particular, Euclid's algorithm was taking an absurdly long time to
> run, apparently because of Agda's call-by-name evaluation strategy
> (see https://lists.chalmers.se/pipermail/agda/2012/003988.html, as
> well as https://code.google.com/p/agda/issues/detail?id=426).
>

As far as  Nat  is represented in _unary system_, it is senseless to
consider efficiency of operations on large Nat or Integer values.

I have tried arithmetic in  Integer/(m)  ("modulo m")  in Agda  for  
m < 20.
The example applies about 100.000 times (partial) division in
Integer/(m).  Each such division applies the  extended GCD algorithm
extGCD  (extended Euclidean method).
I program  extGCD  for Integer (in Agda) by new. 

And all this loop is fast, somewhat comparable with an Haskell program
under GHC.

If  m  is bound by  9000 instead of 20,  then this will be different,
the unary system will not do, probably.

May be, when I go further with another examples, this call by name could
bite me. It is interesting to see.
The matter is that providing proofs takes a great effort, so that the
advance in programming methods is slow.

Regards,

------
Sergei