[Agda] summing rationals

[Sergei Meshveliani]

On Sun, 2017-06-25 at 09:46 +0200, Ulf Norell wrote:
> 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:
> 
> 
> module Harmonic where
> 
> 
> open import Prelude
> open import Numeric.Rational
> 
> 
> -- sum [ 1/k | k <- [1..n] ]
> harmonic : Nat → Rational
> harmonic 0 = 0
> harmonic (suc n) = sum (map (λ k → ratio 1 (suc k) refl) (from 0 to
> n))
> 
> 
> test : Nat → Rational
> test n = harmonic n * 0
> 
> 
> main : IO ⊤
> main =
>   caseM getArgs of λ where
>     (s ∷ []) → print (test <$> parseNat s)
>     _ → pure _
> 


1. It appears that final  fn - fn  in my test costs as much as all the 
   rest.
Instead using (_* 0), as in your test, reduces the cost twice (because
fn is large).

And I suggest to apply the final taking a remainder by 1000: 

  toSmall :  Fraction → ℕ
  toSmall f =
            rem $ divMod (∣ num f ∣ + ∣ denom f ∣) 1000 {suc≢0}

take the remainder by 1000
(my divMod is agda-prelude.divMond with swapped arguments -
the classical tradition is that the dividend is first).

This is safe for the cost, and it is safe against the rule  
_ * 0 = 0   which may be possible in some implementations.



2. Further, I have the three versions:

  _+₁_   to add fractions as in GHC (and as in agda-prelude, I expect),

  n₁/d₁ +fr n₂/d₂ =  h *fr (f' + g')
                     where
                     h = (gcd n₁ n₂) / (gcd d₁ d₂)
     -- where f' and g' are canceled by a certain gcd,
     and using coprimality for several corresponding pairs, in 
     order to reduce the usage of  gcd.

  _+fr'_  -- as in Knuth and as in DoCon.
          It finds certain additional intermediate gcd, and relies on a 
          certain additional coprimality.

In DoCon (Haskell under GHC) ,  +fr'  is the most efficient.
In DoCon-A (Agda),  the most efficient is  +₁.

+₁   now shows    5.5 sec for n = 2000,  and  288 sec for 10,000
(3 GHz machine).

+fr      shows   11.8 sec for n = 2000,  and  625 sec for 10,000.

+fr'     is only 25% faster than _+fr_
         (and it must be many times faster).


Probably,  +₁  has performance close to agda-prelude.
But I need to find of how to fix  +fr'   in order to make it close to
DoCon.
  
Regards,

------
Sergei