延续的正确术语

我一直在摸索延续最近，我对正确的术语感到困惑。Here http://www.haskellforall.com/2012/12/the-continuation-monad.html加布里埃尔·冈萨雷斯 说：

Haskell 延续具有以下类型：

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

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

The 维基百科 http://en.wikipedia.org/wiki/Continuation文章似乎支持这个想法，说

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

然而，here http://www.haskell.org/haskellwiki/MonadCont_under_the_hood作者说

延续是代表“剩余的计算要做”的函数。

但那只是(a->r)的一部分Cont类型。这与 Eugene Ching 所说的一致here http://www.codejury.com/continuations-in-haskell/:

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

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

我看过另一个教程（Brian Beckman 和 Erik Meijer），他们将整个过程（等待函数）称为可观察到的以及它完成所需的功能observer.

• 什么是延续、(a->r)->r东西或只是(a->r)东西（没有包装）？
• 可观察/观察者的措辞是否正确？
• 上面的引文真的是矛盾的吗？有共同的真理吗？

什么是延续， (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>

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

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 to 1 and 1 to 2.

这一切都很好，但是你如何处理分支呢？好吧，如果你仔细思考一下，你可能会想出一种方法来处理if以及执行精确次数的循环...但是一般情况呢while loops?

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. 利润定义新的语义函数”的指称语义方法经常出奇地有效。例如，让你的语义域形成一个lattice（思考，抽象解释）。你怎么得到这个？好吧，一种选择是获取域的幂集，并通过将函数解释为单例来注入该域。如果你内联这个 powerset 结构，你会得到一些可以建模的东西非决定论或者，在抽象解释的情况下，除了程序功能的确切确定性之外，有关程序的各种信息量。

随后还有其他各种工作。在这里，我跳过了许多伟大的论文，例如 lambda 论文……但是，也许最值得注意的是 Griffin 的里程碑式论文“控制的公式作为类型的概念”，该论文显示了连续传递风格与经典逻辑之间的联系。这里强调“延续”和“评估上下文”之间的联系

也就是说，E 表示在计算 N 后仍需要完成的其余计算。在评估序列中，上下文 E 被称为 N 在此时的延续（或控制上下文）。正如我们将在下面看到的，求值上下文的表示法允许对操作延续的运算符的操作语义进行简洁的规范（实际上，这是其预期用途[3,2,4,1]）。

明确“继续”是“只是a -> r bit"

这一切都是从语义的角度看待事物，并将延续视为函数。问题是，延续作为函数给你比像计划的 callCC 这样的东西更强大的功能。因此，关于延续的另一个观点是，它们是程序中内部化调用堆栈的变量。 Parigot 的想法是将连续变量作为一个单独的语法类别，从而产生“λμ-微积分：经典自然演绎的算法解释”中优雅的 lambda-mu 微积分。

可观察/观察者的措辞是否正确？

我认为埃里克·梅吉尔 (Eric Mejier) 使用的就是这样。它是学术 PL 中的非标准术语。

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

我们再看一下引用

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

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

Haskell 延续具有以下类型：

这有点奇怪。但是，请注意，在帖子的后面，加布里埃尔使用了更标准的语言，并且支持我对语言的使用。

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

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