Idris 是否使用尾调用优化？答案

【问题标题】：Does Idris use tail call optimization?Idris 是否使用尾调用优化？
【发布时间】：2020-10-21 05:13:08
【问题描述】：

我从 Scala 来到 Idris。 Scala 有尾调用优化 (TCO)，如果它不能使用 TCO 优化递归函数，我可以告诉编译器阻止。例如，请参阅these posts。

这个 Scala 函数成功计算 String 长度

def allLengths(strs: List[String]): List[Int] = strs match {
  case Nil => Nil
  case x :: xs => x.length :: allLengths(xs)
}

但是如果我用annotation.tailrec注释它，编译器会出错

错误：无法优化 @tailrec 注释方法 zip：它包含不在尾部位置的递归调用

因为该函数不直接返回对allLengths 的调用。如果我用很长的List 运行它（没有注释），我会得到“错误：递归过多”，正如预期的那样。

但是，我可以将其重写为

@tailrec
def allLengths(strs: List[String], acc: List[Int] = Nil): List[Int] = strs match {
  case Nil => acc.reverse
  case x :: xs => allLengths(xs, x.length :: acc)
}

与注释一起编译得很好。使用@tailrec，Scala 通过将代码转换为没有递归错误风险的命令式循环来编译代码。我相信它作为命令式循环也可能更快。

在布雷迪的Idris book 中，他使用了这个例子

allLengths : List String -> List Nat
allLengths [] = []
allLengths (x :: xs) = length x :: allLengths xs

可以用total 注释编译，我似乎不会导致递归错误（尽管allLengths (replicate 5000 "hi") 有困难）。来自 Scala，我很惊讶他没有以尾递归的方式编写它。几个问题：

对于非尾递归的递归函数，Idris 中是否可能出现运行时递归错误？
是否在编译期间在 Idris 中优化了尾递归函数？非尾递归呢？
是否有类似 Scala 中的注释来确保 TCO？ @tailrec 感觉和total 很像，但前者不保证整体性，后者不保证尾递归

【问题讨论】：

标签： tail-recursion idris

【解决方案1】：

TCO 主要取决于相应的运行时或 Idris 代码生成的后端系统。他们可以采用 Idris IR，识别尾调用并选择优化它们。由于我一直在为 Idris 开发 JVM 后端，我可以说 Idris 的 JVM 后端确实消除了尾递归，并使用蹦床进行非自我尾调用，而无需用户提供任何显式注释。

以下是 Idris 2 JVM 后端如何处理以下尾递归函数：

reverse : List a -> List a
reverse xs = go [] xs where
  go : List a -> List a -> List a
  go acc [] = acc
  go acc (x :: xs) = go (x :: acc) xs

allLengths : List Nat -> List String -> List Nat
allLengths acc [] = reverse acc
allLengths acc (x :: xs) = allLengths (length x :: acc) xs

这里allLengths 中的allLengths 和go 都是尾递归的，还要注意allLengths 在尾部位置调用reverse。 Idris 2 JVM 后端将这两个函数都转换为字节码级别的循环，但也会蹦床其他尾部调用。这是反编译后的字节码的样子：

    // `go` function decompiled code
    public static Object Main$$nested1190$243$go(Object arg$0, Object arg$1, IdrisObject arg$2, IdrisObject arg$3) {
        while(true) {
            switch(arg$3.getConstructorId()) {
            case 0:
                return arg$2;
            case 1:
                Object e$2 = arg$3.getProperty(0);
                IdrisObject e$3 = (IdrisObject)Runtime.unwrap(arg$3.getProperty(1));
                arg$0 = null;
                arg$2 = (IdrisObject)(new col(1, Runtime.unwrap(e$2), arg$2));
                arg$3 = e$3;
                break;
            default:
                return Runtime.crash("Unreachable code");
            }
        }
    }

    // `reverse` function
    public static Thunk Main$reverse(Object arg$0, IdrisObject arg$1) {
        return () -> {
            return Runtime.createThunk(Main$$nested1190$243$go((Object)null, arg$1, (IdrisObject)(new Nil(0)), arg$1));
        };
    }

    // `allLengths` function
    public static Thunk Main$allLengths(IdrisObject arg$0, IdrisObject arg$1) {
        while(true) {
            switch(arg$1.getConstructorId()) {
            case 0:
                return () -> {
                    return Main$reverse((Object)null, arg$0);
                };
            case 1:
                String e$2 = (String)Runtime.unwrap(arg$1.getProperty(0));
                IdrisObject e$3 = (IdrisObject)Runtime.unwrap(arg$1.getProperty(1));
                arg$0 = (IdrisObject)(new col(1, Runtime.unwrap(Prelude.length(e$2)), arg$0));
                arg$1 = e$3;
                break;
            default:
                return Runtime.createThunk(Runtime.crash("Unreachable code"));
            }
        }
    }

我们可以看到go 和allLengths 的while 循环和尾部递归函数调用被完全消除，只需将值存储到函数参数以供while 循环的下一次迭代。对于在尾部位置调用的其他函数，我们还可以看到蹦床 thunk 的 lambdas（reverse 在 allLengths 函数中调用）。 JVM 后端当前不会转换非尾递归函数，因此它们仍然可以耗尽堆栈。

【讨论】：