Suggestion: Optimize tail-recursive definitions when evaluating

[UlfNorell]

From victor@lopezjuan.com on September 25, 2013 12:14:54

A couple of examples:

\begin{code} module TailRec where

open import Data.Nat

-- Good old exponentiation ** : ℕ → ℕ → ℕ m * n = pow' 1 m n where pow' : ℕ → ℕ → ℕ → ℕ pow' acc _ zero = acc pow' acc m (suc n) = pow' (m \ acc) m n

-- A sophisticated identity function dummy : ℕ → ℕ dummy n = dummy' zero n where dummy' : ℕ → ℕ → ℕ dummy' acc zero = acc dummy' acc (suc m) = dummy' (suc acc) m \end{code}

With the default stack size, both (2 \ 100000) and (dummy 1000000) throw a stack-overflow error; it seems they are pushing up to 100_000 or 1_000_000 frames into the stack, respectively.

Most functional languages optimize tail-recursive functions so that they only use O(1) stack space. Could Agda do something similar?

Original issue: http://code.google.com/p/agda/issues/detail?id=912

[UlfNorell]

From andreas....@gmail.com on September 28, 2013 07:03:55

The problem here is that Agda expands 1000000 into its unary representation eagerly. So, the argument to dummy is a linked list of length 1000000. The question is of course, why?

Enhancement request: expand literal numbers lazily!

Summary: Lazy computation of constructor form [WAS: Optimize tail-recursive definitions when evaluating] (was: Suggestion: Optimize tail-recursive definitions when evaluating)
Status: Accepted
Labels: Type-Enhancement Priority-Medium PatternMatching Literals

[UlfNorell]

From andreas....@gmail.com on September 28, 2013 07:19:58

Ah sorry, my comment is incorrect. Agda does compute the constructor form lazily when matching. But the accumulator is constructed by iterated suc from zero, which constructs this linked list. But this does not explain why you get a stack overflow.

So it must have something to do with a non-tail-recursive implementation of evaluation in Agda. In fact, I would have been suprised if evaluation of tail-recursive things was tail-recursive itself...

Summary: Suggestion: Optimize tail-recursive definitions when evaluating (was: Lazy computation of constructor form [WAS: Optimize tail-recursive definitions when evaluating])