延续的正确术语

Question

我最近一直在探索延续，我对正确的术语感到困惑。 HereGabriel Gonzalez 说：

Haskell 延续具有以下类型：

newtype Cont r a = Cont { runCont :: (a -> r) -> r }

即整个(a -> r) -> r 是延续（没有包装）

wikipedia 的文章似乎支持这个想法

延续是控制状态的抽象表示 计算机程序。

不过，here 作者是这么说的

Continuations 是表示“要完成的剩余计算”的函数。

但这只是Cont 类型的(a->r) 部分。这与 Eugene Ching 所说的 here 一致：

需要连续函数的计算（函数） 全面评估。

我们将经常看到这种功能，因此，我们将提供它 一个更直观的名字。我们称它们为等待函数。

我看过另一个教程（Brian Beckman 和 Erik Meijer），他们将整个事物（等待函数）称为 observable 以及完成 所需的函数观察者。

• 什么是延续，(a->r)->r 事物或只是 (a->r) 事物（无包装）？
• observable/observer 的措辞是否正确？
• 上面的引用真的是矛盾的吗，有共同的真理吗？

Answer 1

什么是延续，(a->r)->r 事物或只是 (a->r) 事物（没有包装）？

我会说a -> r 位是延续，(a -> r) -> r 是“延续传递风格”或“是延续单子的类型。

我要对延续的历史进行长时间的题外话了，这与这个问题并不真正相关......所以请注意。

我相信第一篇发表的关于延续的论文是 Strachey 和 Wadsworth 的“Continuations: A Mathematical Semantics for Handling Full Jumps”（尽管这个概念已经成为民间传说）。我认为那篇论文的想法非常重要。命令式程序的早期语义试图将命令建模为状态转换函数。例如，考虑以下 BNF 给出的简单命令式语言

Command := set <Expression> to <Expression>
         | skip
         | <Command> ; <Command>

Expression := !<Expression>
            | <Number>
            | <Expression> + <Expression>

这里我们使用表达式作为指针。最简单的指称函数将状态解释为从自然数到自然数的函数：

S = N -> N

我们可以将表达式解释为从状态到自然数的函数

E[[e : Expression]] : S -> N

和命令作为状态传感器。

C[[c : Command]] : S -> S

这个指称语义可以很简单地拼写出来：

E[[n : Number]](s) = n
E[[a + b]](s) = E[[a]](s) + E[[b]](s)
E[[!e]](s) = s(E[[e]](s))

C[[skip]](s) = s
C[[set a to b]](s) = \n -> if n = E[[a]](s) then E[[b]](s) else s(n)
C[[c_1;c_2]](s) = (C[[c_2] . C[[c_1]])(s)

这种语言的简单程序可能看起来像

set 0 to 1;
set 1 to (!0) + 1

这将被解释为将状态函数 s 转换为类似于 s 的新函数，除了它将 0 映射到 1 和 1 到 2。

这一切都很好，但是你如何处理分支？好吧，如果你想了很多，你可能会想出一种方法来处理 if 和循环的确切次数......但是一般的 while 循环呢？

Strachey 和 Wadsworth 向我们展示了如何做到这一点。首先，他们指出这些“状态转换器函数”非常重要，因此决定将它们称为“命令延续”或仅称为“延续”。

C = S -> S

他们由此定义了一个新的语义，我们将暂时这样定义

C'[[c : Command]] : C -> C
C'[[c]](cont) = cont . C[[c]]

这里发生了什么？好吧，观察一下

C'[[c_1]](C[[c_2]]) = C[[c_1 ; c_2]]

还有更多

C'[[c_1]](C'[[c_2]](cont) = C'[[c_1 ; c_2]](cont)

我们可以内联定义，而不是这样做

C'[[skip]](cont) = cont
C'[[set a to b]](cont) = cont . \s -> \n -> if n = E[[a]](s) then E[[b]](s) else s(n)
C'[[c_1 ; c_2]](cont) = C'[[c_1]](C'[[c_2]](cont)

这给我们带来了什么？嗯，一种解释while的方法，就是这样！

Command := ... | while <Expression> do <Command> end

C'[[while e do c end]](cont) =
  let loop = \s -> if E[[e]](s) = 0 then C'[[c]](loop)(s) else cont(s)
  in loop

或者，使用固定点组合器

C'[[while e do c end]](cont) 
    = Y (\f -> \s -> if E[[e]](s) = 0 then C'[[c]](f)(s) else cont(s))

无论如何......这是历史，并不是特别重要......除了它展示了如何以数学方式解释程序，并设置“延续”的语言。

此外，“1. 根据旧的 2. 内联 3. 利润定义一个新的语义函数”的指称语义方法的效果出人意料地频繁。例如，让您的语义域形成一个格（想想，抽象解释）通常很有用。你怎么知道的？好吧，一种选择是获取域的幂集，并通过将您的函数解释为单例来注入其中。如果你内联这个 powerset 构造，你会得到一些可以模拟非确定性的东西，或者在抽象解释的情况下，除了关于它做什么的确切确定性之外，关于一个程序的各种信息量。

随后进行了各种其他工作。在这里，我跳过了许多伟大的文章，例如 lambda 论文……但是，也许最值得注意的是 Griffin 的具有里程碑意义的论文“A Formulae-as-Types Notion of Control”，它展示了延续传递风格和经典逻辑之间的联系。这里强调“延续”和“评估上下文”之间的联系

也就是说，E 表示在评估 N 之后剩余的计算。在求值序列的这一点上，上下文 E 被称为 N 的延续（或控制上下文）。正如我们将在下面看到的，评估上下文的符号允许对操作延续的操作符的操作语义进行简明规范（实际上，这是它的预期用途 [3,2,4,1]）。

明确“延续”是“只是a -> r 位”

这一切都是从语义的角度看待事物，并将延续视为函数。问题是，作为函数的延续给你的权力比你通过类似方案的 callCC 获得的更多。因此，关于延续的另一个观点是，它们是程序中的变量，将调用堆栈内部化。 Parigot 的想法是让连续变量成为一个单独的句法类别，从而在“λμ-演算：经典自然演绎的算法解释”中产生了优雅的 lambda-mu 演算。

observable/observer 的措辞是否正确？

我认为它是 Eric Mejier 所使用的。这是学术 PL 中的非标准术语。

上面的引用真的是矛盾的吗，有共同的真理吗？

让我们再看看引文

延续是计算机程序控制状态的抽象表示。

在我的解释（我认为这是相当标准的）中，延续模拟程序下一步应该做什么。我认为维基百科与此一致。

Haskell 延续具有以下类型：

这有点奇怪。但是，请注意，Gabriel 在后面的帖子中使用了更标准的语言并支持我使用的语言。

这意味着如果我们有一个有两个延续的函数：

 (a1 -> r) -> ((a2 -> r) -> r)

Answer 2

通过阅读 Andrzej Filinski 的 Declarative Continuations and Categorical Duality 的后续内容，我采用以下术语和理解。

a 值的延续是一个“接受a 值的黑洞”。你可以把它看成一个只有一个操作的黑盒子——你给它一个值a，然后世界就结束了。至少在本地。

现在假设我们在 Haskell 中，我要求你为我构造一个函数 forall r . (a -> r) -> r。假设现在，a ~ Int 它看起来像

f :: forall r . (Int -> r) -> r
f cont = _

类型孔的上下文类似于

r    :: Type
cont :: Int -> r
-----------------
_    :: r

显然，我们能够满足这些要求的唯一方法是将Int 传递给cont 函数并返回它，之后就不会发生进一步的计算。这模拟了“将 Int 提供给 continuation，然后世界结束”的想法。

所以，只要它位于具有固定但未知的r 并且需要返回该r 的上下文中，我就会将函数(a -> r) 称为延续。例如，以下不是延续

forall r . (a -> r) -> (r, a)

因为我们显然被允许从失败的宇宙中传回比仅延续所允许的更多的信息。

---

关于“可观察”

我个人不喜欢“观察者”/“可观察”术语。用那个术语我们可以写

newtype Observable a = O { observe :: forall r . (a -> r) -> r }

这样我们就有了observe :: Observable a -> (a -> r) -> r，它确保只有一个a 将被传递给“观察者”a -> r“观察”它。这为上面的类型提供了一个非常实用的视图，而Cont 甚至the scarily named Yoneda Identity 更明确地解释了该类型实际上是什么。

我认为关键是要以某种方式将Cont 的复杂性隐藏在隐喻后面，以减少“普通程序员”对它的恐惧，但这只是为行为泄漏增加了一层额外的隐喻。 Cont 和 Yoneda Identity 无需修饰即可准确解释类型。

Answer 3

我建议回忆一下 x86 平台上 C 的调用约定，因为它使用堆栈和寄存器来传递参数。这对于理解抽象非常有用。

假设，函数f 调用函数g 并将0 传递给它。这看起来像这样：

mov eax, 0
call g   -- now eax is the first argument,
         -- and the stack has the address of return point, f'
         g: -- here goes g that uses eax to compute the return value
            mov eax,1 -- which by calling convention is placed in eax
            ret -- get the return point, f', off the stack, and jump there
f': ...

您看，将返回点f' 放在堆栈上与传递函数指针作为参数之一相同，然后返回与调用给定函数并传递一个值相同。所以从g 的角度来看，f 的返回点看起来像一个参数f' :: a -> r 的函数。如您所知，堆栈的状态完全捕获了f 正在执行的计算的状态，并且需要g 中的a 才能继续。

同时，在g被调用时，它看起来像一个接受一个参数的函数的函数（我们将该函数的指针放在堆栈上），最终将计算@类型的值987654333@ 表示从f': 开始的代码用于计算，因此类型变为g :: (a->r)->r。

由于f' 是给定一个来自“某处”的a 类型的值，f' 可以被视为g 的观察者——相反，它是可观察的。

这只是为了给出一个基本的想法，并以某种方式与你可能已经知道的世界联系起来。延续的魔力允许做更多的技巧，而不仅仅是将“普通”计算转换为使用延续的计算。

Answer 4

当我们提到延续时，我们指的是让我们继续计算结果的部分。

Continuation Monad 中的操作类似于一个不完整的函数，因此它正在等待另一个函数完成它。虽然，Continuation Monad 本身是一个有效的构造，可以用来完成另一个 Continuation Monad，这就是 Cont Monad 的绑定运算符 (>>=) 所做的。

在编写涉及 callCC 或 Call with Current Continuation 的代码时，您将当前的 Cont Monad 传递给另一个 Cont Monad，以便第二个可以使用它。例如，它可能会通过调用第一个 Cont Monad 来提前结束执行，然后循环可以从那里重复或分叉到不同的 Continuation Monad。

作为延续的部分与您使用的视角不同。在我个人看来，描述延续的最佳方式是与另一个构造相关。

因此，如果我们回到两个 Cont Monad 交互的示例，从第一个 Monad 的角度来看，延续是 (a -> r) -> r（因为这是第一个 Monad 的展开类型），从第二个 Monad 的角度来看延续是(a -> r)（因为这是a 替换(a -> r) 时第一个monad 的展开类型。