问题标签 [callcc]

直观的逻辑，具有建设性，是函数式编程中类型系统的基础。经典逻辑不是建设性的，尤其是排中律A ∨ ¬A（或其等价物，例如双重否定消除或皮尔斯定律）。

但是，我们可以实现（构造）call-with-current-continuation运算符（AKA call/cc），例如在Scheme中。那么为什么call/cc没有建设性呢？

我不明白以下内容如何不设置无限循环：

当我调用 时(return 22)，我跳回继续，但使用传递的值 22 作为call/cc表单的新评估结果。这不会导致(return 22)被评估为下一条语句，从而设置一个无限循环吗？

我知道这不是无限循环，但我不明白为什么不是。

我在球拍上尝试这个，它给出的答案是 5。但我似乎无法弄清楚它是如何得到答案的。

我将其扩展如下。

假设扩展是正确的，我仍然不明白当 k 延续应用于 k1 延续时会发生什么，以及它如何执行外部 lambda 以产生 5。

Racket 中的延续类型是什么？以及如何确定查看 call/cc 调用的当前延续？（例如：假设当前的延续是紧跟在 call/cc 右括号之后的内容是正确的策略吗？）

考虑以下定义。我正在使用球拍。

现在如果它调用如下

（五一）

它什么也没有。这样做后，如果直接调用 5，它会给出 120。

五美元

120

但是如果我重试（5 1）它会失败，说 120 不是程序。

我知道最初有五个点指向在（零？n）基本情况下捕获的延续。但我不确定如何解释上述行为。

另一个使用不同参数的运行

$（五四）

五美元

480

我完全迷失了 Scheme 中的通话继续。有人可以帮我这个例子吗？

我了解第一个结果（3），但我不了解 2017 年的结果。

在Lisp in Small Pieces一书中，有以下示例代码，旨在演示call/cc可以模拟 goto。

但是，我不确定我是否误解了某些东西，但我看不出这是call/cc模拟 goto 的方式。当k在最后一行应用时，恢复的延续具有原始延续的r和n，其值不会被两个应用程序更改set!。所以整个循环永远不会终止。

这个例子中的书错了吗？还是我错过了什么？

前言

我正试图围绕如何实际使用ContT和callCC寻找有用的东西。我在跟踪代码周围的信息和控制流时遇到了麻烦。（但是，这不是延续的意义吗？）

有很多不同的方法可以使用这个 monad 和一小部分不太直接的组合器来移动片段。我承认我仍然对我对 ContT 工作原理的理解感到不舒服，但我会指出我到目前为止所读到的内容：

• Haskell/继续传球风格
• Haskell Cont monad 如何以及为什么工作？
• 理解 Haskell callCC 例子
• Haskell 中的 Goto：谁能解释这种看似疯狂的 continuation monad 使用效果？
• 如何在 Haskell 中解释 callCC？
• Parsec 一般（让我开始走这条路的文章）

我想做的是发布一个伪代码示例，然后问一些关于它的问题。这代表了使用 ContT 的代码的典型外观

伪代码

问题

1. 是什么决定了它的价值和类型output？
2. b的类型是什么意思k？
3. 赋予的价值k去哪儿了？
4. 什么时候inner_block运行？它看到的是什么版本的状态？
5. 去哪里rval，它的类型是什么？
6. k和之间有什么关系rval？
7. 当我申请ka) in inner_block, b) in after_callcc, c) outside 时会发生block什么？
8. 上述每个状态的版本是什么？
9. 我需要做什么才能k摆脱block？
10. 我可以放入k状态吗？

颜色编码，便于阅读

我正在call/ccRacket 中按照论文Continuations by example: Exceptions, time-traveling search, generators, threads, and coroutines 1学习。

该论文提到，最有利的 API 是call/cc通过提供一个过程派生而来的lambda (cc) (cc cc)。我理解这个特定call/cc的调用将当前的延续一等对象返回给主程序。

在下面的示例中，本文将所有 this 称为(right-now).

我看到的是，在同一个示例中cc，上述call/cc调用返回的对象总是在之后通过将其应用于自身来运行。这就是我不明白的。

我没有看到 value 有什么特别之处cc，所以我尝试用(cc ()), or (cc (lambda () ())), 甚至(cc "whatever")and来启动它(cc)。没有任何乐趣：显然，延续只需要该应用程序自己才能开始运行。

这是为什么？有什么例子可以清楚地说明运行 cc 的独特性(cc cc)？

我正在阅读这个有趣的页面，解释球拍中的延续。

他们提供代码来保存计算的当前延续（稍后使用这个技巧来实现回溯）。代码如下所示：

现在我想在标准 ML 中做同样的事情，因为新泽西州的 SML 似乎是唯一实现延续的解释器，所以我在那里做。

那里的延续签名如下所示：

直接翻译是：

但是 ML 的类型系统禁止这样做（因为这是循环的）。

所以我尝试了类似的东西：

以及其他各种带有引用的技巧，但我找不到真正保存当前延续的方法（因为在此示例中，我之后使用 !glcc 更改了想要的延续）。

有谁知道实现运算符的方法savecc，backjump让我保存程序的当前延续，然后在标准 ML 中跳回到那个点？

提前谢谢了！

雅尼克