<div dir="ltr">The rationals are not very well-developed in agda-prelude. Nevertheless I get unsurprising performance compared to ghc (~2min for n = 20,000 on my machine) with the following benchmark:<div><br></div><div><div>module Harmonic where</div><div><br></div><div>open import Prelude</div><div>open import Numeric.Rational</div><div><br></div><div>-- sum [ 1/k | k <- [1..n] ]</div><div>harmonic : Nat → Rational</div><div>harmonic 0 = 0</div><div>harmonic (suc n) = sum (map (λ k → ratio 1 (suc k) refl) (from 0 to n))</div><div><br></div><div>test : Nat → Rational</div><div>test n = harmonic n * 0</div><div><br></div><div>main : IO ⊤</div><div>main =</div><div>  caseM getArgs of λ where</div><div>    (s ∷ []) → print (test <$> parseNat s)</div><div>    _ → pure _</div></div><div><br></div><div>The reason that DoCon performs so well is that it has a more clever implementation of _+_. agda-prelude and GHC implements _+_ as</div><div><br></div><div>  (p :% q) + (p1 :% q1) = (p * q1 + p1 * q) % (q * q1)</div><div>    where a % b = let d = gcd a b in div a d :% div d b</div><div><br></div><div>DoCon implements _+_ as</div><div><br></div><div>  (p :% q) + (p1 :% q1) = div n dd :% (q' * q1' * div d dd)</div><div>    where</div><div>      d = gcd q q1</div><div>      q' = div q d</div><div>      q1' = div q1 d</div><div>      n = p * q1' + p1 * q'</div><div>      dd = gcd n d</div><div><br></div><div>I can't claim to understand why this is so much faster, but it is.</div><div><br></div><div>/ Ulf</div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Jun 24, 2017 at 9:06 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:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear all,<br>
<br>
Consider the following performance test for rational arithmetic.<br>
Call this test call "Harmonic":<br>
<br>
  f n =  sum [1/k | k <- [1 .. n]]   for n : Nat, 1/k : Rational,<br>
<br>
  sum = foldr _+_ 0    where _+_ = fraction addition<br>
<br>
  test n =  let fn = f n<br>
            in  fn - fn<br>
<br>
  Read from file   n = 100, 1000, 2000, 100.000 ...,<br>
<br>
  print  (test n)  and check time.<br>
<br>
(fn - fn)  is applied here in order to avoid printing large values.<br>
<br>
<br>
  --------------------------- Haskell code -------<br>
  import Data.Ratio ((%))<br>
<br>
  f :: Integer -> Rational     -- :: Ratio Integer<br>
  f n =<br>
      sum [1 % k | k <- [1 .. n]]<br>
  ------------------------------<wbr>-------------------<br>
<br>
<br>
I compare the three libraries:<br>
<br>
  (GHC) GHC  (Glasgow Haskell 7.10.2),<br>
<br>
  (D)   DoCon-2.12  written in Haskell, running under GHC,<br>
<br>
  (DA)  DoCon-A 2.00-pre   written in Agda,<br>
                           running under Agda 2.5.2 -like.<br>
<br>
(D) and (DA) keep fractions with numerator and denominator mutually<br>
coprime, and cancel fractions most eagerly by gcd.<br>
<br>
(GHC)  does not cancel by gcd so eagerly.<br>
<br>
The performance comparison on Harmonic is:<br>
<br>
                (D) >> (GHC) > (DA).<br>
<br>
(D) takes  n = 200.000  easily, while GHC "hangs" on 20.000<br>
    -- for a 3 GHz machine.<br>
<br>
(GHC) is considerably faster (DA)<br>
      (DA hangs for long on 4000).<br>
<br>
The method in (DA) is the same as (D).<br>
gcd is almost as fast as GHC.gcd, this has been tested.<br>
Division (with remainder) is via  dimMod  of Agda-prelude, it is fast.<br>
<br>
And I wonder why (DA) is so slow.<br>
(DA) carries all the needed proofs (for coprimality, and such).<br>
But I hope, this does not effect performance any essentially.<br>
<br>
Can anybody provide the code for testing Harmonic for  Rational numbers<br>
in  agda-prelude ?<br>
<br>
The (DA) test for (Fraction Integer) is like this:<br>
<br>
------------------------------<wbr>------------------------------<wbr>------------<br>
...<br>
open Fraction.F0 Int1.integralRing-with∣? Int1.gcdRing using<br>
                                 (Fraction; fraction; fraction-showInst)<br>
open Fraction.F1 Int1.integralRing-with∣? Int1.gcdRing using (frRingoid)<br>
open Ringoid frRingoid using (_-_)<br>
open Fraction<br>
<br>
inv-n :  ℕ → Fraction              -- \n → 1/(1+n)<br>
inv-n n =<br>
        fraction (+ 1) (+ (suc n)) +suc≢+0<br>
<br>
f : ℕ → Fraction    -- sum [1/n | n <- [1 .. n+1]]<br>
f n =<br>
    sum frRingoid (map inv-n (natSegment 0 n))<br>
<br>
main : IO Unit<br>
main = (readFiniteFile "data.txt") >>= putStrLn ∘ toCostring ∘ g<br>
  where<br>
  g : String -> String<br>
  g str =<br>
    -- n  is first read from file  data.txt<br>
<br>
    concatStr<br>
    ("n = "                 ∷  showNat n                 ∷ ",   " ∷<br>
     "num (f n - f n) =  "  ∷  showInt (num (fn - fn))   ∷ "\n\n"<br>
     ∷ []<br>
    )<br>
    where<br>
    n  = stringToNat $ filterStr decimalDigit? str<br>
    fn = f n<br>
------------------------------<wbr>------------------------------<wbr>-------------<br>
<br>
<br>
So far, I do not find the performance bottleneck in (DA).<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>