Enable tail-call optimization in Agda

Question

I'm using Emacs with agda-mode, and have written this function:

pow : Nat → Nat → Nat
pow m n = pow' 1 m n
          where
            pow' : Nat → Nat → Nat → Nat
            pow' acc _ zero = acc
            pow' acc m (succ n) = pow' (m * acc) m n

Nat, succ and * are defined to be compatible with Agda's internal definitions of natural numbers.

When I evaluate (pow 2 100000) I get a stack overflow error. However, given that the recursive call is a tail call, I would like the agda interpreter to optimize pow' into a loop.

How can I enable this optimization?

Answer 1

This optimisation is not implemented in the current version of Agda. Alternatives include increasing the size of the stack, or rewriting the recursion to be logarithmic in the exponent, not linear.

I have also been told that:

There is ongoing work to deeply change the Agda.TypeChecking.Reduce module (among others), which hopefully would have a positive impact on recursion over builtin naturals as well.

Ticket on the issue tracker.