[Agda] Performance issues with --sharing

[Sergei Meshveliani]

On Thu, 2015-09-24 at 13:57 -0300, Peter Selinger wrote:
> Dear all,
> 
> last month, in the thread "type check performance", Wolfram Kahl
> suggested that I try the experimental --sharing feature in the
> development branch.
> 
> The issue at hand was Agda's extremely inefficient evaluation
> strategy, which is normal order and not lazy: it recomputes the same
> value a potentially unlimited number of times.
> 
> [..] 
>
> I've created a self-contained example below. In order to compare
> different Agda versions without depending on different versions of the
> standard library, I have made the example to be completely independent
> of the library.
> 
> Here are the results:
> [..]
> 
> ----------------------------------------------------------------------
> -- Begin Agda Code
> ----------------------------------------------------------------------
> 
> -- Natural numbers
> data Nat : Set where
>   zero : Nat
>   succ : Nat -> Nat
> 
> _+_ : Nat -> Nat -> Nat
> zero + m = m
> succ n + m = succ (n + m)
> 
> _-_ : Nat -> Nat -> Nat
> zero - m = zero
> n - zero = n
> succ n - succ m = n - m
> 
> {-# BUILTIN NATURAL Nat #-}
> {-# BUILTIN NATPLUS _+_ #-}
> {-# BUILTIN NATMINUS _-_ #-}
> 
> -- Lists
> data List (X : Set) : Set where
>   nil : List X
>   _::_ : X -> List X -> List X
> 
> replicate : ∀ {X} -> Nat -> X -> List X
> replicate zero x = nil
> replicate (succ n) x = x :: replicate n x
> 
> foldl : ∀ {A B} -> (A -> B -> A) -> A -> List B -> A
> foldl f a nil = a
> foldl f a (x :: xs) = foldl f (f a x) xs
> 
> -- Test
> test : Nat -> Nat
> test n = foldl (\a x -> succ ((a + x) - a)) 0 (replicate n 1)


But how precisely the test is run?

For  n : Nat   
     n = 12345678,

how much  (show n)  will take?
Will the test convert  n  into the unary system and back?

(I do not know what is the effect of the above BUILTIN).

Instead of measuring the true  foldl,  could happen so that it measures
the conversion costs of  Decimal <--> Unary  for  n  ? 

In the performance tests, I do not use BUILTIN, and use the binary
arithmetic of Bin for the counter like  n  above.
And I do not know, may be BUILTIN is simpler.

Thanks,

------
Sergei