Suspicious slow-down when introducing a meta-variable

[omelkonian]

In the current Agda Implementor's Meeting, we are trying to ~steal~find ideas in smalltt to improve Agda's performance. In the process of doing so, in the context of deciding whether to instantiate meta-variables eagerly/early or lazily/later, we came across a benchmark in Agda which exhibits the case where not instantiating a meta-variable renders subsequent term traversals more costly in an exponential fashion.

We ported this example to smalltt and it seems that indeed introducing a variable leads to a significant performance hit, while Agda is unaffected currently:

Nat : U
 = (n : U) → (n → n) → n → n

zero : Nat
 = λ n s z. z

mul : Nat → Nat → Nat
 = λ a b n s. a n (b n s)

Eq : {A} → A → A → U
 = λ {A} x y. (P : A → U) → P x → P y

refl : {A}{x : A} → Eq {A} x x
 = λ P px. px

--------------------------------------------------------------------------------

n2 : Nat = λ N s z. s (s z)
n5 : Nat = λ N s z. s (s (s (s (s z))))
n10   = mul n2 n5
n100  = mul n10 n10
n1000 = mul n10 n100
n10000 = mul n10 n1000
n100000 = mul n10 n10000
n1000000 = mul n10 n100000
n10000000 = mul n10 n1000000

yippie : (A : U) → A
  = _

fast : (A : U) → Nat → A
  = λ A n. n ((A : U) → A) (λ r A. r A) yippie A

slow : (A : U) → Nat → A
  = λ A n. n ((A : U) → A) (λ r _. r _) yippie A

testFast [elabtime]: Eq (fast Nat n1000000) (yippie Nat)
  = refl

testSlow [elabtime]: Eq (slow Nat n1000000) (yippie Nat)
  = refl

smalltt 2.0.0
enter :? for help
> :l bench/late_meta.stt
bench/late_meta.stt parsed in 0.000040429s
testFast elaborated in 0.154774439s
testSlow elaborated in 0.578733852s
bench/late_meta.stt elaborated in 0.733892344s
created 11 metavariables
loaded 20 definitions
total load time: 0.73471356s

[nad]

A little more context: Back in 2010 @UlfNorell and I noticed that some Agda code that should be linear wasn't, and found a way to make the code faster. The problem is described in the commit comment. The solution we chose was to replace a meta-variable application α A n with its instantiation A. However, instantiating meta-variables can lead to other problems. Perhaps it would make sense to perform this kind of instantiation when the solution is sufficiently small (and the size of the solution can be computed quickly).

[AndrasKovacs]

The slowdown here seems to be a constant factor. It's expected, and it's entirely because of the overhead of the extra inserted meta (with the construction/deconstruction of the unfolding and the extra application).

As I mentioned in the README, currently there's no optimization of elaboration output at all. It makes sense to inline small and linear solutions, and in fact I did exactly this in the old smalltt branch.

There are IMO two complementary ways to add inlining:

• When solving a meta, it can be immediately marked inlinable if "small", and during evaluation we can omit building lazy unfoldings for inlinable metas.
• After elaborating a top-level binding group (or any "meta freezing" unit), we can walk the output and actually perform inlining.