问题标签 [continuation-passing]

• 定点组合器是引入递归的非常有用的工具。
• Continuation-Passing 风格是一种 lambda 演算风格，其中函数永远不会返回。相反，您将程序的其余部分作为 lambda 参数传递给您的函数并继续执行它们。它使您可以更好地控制执行流程并更轻松地定义各种流程更改结构（循环、协程等）

但是，我想知道您是否可以用另一种方式表达？我见过的所有 CPS 风格的语言都有一个明确的FIX结构来定义递归。

• 是因为不可能在普通 CPS 中定义定点组合器（或类似的），没有FIX？如果是这样，你知道这件事的证据吗？
• 或者仅仅是因为打字问题？
• 或者也许这是可能的，但由于某种原因不切实际？
• 或者我根本没有找到一个解决方案......？

我希望类似 Y-combinator 的 CPS 函数CPSY可以这样工作：如果我定义一个 Y-ready CPS 函数，例如：

然后我会将它放入CPSY以产生一个递归到自身的函数：

CPSY应该是一个简单的延续传递风格的函数，它本身不依赖于任何递归。Y-combinator 可以在没有内置递归的普通 lambda 演算中以这种方式定义。它也能以某种形式存在于 CPS 中吗？

重申一下：我正在寻找一个类似组合器的函数CPSY：

• 将启用 CPS 函数的递归
• 它的定义不依赖递归
• 它的定义以连续传递样式给出（在 的主体内任何地方都没有返回 lambda CPSY）

我正在尝试证明连续传递风格（CPS）Monad 的 Monad 定律（左右单位 + 关联性）。

我正在使用来自https://coq.inria.fr/cocorico/AUGER_Monad的基于类型类的 Monad 定义：

CPS 类型构造函数来自 Ralf Hinze 的Functional Pearl关于编译时解析Haskell 中

我定义bind并return_喜欢这个

但我坚持对right_unitand的证明义务associativity。

规定义务right_unit：

非常感谢您的帮助！

编辑：András Kovács 指出类型检查器中的 eta 转换就足够了，所以intros; apply eq_refl., 或reflexivity.就足够了。

首先，我必须更正我对bind. （无形的论点c是在错误的一面)......

试图在 haskell 中为这个 monad 定义绑定。如果计算成功，则调用 SCont 延续，如果计算失败，则调用 FCont 延续。

有没有办法链接函数withCString？我的意思是任何看起来像f :: Foo -> (CFoo -> IO a) -> IO a.

例如，假设有一个函数cFunc :: CString -> CFoo -> CBar -> IO ()

通常，我会做类似的事情：

但我想做类似的事情：

带有一些适当的组合运算符|.|。

我正在编写带有很多 C 绑定的库，并且这个样板经常出现。难道我做错了什么？

我正在查看延续传递样式教程，无法理解以下函数中的类型。

以上是对以下内容的改造：

查看 Atom 编辑器提供的类型信息，我可以看到s :: (a -> r) -> r, f :: a -> (b -> r) -> r, k :: b -> r. 此外在zisx类型x :: a.

对此我感到困惑的z是 type z :: a -> r。

这意味着应用到后s z应该是类型。rzs

如果是这样，最终类型是如何产生的(b -> r) -> r？

编辑：b -> r来自k...对。正如编辑所说，这意味着z真的是 type 。a -> r但是为什么下面的类型检查失败了？

I have superficially read a couple of blog articles/Wikipedia about continuation-passing style. My high-level goal is to find a systematic technique to make any recursive function (or, if there are restrictions, being aware of them) tail-recursive. However, I have trouble articulating my thoughts and I'm not sure if what my attempts of it make any sense.

For the purpose of the example, I'll propose a simple problem. The goal is, given a sorted list of unique characters, to output all possible words made out of these characters in alphabetical order. For example, sol("op".toList, 3) should return ooo,oop,opo,opp,poo,pop,ppo,ppp.

My recursive solution is the following:

I did try to rewrite this by adding a function as a parameter but I did not manage to make something I was convinced to be tail-recursive. I prefer not including my attempt(s) in the question as I'm ashamed of their naiveness, so please excuse me for this.

Therefore the question is basically: how would the function above be written in CPS ?

我正在寻找关于如何将各种编程语言结构转换为 Z3 的讨论，而不限制求解器的效率。

特别是，是否有一种算法和一组最佳实践规则来将一个以延续传递风格表示的函数/程序转换为 Z3？

使用上下文是使用 Z3 来实现编程语言的类型系统，因此解决方案必须高效且增量（例如，在 Z3 实例中保留以前的 Z3 AST）。

我知道 Boogie，但如果可能的话，我正在寻找更轻量级的东西。

在某种程度上限制输入语言的语义是可以接受的，但目前还不能在 SMTLIB 中简单地表达。

我基本上是在寻找关于人们可能会考虑用于各种典型语言结构的不同策略的讨论。

编辑：限制使输入语言不完整并且仅对较小的程序片段（如库中的函数）合理有效，这可能是可以接受的。例如，输入语言可以是一种用于编写“静态检查”库的语言，该库随后被转译为现有动态编程语言的库，并在适当时使用动态运行时断言。

我来自 OOP，非功能性背景，因此我无法完全可视化几个有关continuation pass的在线示例。此外，像 Scheme 这样的函数式语言不必指定参数类型或返回值，所以我不确定我是否正确理解了这个想法。

由于 C# 支持 lambda，我从 Wikipedia 文章中获取了第一个示例，并尝试将其移植到具有强类型的 C#，以查看该模式将如何应用：

因此，用 C# 重写 CPSpyth&版本会导致：

我本可以使用泛型而不是double，但签名会更长。无论如何，我不确定的是：

1. 上面的Cont签名是否正确（即Func<double, double>）？应该继续fn。接受参数，处理它，然后返回相同类型的值？

2. 当我第一次开始阅读关于延续的文章时，我觉得这个延续函数将在调用堆栈中的每个步骤中被调用，但在上面的示例中，它只传递sqrt&给" 原始延续的中间值。上面函数中的代码基本上类似于k(Math.Sqrt(x * x + y * y))，那么这是否意味着我对中间“钩子”的假设是错误的？

我正在尝试Vector在 Attoparsec 中添加一些功能以提高效率，但我遇到了麻烦。

如果 Attoparsec 不是使用 CPS 编写的，我可以使用功能展开器，但这不是这里的选项。问题是所有调用都必须在此处的尾部位置，并且在事物的标准意义上没有函数返回，因此数组必须作为累加器传递。

我尝试使用 ST monad 来做到这一点，但是当那不起作用时，我尝试了上述方法，但即便如此它也无法正常工作。Haskell 的类型系统在这里真的要了我的命。在使用 CPS 编程时是否可以编辑可变数组？

如果可以在 ST monad 中做到这一点，我将倍加感激。

但是，告诉我使用数组以外的数据结构的帖子将被否决。

一个非常典型的用例：一个对象（或类）声明了几个相关类型的公共 val，并且它想声明一个访问器，返回一个包含所有这些的集合：

这个例子显然违反了 DRY 并且容易出错。使用可变状态可以很容易地解决它（例如向构造函数添加隐式Builder[Ball, Seq[Ball]]参数Ball。但是，该解决方案也不是没有问题。特别是当我们尝试概括解决方案和/或具有每个类都声明的类层次结构时一些值，我们应该从可变部分摘要切换到最终不可变值的时刻尚不清楚。

更多的是作为一种智力练习，出于好奇，我试图提出一个纯粹的功能变体，但没有取得多大成功。我想出的最好的是

这是相当整洁的，但一旦球或它们的初始化器的数量不小，就会变得难以管理。一个可行的替代方法是将所有内容都更改为 HMap，但我通常会尽量避免公共 API 中的无形依赖。似乎它可能对 scala 延续是可行的，但我不知道如何使声明非本地到重置块。

编辑：我以前没有强调过，为什么scala.Enumeration不为我做这项工作的原因是，在实际情况下，对象并不相同，但实际上是复合结构，构造函数需要几行或更多行. 因此，虽然最终类型可能相同（或者至少我对细节不感兴趣），但它不是一个简单的枚举，并且出于可读性原因，声明的成员/键的名称可以是很重要的很容易在视觉上与它的定义联系起来。所以我在这里的无形解决方案，以及基于 Seq 的无形解决方案，很容易受到一个错误的影响，即通过错误的真实标识符对错误的值进行修改。

当然，目前真实案例的实现方式与 scala.Enumeration 类似，通过维护继承的构造方法产生的一系列值。然而，它会遇到 Enumeration 会遇到的所有问题，并且会因在实际初始化程序之外调用构造object Balls函数或丢弃条件块中的值而放大错误的可能性。此外，我对如何用纯函数式语言解决这个问题非常感兴趣。

有什么想法如何吃蛋糕吗？