agda - 在 Agda 中启用尾调用优化

Question

我将 Emacs 与 一起使用agda-mode，并编写了这个函数：

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并且*被定义为与 Agda 的自然数内部定义兼容。

当我评估时，(pow 2 100000)我得到一个堆栈溢出错误。但是，鉴于递归调用是尾调用，我希望 agda 解释器优化pow'成一个循环。

如何启用此优化？

Answer 1

当前版本的 Agda 中未实现此优化。替代方法包括增加堆栈的大小，或将递归重写为指数的对数，而不是线性的。

我也被告知：

正在进行深入更改 Agda.TypeChecking.Reduce 模块（以及其他模块）的工作，希望这也将对内置自然的递归产生积极影响。

问题跟踪器上的票证。