[Agda] evaluation strategies of the future [issue #426]

[Sergei Meshveliani]

On Tue, 2016-10-25 at 14:19 +0200, Ulf Norell wrote:
> Before we discuss any particular solution to get call-by-need working,
> it's useful to distinguish between two separate problems one might
> envision call-by-need solving. The first, which I believe is the one
> you are interested in, is to get efficient compile-time evaluation.
> The second is to reduce the memory requirements of type checking by
> having more sharing in terms. These are related but the second goal
> requires more care during other phases of type checking than pure
> evaluation (such as unification).
> 
> 
> The current implementation of `--sharing` is a hack using `IORef`s to
> see how far it would get us towards solving problem number 2 (not very
> far). The main problem with it, aside from being hacky, is that
> `IORef`s are too persistent, so you run into problems when working
> interactively. For instance, once you've looked at the normal form of
> a goal type you cannot get back the original goal type, since it's
> been destructively updated to its normal form. You could imagine ways
> to solve this problem, for instance by making deep copies of terms
> before working on them, but it's easy to miss cases and since the
> current implementation isn't really that nice to begin with we haven't
> spent time on that.
> [..]


Consider a known example: 

-------------------------
module FoldlTest where
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 20 ≡ 2   -- put here  n = 18, 19, 20, 21 ...  instead of 20
lemma = PE.refl
--------------------------

Its type check by  
               > agda $agdaLibOpt FoldlTest.agda

has the cost growing exponentially in  n

(this is for Development Agda of October 4, 2016).

Adding  --sharing  improves this. For example, it becomes that 
time(5) is near time(90).  
  
Can anybody provide a small and clear example having an exponential type
check cost both with --sharing and without it?

(for in the case of my CA library, --sharing does not help).

Thanks,

------
Sergei