我从斯卡拉来到 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,我很惊讶他没有以尾递归的方式编写它。几个问题:@tailrec
感觉很像total
,但前者不保证完整性,后者不保证尾递归最佳答案
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 后端转换,因此它们仍然可以耗尽堆栈。
关于tail-recursion - Idris 是否使用尾调用优化?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/62665251/