[Agda] Data.Rational

[Sergei Meshveliani]

On Wed, 2014-03-12 at 20:45 +0400, Sergei Meshveliani wrote:
> 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.
> [..]

The letter https://lists.chalmers.se/pipermail/agda/2012/003988.html
of (may, 2012)

writes of        GCD of 14303480934 and 44934319042,

But for unary system, most of the cost in this example will, probably,
eaten by conversion  Decimal <--> Unary. 

There is another point:

> Euclid's algorithm was taking an absurdly long time to run, apparently
> because of Agda's call-by-name evaluation strategy

But does this  call-by-name evaluation  relate to run-time?
May be, it is applied only at the type-check stage?

Also the Agda implementation has, probably, changed during last 2 years.

Can the developers comment, please?

Regards,

------
Sergei