正确的延续术语

Question

我最近一直在寻找延续,我对正确的术语感到困惑.Gabriel Gonzalez 在这里说:

Haskell延续具有以下类型:

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

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

在维基百科的文章,似乎说支持这个想法

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

但是,这里作者说

Continuations是表示"要执行的剩余计算"的函数.

但这只是(a->r)该Cont类型的一部分.这与Eugene Ching 在这里所说的一致:

计算(函数),需要一个连续函数才能完全评估.

我们将会看到很多这样的功能,因此,我们会给它一个更直观的名称.我们叫他们等待功能.

我已经看到了另一个教程(Brian Beckman和Erik Meijer),他们调用了整个事物(等待函数)observable以及它完成观察者所需的函数.

• 什么是延续,(a->r)->r东西或只是(a->r)东西(没有包装)？
• 措辞可观察/观察者是否正确？
• 以上的引用是否真的相互矛盾,是否有一个共同的事实？

Answer 1

什么是延续,(a-> r) - > r thingy或只是(a-> r)的东西(没有包装)？

我会说这a -> r一点是延续,而且(a -> r) -> r是"继续传递风格"或"是延续monad的类型.

我将继续对延续的历史进行长期的讨论,而这种历史并不是真正依赖于这个问题......所以请注意.

我相信,第一篇关于延续的论文是Strachey和Wadsworth的"延续:处理全跳的数学语义"(虽然这个概念已经是民间传说).这篇论文的想法是我认为非常重要的一个.命令式程序的早期语义试图将命令建模为状态变换器函数.例如,考虑以下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,并通过将您的函数解释为单例来注入.如果你内联这个powerset结构,你可以得到一些东西可以模拟非决定论,或者在抽象解释的情况下,可以获得关于程序的各种信息量,而不是确切地说明它的作用.

其他各种工作随之而来 在这里,我跳过了许多伟大的文章,例如lambda论文......但是,最值得注意的可能是格里芬的标志性文章"一个公式作为控制的控制概念",它表明了延续传递风格和经典逻辑之间的联系.这里强调了"延续"和"评价背景"之间的联系

也就是说,E表示在评估N之后剩余的计算.在评估序列中,上下文E被称为N的延续(或控制上下文).正如我们将在下面看到的那样,评估上下文的表示法允许对操作符合连续性的操作符的操作语义进行简明说明(实际上,这是它的预期用途[3,2,4,1]).

明确"延续"是"只是一a -> r点点"

这一切都从语义的角度来看待事物,并将延续视为函数.问题是,作为函数的延续比使用scheme的callCC之类的东西给你更多的功能.因此,关于continuation的另一个观点是它们是程序中的变量,它内化了调用堆栈.Parigot的想法是将连续变量作为一个单独的句法范畴,导致"λμ-Calculus:经典自然演绎的算法解释"中优雅的lambda-mu演算.

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

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

以上的引用是否真的相互矛盾,是否有一个共同的事实？

让我们再看一下引文

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

在我的解释中(我认为这是非常标准的),延续模型是一个程序下一步应该做什么.我认为维基百科与此一致.

Haskell延续具有以下类型:

这有点奇怪.但请注意,后来加布里埃尔使用的语言更为标准,并支持我使用语言.

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

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

Answer 2

通过阅读 Andrzej Filinski 的Declarative Continuations 和 Categorical Duality中有关延续的内容，我采用了以下术语和理解。

\n\n

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

\n\n

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

\n\n

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

\n\n

其中类型孔的上下文如下

\n\n

r    :: Type\ncont :: Int -> r\n-----------------\n_    :: r\n

\n\n

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

\n\n

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

\n\n

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

\n\n

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

\n\n\n\n

关于“可观察”

\n\n

我个人不喜欢“观察者”/“可观察”术语。在这个术语中我们可以写

\n\n

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

\n\n

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

\n\n

我认为关键在于以某种方式隐藏Cont隐喻背后的复杂性，以使其对“普通程序员”不那么可怕，但这只是为泄漏的行为增加了一层额外的隐喻。Cont并Yoneda Identity准确地解释类型是什么，而不需要修饰它。

\n