[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.
>
> [..]
>
> As you can see, --sharing does not do anything to fix the exponential
> runtime (neither in this example nor in several others that I have
> tried). Instead, it slows things down by a constant factor.
> (The exponential runtime here is caused by folding a function that
> uses the accumulator twice).
>
> [..]


Here is a version of Peter's example which I tried.

This following code is being type-checked by  

               agda $agdaLibOpt  FoldlTest.agda
:
---------------------------------------------------------------------
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.List using (replicate; foldl)
open import Data.Nat  using (ℕ; suc; _+_; _∸_; _*_)

comb : ℕ → ℕ → ℕ
comb a x =  suc ((a + x) ∸ a)

test : ℕ → ℕ
test n = foldl comb 0 (replicate n 1)

lemma : test 19 ≡ 2   -- set here 19, 20, 21, ...
lemma = PE.refl

lemma2 : 12 * 20 ≡ 240                                      
lemma2 = PE.refl                  
------------------------------------------------------------------

lemma2  is added to show that the arithmetic of  0 < n < 200  costs
almost zero with respect to proper  foldl  evaluation. Because
commenting out  lemma2  shows that the cost of  lemma2  is not
essential. 

The timing table for type checking is (on my machine)

{- n    time [sec]   
   18    4     
   19    6                                                        
   20   12   
   21   22  
-}
Indeed, it looks like exponential.

Regards,

------
Sergei