[Agda] summing rationals

[Sergei Meshveliani]

Dear all,

Consider the following performance test for rational arithmetic.
Call this test call "Harmonic":

  f n =  sum [1/k | k <- [1 .. n]]   for n : Nat, 1/k : Rational,
                                     
  sum = foldr _+_ 0    where _+_ = fraction addition

  test n =  let fn = f n
            in  fn - fn

  Read from file   n = 100, 1000, 2000, 100.000 ...,

  print  (test n)  and check time. 

(fn - fn)  is applied here in order to avoid printing large values.


  --------------------------- Haskell code -------
  import Data.Ratio ((%))

  f :: Integer -> Rational     -- :: Ratio Integer
  f n =
      sum [1 % k | k <- [1 .. n]]
  -------------------------------------------------


I compare the three libraries:

  (GHC) GHC  (Glasgow Haskell 7.10.2),

  (D)   DoCon-2.12  written in Haskell, running under GHC,

  (DA)  DoCon-A 2.00-pre   written in Agda, 
                           running under Agda 2.5.2 -like.

(D) and (DA) keep fractions with numerator and denominator mutually
coprime, and cancel fractions most eagerly by gcd.

(GHC)  does not cancel by gcd so eagerly.

The performance comparison on Harmonic is:
                                       
                (D) >> (GHC) > (DA).

(D) takes  n = 200.000  easily, while GHC "hangs" on 20.000
    -- for a 3 GHz machine.

(GHC) is considerably faster (DA) 
      (DA hangs for long on 4000).

The method in (DA) is the same as (D). 
gcd is almost as fast as GHC.gcd, this has been tested.
Division (with remainder) is via  dimMod  of Agda-prelude, it is fast.

And I wonder why (DA) is so slow.
(DA) carries all the needed proofs (for coprimality, and such).
But I hope, this does not effect performance any essentially.

Can anybody provide the code for testing Harmonic for  Rational numbers
in  agda-prelude ?

The (DA) test for (Fraction Integer) is like this:

------------------------------------------------------------------------
...
open Fraction.F0 Int1.integralRing-with∣? Int1.gcdRing using
                                 (Fraction; fraction; fraction-showInst)
open Fraction.F1 Int1.integralRing-with∣? Int1.gcdRing using (frRingoid)
open Ringoid frRingoid using (_-_)
open Fraction

inv-n :  ℕ → Fraction              -- \n → 1/(1+n)        
inv-n n =
        fraction (+ 1) (+ (suc n)) +suc≢+0

f : ℕ → Fraction    -- sum [1/n | n <- [1 .. n+1]]                
f n =
    sum frRingoid (map inv-n (natSegment 0 n))

main : IO Unit
main = (readFiniteFile "data.txt") >>= putStrLn ∘ toCostring ∘ g
  where
  g : String -> String
  g str =
    -- n  is first read from file  data.txt
                       
    concatStr
    ("n = "                 ∷  showNat n                 ∷ ",   " ∷
     "num (f n - f n) =  "  ∷  showInt (num (fn - fn))   ∷ "\n\n"   
     ∷ []
    )
    where
    n  = stringToNat $ filterStr decimalDigit? str
    fn = f n
-------------------------------------------------------------------------


So far, I do not find the performance bottleneck in (DA).

Thanks,

------
Sergei