[Agda] Performance issues with --sharing

[Peter Selinger]

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 have tested --sharing on various examples, and the results are not
encouraging: I have not been able to find any code examples where
--sharing will actually speed up performance. On the contrary, it
usually slows things down by a factor of 2 or more.

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:

Using Agda 2.4.2.3:

test 15: ca. 1 second
test 16: ca. 2 seconds
test 17: ca. 4 seconds
test 18: ca. 8 seconds

Using the development version without --sharing (master revision df481626e):

test 15: ca. 1 second
test 16: ca. 2 seconds
test 17: ca. 4 seconds
test 18: ca. 8 seconds

Using the development version with --sharing (master revision df481626e):

test 15: ca. 2 second
test 16: ca. 4 seconds
test 17: ca. 9 seconds
test 18: ca. 19 seconds

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).

I think a proper lazy evaluation strategy will eventually be a
must-have feature, and unfortunately, --sharing does not seem to be
it. Right now I am rewriting many of my programs using forced
strictness and CPS translations, and this makes them efficient, but
unreadable (and non-trivial to prove theorems about).

As mentioned in a previous thread: I am aware that the code becomes
more efficient when I compile it to Haskell. But since all of my code
is used inside proofs, it is really the type checking cost that is
affected. 

-- Peter

----------------------------------------------------------------------
-- 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)