<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jun 21, 2017 at 10:20 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear all,<br>
<br>
Earlier there was discussed in this list the performance of _+_ and _*_<br>
on Nat. I provided a test program.<br>
And as I recall, the performance is high: as in the Haskell program for<br>
ghc-7.10.2.<br>
<br>
Now I need fast  divMod and gcd  for Nat.<br>
Standard library is very-very slow at this point.<br>
<br>
So I try  agda-prelude.<br>
It shows considerably faster.<br>
But it is still slower than  GHC.<br>
gcd  is about  12 times  slower,<br>
and  divMod  is about 4000 times slower (?).<br></blockquote><div><br></div><div>divMod isn't slow, the problem is that you are using ≤? from the standard library in</div><div>your implementation of max. If you replace it by ≤? from agda-prelude the Agda code<br></div><div>is 40% slower than the Haskell code. None of that slowdown is due to divMod, which</div><div>if you look at the Haskell code generated by the Agda compiler, is actually compiled</div><div>to calls to Integer rem and quot.</div><div><br></div><div>The gcd benchmark is around 5 times slower on my machine. I suspect this is because</div><div>Haskell gcd is heavily optimised, and the Agda implementation pays for carrying around</div><div>the correctness proofs (which does contain computational content for gcd, and so are</div><div>not being erased).</div><div><br></div><div>/ Ulf</div><div><br></div></div></div></div>