[Agda] Nat arithmetic performance

[Sergei Meshveliani]

People,

Please, find attached a certain test for performance of arithmetic in
Agda, as compared to ghc-7.10.2.

Shortly saying, it is 
                   sum [x*x - y*y | x, y <- [n .. 0]],  
                   n = 1000, ..., 6000, ...

The Hasell program is also there. 

{-
--------------------------------------------------------------------            
Timing for  Agda of September 16, 2016,  ghc-7.10.2,  3 GHz computer

 n    |  s (control)    |    time [sec]
      |                 | Agda     ghc-7.10.2 -O
--------------------------------------------------                              
 1000 |    166499833500 |  0.3  |  0.04
 2000 |   2665332667000 |  1.3  |  0.2
 3000 |  13495498500500 |  3.0  |  0.4
 4000 |  42655997334000 |  5.1  |  0.8
 5000 | 104145829167500 |  8.0  |  1.6
 6000 | 215963994001000 | 11.9  |  2.5
-}

The cost order of  n^2  is as needed. 
Bug GHC is somewhat 5 times faster.
I think, this factor of 5 is not so important.
But still, what may be its source? 

The Haskell program sets  n  in its code, but this does not change
performance, because reading and parsing "6000" in Agda takes certainly
less than 0.1 sec.

Another question is on Standard library.
The functions  decimalDigit?, filterStr, readNat 
are used to parse n : Nat.
Has Standard library something for this?

Thanks,

------
Sergei


-------------- next part --------------
import Foreign.Haskell
open import IO.Primitive        using (IO; readFiniteFile; _>>=_; putStrLn)
open import Data.String as Str  using (String; toCostring)
open import Data.Char   as Char using (Char)

open import Function                   using (_∘_; _$_; case_of_)
open import Relation.Nullary           using (yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Unary using (Decidable) 
open import Data.Product   using (_×_; _,_; _,′_; proj₁; proj₂)
open import Data.List using (List; []; _∷_; map; _++_; reverse; filter; foldr)
open import Data.Nat  using (ℕ; suc; _*_; _+_; _∸_; _≤_; _≤?_)
import Data.Nat.Show as NatShow


-- Prelude -----------------------------------------------------------------

concatStr : List String → String
concatStr = foldr Str._++_ ""

filterStr :  ∀ {p} {P : Char → Set p} → Decidable P → String → String
filterStr P? =  Str.fromList ∘ filter (⌊_⌋ ∘ P?) ∘ Str.toList

listPairs : ∀ {α β} {A : Set α} {B : Set β} → List A → List B → List (A × B)
listPairs []       _  =  []
listPairs (x ∷ xs) ys =  (map (_,_ x) ys) ++ (listPairs xs ys)

sum : List ℕ → ℕ 
sum []       =  0
sum (n ∷ ns) =  n + (sum ns)

downFrom : ℕ → List ℕ
downFrom 0       =  []
downFrom (suc n) =  n ∷ downFrom n

isDecimapDigit : Char → Set
isDecimapDigit c =  48 ≤ n × n ≤ 57  where
                                     n = Char.toNat c

decimalDigit? : Decidable isDecimapDigit
decimalDigit? c =
                let n = Char.toNat c
                in
                case ((48 ≤? n) ,′ (n ≤? 57)) of \
                                   { (yes le ,  yes le') → yes (le , le')
                                   ; (no 48≰n , _      ) → no (48≰n ∘ proj₁)
                                   ; (_ ,       no n≰57) → no (n≰57 ∘ proj₂)
                                   }

charToDecDigitNat : Char -> ℕ
charToDecDigitNat c = (Char.toNat c) ∸ 48

readNat : List Char -> ℕ                 -- convert from decimal digit chars  
readNat =  toN ∘ map charToDecDigitNat ∘ reverse
           where
           toN : List ℕ -> ℕ
           toN []       = 0
           toN (j ∷ js) = j + (10 * (toN js))

stringToNat : String → ℕ
stringToNat = readNat ∘ Str.toList

-- NN-Show  = pairShow Nat0.showInst Nat0.showInst
-- NL-Show  = listShow Nat0.showInst
-- NNL-Show = listShow NN-Show

-- End - Prelude -----------------------------------------------------------


f : ℕ × ℕ → ℕ 
f (m , n) =  (m * m) ∸ (n * n)

test : ℕ → String
test n = 
       concatStr
       ("n = "         ∷ (NatShow.show n)            ∷
        "\ns =  "      ∷ (NatShow.show s)            ∷ 
        -- "\nxs =\n "    ∷ (Show.shownS NL-Show 0 xs)  ∷ 
        []
       )
       where
       xs    = downFrom n
       pairs = listPairs xs xs
       s     = sum $ map f pairs 

  
main = (readFiniteFile "data.txt") >>= putStrLn ∘ toCostring ∘ h
       where
       h : String -> String
       h str =  test n
                where
                n = stringToNat $ filterStr decimalDigit? str




{- -----------------------------------------------------------------
Timing for  Agda of September 16, 2016,  ghc-7.10.2,  3 GHz computer

 n    |  s (control)    |    time [sec] 
      |                 | Agda     ghc-7.10.2 -O
--------------------------------------------------
 1000 |    166499833500 |  0.3  |  0.04     
 2000 |   2665332667000 |  1.3  |  0.2 
 3000 |  13495498500500 |  3.0  |  0.4
 4000 |  42655997334000 |  5.1  |  0.8
 5000 | 104145829167500 |  8.0  |  1.6
 6000 | 215963994001000 | 11.9  |  2.5  
-}


{- Haskell program ----------------------------------

sum' :: [Integer] -> Integer
sum' []       =  0
sum' (n : ns) =  n + (sum ns)

downFrom :: Integer -> [Integer]
downFrom 0 =  []
downFrom n =  (pred n) : downFrom (pred n)

minus :: Integer -> Integer -> Integer
minus m n =
          if m <= n then 0 else m - n

f :: (Integer , Integer) -> Integer
f (m , n) =  minus (m * m) (n * n)

test :: Integer -> String
test n = concat
         ["n = ",       show n,
          "\ns =  ",    show s
          -- "\nxs =\n ",  show xs
         ]
         where
         xs    = downFrom n
         pairs = [(x , y) | x <- xs, y <- xs]
         s     = sum' $ map f pairs

n = 6000  :: Integer

main =  putStrLn (test n)
----------------------------------------------------

Making and running:
 
       > ghc -O --make TT
       > time ./TT
-}