[Agda] timing for agda-prelude gcd

[Ulf Norell]

On Wed, Jun 21, 2017 at 10:20 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> Dear all,
>
> Earlier there was discussed in this list the performance of _+_ and _*_
> on Nat. I provided a test program.
> And as I recall, the performance is high: as in the Haskell program for
> ghc-7.10.2.
>
> Now I need fast  divMod and gcd  for Nat.
> Standard library is very-very slow at this point.
>
> So I try  agda-prelude.
> It shows considerably faster.
> But it is still slower than  GHC.
> gcd  is about  12 times  slower,
> and  divMod  is about 4000 times slower (?).
>

divMod isn't slow, the problem is that you are using ≤? from the standard
library in
your implementation of max. If you replace it by ≤? from agda-prelude the
Agda code
is 40% slower than the Haskell code. None of that slowdown is due to
divMod, which
if you look at the Haskell code generated by the Agda compiler, is actually
compiled
to calls to Integer rem and quot.

The gcd benchmark is around 5 times slower on my machine. I suspect this is
because
Haskell gcd is heavily optimised, and the Agda implementation pays for
carrying around
the correctness proofs (which does contain computational content for gcd,
and so are
not being erased).

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170622/20c774a4/attachment.html>