tail-recursion - Idris 是否使用尾调用优化？

Question

我从斯卡拉来到 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 注释它，编译错误

error: could not optimize @tailrec annotated method zip: it contains a recursive call not in tail position

因为该函数不直接返回对 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 ，但前者不保证完整性，后者不保证尾递归

Answer 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和 go内 reverse是尾递归的，还要注意 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"));
            }
        }
    }

我们可以看到 while两个循环 go和 allLengths并且通过将值存储到函数参数以供 while 的下一次迭代而完全消除尾递归函数调用。环形。我们还可以看到用于在尾部位置调用的其他函数的蹦床 thunk 的 lambda( reverse 调用 allLengths 函数)。非尾递归函数当前不会被 JVM 后端转换，因此它们仍然可以耗尽堆栈。