时间戳

首页 > 解决方案 > Idris 是否使用尾调用优化？

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

问题描述

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

这个 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 通过将代码转换为没有递归错误风险的命令式循环来编译代码。我相信它作为命令式循环也可能更快。

在布雷迪的伊德里斯书中，他使用了这个例子

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

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

标签： tail-recursionidris

解决方案

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，goandallLengths和尾递归函数调用的循环完全消除了，只需将值存储到函数参数中以供循环的下一次迭代使用while。我们还可以看到用于在尾部位置调用的其他函数的蹦床 thunk（函数reverse调用）的 lambda。allLengthsJVM 后端当前没有转换非尾递归函数，因此它们仍然可以耗尽堆栈。

推荐阅读