gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-04 13:35:02 24 4
gpt4 key购买 nike

我从斯卡拉来到 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 ,但前者不保证完整性,后者不保证尾递归
  • 最佳答案

    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
    这里都有 allLengthsgoreverse是尾递归的,还要注意 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两个循环 goallLengths并且通过将值存储到函数参数以供 while 的下一次迭代而完全消除尾递归函数调用。环形。我们还可以看到用于在尾部位置调用的其他函数的蹦床 thunk 的 lambda( reverse 调用 allLengths 函数)。非尾递归函数当前不会被 JVM 后端转换,因此它们仍然可以耗尽堆栈。

    关于tail-recursion - Idris 是否使用尾调用优化?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/62665251/

    24 4 0
    Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
    广告合作:1813099741@qq.com 6ren.com