续体
在计算机科学中,续体(英語:continuation,也译作计算续体、续延、延續性),是实化计算机程序的控制状态的一种抽象表示。程式在運算過程中給定一個點,其「剩餘將要執行的部分」,即為「續體」。借助程式語言中的續體特性,程式設計師不但能模組化地自訂迴圈、break陳述句、continue陳述句等基本控制結構;此外還能以更加簡練的方式實現更加複雜的控制結構或計算模式,例如:異常處理、 生成器、協程、回溯、非确定性計算、概率编程[1]、反向传播算法、可微分编程等[2]。
概述
[编辑]對一段程式 1 * (2 + 3) - 4 而言,若當前正在計算 2 + 3,這部份則稱為可約表達式(英語:redex; reducible expression)[3];而其餘的部分 1 * - 4 即是續體。這裡的符號 被稱為「洞」,表示可約表達式之計算結果將要回填的地方,可視為佔位符。
[4]
續體的種類
[编辑]續體的概念在任何程式語言中都會出現,而不同的程式語言之間的差別在於是否提供構造或是算子,以供顯示地捕捉跟恢復續體。不同種類的算子,亦有相異的抽象程度與表達能力。
头等续体
[编辑]若能將捕捉到的續體實化作為一般的值儲存與傳遞,便會稱其為头等續體(英語:first-class continuations)。而當被捕捉的續體被呼叫時,程式的流程控制將會恢復到續體被捕捉時所在的地方。這賦予程式语言強大的执行順序控制能力。它可以跨越多個呼叫堆疊來返回結果,或者跳转到此前已经退出了的函数。可以认为其保存了程序的控制流程上下文,而需要注意的是這與进程映像不同,它不保存程序数据,只保存控制流程上下文。这经常采用“续体三明治”譬喻来说明:
你正站在冰箱前,想要做一个三明治。
你就把這個情況變成一个续体,放入口袋里。
接着,从冰箱里拿出火鸡肉和面包,並坐到桌案前,做了一个三明治。
你启用了口袋里的续体。
这时发现自己再次站到了冰箱之前,想要一个三明治。
幸运的是,在桌案上就有一个三明治,而用于做三明治的材料都没有了。你可以吃三明治了。[5]
在这个譬喻中,三明治是一部份程序数据,比如在分配堆上一个对象,并非去调用“制做三明治”例程并等它返回,这里调用“以当前续体制做三明治”例程,它创建一个三明治并在已脱离执行的续体所保存的地方继续执行。
多發及單發恢復
[编辑]能夠恢復多次的多發續體(英語:multi-shot continuations),其表達能力比僅能恢復一次的單發續體(英語:one-shot continuations)還要強。單發續體能夠直接表達迴圈、异常处理、迭代器、生成器、协程等控制結構,而多發續體不僅僅是具備單發續體的能力,此外還能用在非確定性、回溯法、布林可滿足性問題、反向傳播這些單發續體無法直接表達的問題。 [6] [7]
然而,多發恢復的續體在編譯器及執行期系統的實現面臨著工程上的挑戰。為了實現多發恢復的語意,通常需要以複製呼叫堆疊實現,這也為多發續延帶來了一些性能負擔。考慮到這個原因,部分程式語言僅提供單發恢復,例如OCaml的Effect[8];也有程式語言實現提供了單發化版本的控制算子,例如Chez Scheme提供了call/1cc。[9]而如何更高效地實現多發恢復,在近年來(2025)仍然是學者積極探討的問題。[10][11][12]
學界也探討了單發有界續體與協程的關係。有堆疊的非對稱式協程,例如Lua所提供的協程,可以對應到單發有界續體。[13][14][15][16]
历史
[编辑]Gerald J. Sussman和Guy L. Steele Jr.在1976年论文《Lambda:终极指令式》中,提及了John C. Reynolds在1972年介入去函数化变换的论文《高阶编程语言的定义性解释器》中采用了术语“续体”[17],并认定Alonzo Church在1941年著作《Lambda转换的演算》里[18],已经清晰的理解了“续体”的使用,这是用纯λ演算彻底完成所有事情即邱奇编码的唯一方式,并举出其中有序对定义所对应的Scheme表示为例[19]:
(define (cons m n)
(lambda (a) (a m n)))
(define (car a)
(a (lambda (b c) b)))
(define (cdr a)
(a (lambda (b c) c)))
John C. Reynolds在1993年的论文《续体的发现》中给出了发现续体的完整历史[20]。Reynolds认为续体的最早描述由Adriaan van Wijngaarden在1964年9月作出。van Wijngaarden在奥地利的維也納附近巴登召开的关于“形式语言描述语言”的IFIP工作会议上,在关于ALGOL 60预处理器的公式化的论文《语法和语义的递归定义》中[21],倡导将真正(proper)过程变换成续体传递风格,并附带消除标签和goto语句,但是他没有使用“续体”这个名字。
Steve Russell为他给IBM 704的LISP实现的一个用户,发明了续体来解决双重递归问题[22],但是他没有为其命名。
在指称语义领域的研究中,学者采用“续体”来规定一个控制构造对整个程序执行最终结果的贡献[23][24]。Christopher Strachey和Christopher P. Wadsworth在1974年技术专著《续体:处理完全跳转的数学语义》中给出了一个“小型续体语言”示例[25]。续体的概念在指称语义中定型于Joseph E. Stoy在1977年出版的著作《指称语义:Scott-Strachey编程语言理论途径》[26]。
Scheme语言的1975年最初版本提供了续体算子,即源自Maclisp的用于例外处理的命名catch/throw[27][28]。Steven S. Muchnick和Uwe F. Pleban在1980年论文《LISP与SCHEME的语义比较》中为Scheme语言介入了基于“续体语义”的指称语义规定[29][30]。
Daniel P. Friedman、Mitchell Wand和William Clinger基于按照Scheme语言的“续体语义”而编写的编译器[31][32],在1984年为Scheme介入了头等续体算子call-with-current-continuation(简写为call/cc)[33][34],随后还介入了其约束形式[35]。当前Scheme语言报告中的形式语义描述,沿袭了指称语义一系著作中所采用的概念和表示法[36][37][38]。
Bruce Duba等人在1991年将头等续体模块介入到了SML/NJ[39],CONT签名具有接口:val callcc : ('a cont -> 'a) -> 'a和val throw : 'a cont -> 'a -> 'b[40]。这里的'a cont是接受类型参数'a的续体类型,callcc f应用f到当前续体,如果f以实际参数x调用这个续体,则如同(callcc f)返回x作为结果。throw k a以实际参数a调用续体k;它在本质上将续体强制转变成为了函数,故而在每次续体调用之时重新介入了一个独立的类型参数'b。
续体传递风格
[编辑]续体的概念主要起源于计算模型研究,比如λ演算[41]、指称语义[25]和演员模型[42]。这些模型仰仗于编程者或语义工程师书写数学函数时采用“续体传递风格”(continuation-passing style,简写为CPS)[43]。续体传递风格(CPS)意味着编程中用到的每个函数,都接纳并于结束时应用一个表示有关于这个函数调用的余下计算的函数。表达式的最内部份必须首先求值,将表达式转换为续体传递风格等价者,比如Michael J. Fischer在1972年论文《Lambda演算基模》中所举的例子[41]:将变换成,具有将表达式“从内至外”翻转的效果,从而使求值次序以及控制流程变得更加明确。
下面是Standard ML中的高阶函数foldr和map的续体传递风格实现,和达成一个整数列表的合计函数的简单用例[44]:
fun foldr' f b l = let
fun cf ([], k) = k b
| cf (a :: r, k) = cf (r, fn x => k (f (a, x)))
in
cf (l, fn x => x)
end
fun map' f l = foldr' (fn (x, y) => (f x) :: y) [] l
fun sum l = foldr' (fn (x, y) => (x + y)) 0 l
所有CPS函数比如这里的cf,都接受一个额外的实际参数比如这里的k,它被称为续体。在CPS函数调用中的所有实际参数,必须要么是一个λ表达式比如这里fn x => k (f (a, x)),它将续体k应用于函数f的部份应用,要么是一个变量比如这里的l和r,而不能是更复杂的表达式。当CPS函数已经计算出来其结果值的时候,它通过以结果值作为实际参数调用续体函数来返回它,比如这里的cf ([], k) = k b,在计算的任何步骤中只要直接返回结果值就会终止整个计算。一个函数比如这里的foldr',要调用CPS函数比如这里的cf,就必须提供一个函数比如这里的fn x => x,用来接受它所调用的CPS函数的结果值。
对于输入[e1, e2, …, en],这里的sum函数等价于将函数复合(fn x => x)∘(fn x => e1 + x)∘(fn x => e2 + x)∘…∘(fn x => en + x),应用于0之上,它得到(e1 + (e2 + (… + (en + 0)…)))。此外,建立在惰性求值和柯里化之上的Haskell提供了函数复合算子。
下面是在Scheme语言中仅使用其基本形式的几个例子,对比了直接风格代码和对应的CPS代码,这里约定了将续体函数表示为名为k的形式参数:
直接风格 |
续体传递风格
|
|---|---|
(define (pythag x y)
(sqrt (+ (* x x) (* y y))))
|
(define (pythag& x y k)
(*& x x (lambda (a)
(*& y y (lambda (b)
(+& a b (lambda (c)
(sqrt& c k))))))))
|
(define (factorial n)
(if (= n 0)
1
(* n (factorial (- n 1)))))
|
(define (factorial& n k)
(=& n 0 (lambda (t)
(if t
(k 1)
(-& n 1 (lambda (n-1)
(factorial& n-1 (lambda (acc)
(*& n acc k)))))))))
|
(define (factorial n)
(define (loop n acc)
(if (= n 0)
acc
(loop (- n 1) (* n acc))))
(loop n 1))
|
(define (factorial& n k)
(define (loop& n acc k)
(=& n 0 (lambda (t)
(if t
(k acc)
(-& n 1 (lambda (n-1)
(*& n acc (lambda (n*acc)
(loop& n-1 n*acc k)))))))))
(loop& n 1 k))
|
对于函数式编程者而言,以续体传递风格表达代码使得在直接风格中隐含的一些事物显露出来:中介值或临时值都被指定了名字[45],实际参数求值的次序变为显见;随之而来,过程返回变成了对续体的调用,而尾调用变成将传递给这个调用者的续体不加修改的传递给被调用过程。
这里翻转条件表达式的方式类似于Smalltalk中遵循邱奇布尔值编码的条件执行控制结构:
result := a > b
ifTrue: [ 'greater' ]
ifFalse: [ 'less or equal' ]
注意在CPS版本的代码中,使用的函数原语(functional primitive)[46],比如这里的*&、+&、-&、=&和sqrt&,自身也是CPS而非直接风格,所以要使得上述例子在Scheme系统中运行,就必须写出这些函数原语的CPS版本,例如=&定义为:
(define (=& x y k)
(k (= x y)))
一般编程在写CPS函数之时,经常不采用CPS函数原语,比如将前面的阶乘函数写为:
(define (factorial& n k)
(if (= n 0)
(k 1)
(factorial&
(- n 1)
(lambda (acc) (k (* n acc))))))
要在REPL或直接风格函数中调用CPS函数,必须提供接受CPS函数计算结果的一个续体,比如恒等函数:
(pythag& 3 4 (lambda (x) x))
(factorial& 4 (lambda (x) x))
采用续体传递风格使函数式编程者能获得以任意方式操纵控制流程的表达能力,代价是手工维护控制续体通常是高度复杂的任务。终极解决方案是用Scheme写一组转换例程,将Scheme的直接风格表达式转换成CPS表达式[47],下面的例子仅将直接风格函数原语转换成CPS函数原语:
(define (cps-prim f)
(lambda args
(let ((r (reverse args)))
((car r) (apply f (reverse (cdr r)))))))
(define =& (cps-prim =))
(define *& (cps-prim *))
(define +& (cps-prim +))
(define -& (cps-prim -))
(define sqrt& (cps-prim sqrt))
这里的reverse函数反转LISP列表所用的单向链表,其首次应用将原来尾部元素反转到了首部,接着取出这个元素应用并再次应用reverse函数将余下诸元素反转成原来次序。apply函数的应用(apply f args),以args列表的诸元素作为实际参数调用f函数。
函数eval和通用函数apply[48],是传统元循环求值器的两大中心构件[49]。Daniel P. Friedman和Mitchell Wand,借鉴了John C. Reynolds的扩展了续体的解释器[50],在1984年论文《续体与协程》中,介入了基于CEK(控制、环境和续体)的元循环解释器[51],并在其著作《编程语言的本质》中发展出了“续体传递解释器”。
以当前续体调用
[编辑]非形式化描述
[编辑]在Scheme语言中,每当一个Scheme表达式被求值的时候,就会有一个续体想要这个表达式的结果。续体表示了这个计算的全部抑或缺省的未来。例如,如果这个表达式被求值于顶层,那么续体将接受这个结果,将它打印到屏幕上,提示下一次输入,进行求值,周而复始。多数时候续体包括用户代码所指定的动作,比如在接受这个结果的续体中,向它乘以存储在一个局部变量中的值再加上7,并将答案给予顶层续体来打印它。通常情况下编程者不用过多考虑那些隐藏在幕后的无处不在的续体。
Scheme语言为需要显式的处理续体的场合,提供了实化控制流程的算子call-with-current-continuation(简写为call/cc),call/cc将当前续体包装(package up)成为一个“逃脱过程”(escape procedure),即具有函数应用作为其唯一的运算,并把它作为实际参数传递给Scheme编程者所定义的函数。call/cc所包装的续体是头等对象,逃脱过程有着无限制的时效范围(extent)[52],可以被存储在变量或数据结构之中,它可以按需要多次调用。
在Scheme语言中,在call/cc的调用(call/cc f)中的函数f,接受包装了当前续体的逃脱过程作为其唯一实际参数。在后续执行中将逃脱过程应用于一个实际参数之时,此刻生效的续体被舍弃,转而使用创将这个逃脱过程之时生效的那个续体,控制流程将在这个续体被捕获的那一点上继续,而传递给这个逃脱过程的实际参数则变成这个call/cc调用的返回值。本章节的Scheme代码解说中出现的词语“当前续体”或“续体”,一般就是指在Scheme语言报告中描述的这个可操纵的包装它的“逃脱过程”。
归约语义
[编辑]callcc的形式语义,除了采用指称语义中进行CPS变换的方式来给出[53][54],也可以采用操作语义中小步语义的方式来定义,即使用在上下文之下的归约规则[55][56]:
这里的callcc捕获的当前续体是,其中是不被所绑定的变量。下面是这种callcc在类似OCaml的假设语言中的用例[57]:
2 * callcc (fun k -> 1 + (throw k 0));;
使用具有上下文C = 2 * [ ]的callcc规则,对整个程序也就是这个表达式进行归约:
⇒ 2 * (fun k -> 1 + (throw k 0)) (fun x -> 2 * x)
⇒ 2 * (1 + (throw (fun x -> 2 * x) 0))
接着使用具有上下文C = 2 * (1 + [ ])的throw规则,继续进行归约:
⇒ (fun x -> 2 * x) 0 ⇒ 2 * 0 ⇒ 0
Scheme编程语言示例
[编辑]立即返回
[编辑]下面的例子中,使用call/cc来模拟C风格语言中的return语句:
(define (f return)
(return 2)
3)
(f (lambda (x) x))
===> 3
(call/cc f)
===> 2
第一个演示,以恒等函数(lambda (x) x)作为实际参数调用函数f,函数f将绑定到形式参数return上的恒等函数应用于2,接着执行最后一个表达式3,从而函数f返回3。第二个演示,将call/cc应用于函数f,函数f将绑定到形式参数return上的续体应用于2,这在控制流程上等价于非局部跳转回到调用(call/cc f)的那一点上,将其代换为返回值2。
生成器
[编辑]下面是生成器的实现代码:
(define (generator lst)
(define iterator (lambda (yield)
(for-each (lambda (item)
(set! yield (call/cc (lambda (resume)
(set! iterator resume)
(yield item)))))
lst)
(yield 'stop-iteration)))
(lambda () (call/cc iterator)))
在这里于生成器之中定义它所生成的迭代器函数iterator,和随后定义函数generate-digit的时候,采用了函数定义的不加语法糖的原始形式。call/cc在这里被用到了两处:一处是(call/cc iterator),它以当前取用遍历返回值续体调用迭代器;另一处是(call/cc (lambda (resume) ……)),它在迭代器遍历目标列表之时捕获当前位置,用于下次重入迭代器之时于此处恢复执行。下面是上述代码的简单用例:
(define generate-digit
(generator '(0 1 2)))
(define (display-two-digits)
(display (generate-digit)) (newline)
(display (generate-digit)) (newline))
(display-two-digits) ;; 分两行打印 0 和 1
(display-two-digits) ;; 分两行打印 2 和 stop-iteration
这里定义的函数generate-digit,是将函数generator应用于聚集(aggregate)即这里的列表'(0 1 2)之上,而得到的闭包(lambda () (call/cc iterator))。
在第一次执行(generate-digit)之时,执行(call/cc iterator),进而执行(iterator yield),它将取用遍历返回值续体绑定到形式参数yield之上;然后开始遍历列表的元素进行迭代的(for-each (lambda (item) ……) lst),在求值(set! yield (……))的第二个实际参数之时,进行每一次迭代步骤(call/cc (lambda (resume) ……)),其中的(set! iterator resume),将绑定到变量resume上的当前续体,重新绑定到函数名字iterator之上用于以后恢复执行,最后执行暂停表达式(yield item)返回当前列表项目。
在下一次执行(generate-digit)之时,(call/cc iterator)将iterator所绑定的续体应用于当前取用遍历返回值续体之上,从而在上次迭代的(set! yield (call/cc ……))之处恢复执行,这个函数的实际参数求值完毕,它的执行将新传入的取用遍历返回值续体绑定到变量yield上,此后继续这一次的迭代步骤。在遍历了列表的元素之后迭代结束,最终执行(yield 'stop-iteration),返回一个约定的文字常量。
协程
[编辑]call/cc还可以表达其他复杂的原始运算比如协程[58]。下面的代码使用续体达成协程即协作式多任务的用户级线程:
(define *ready-list* '())
(define (yield)
(call/cc (lambda (reenter)
(let ((cont (car *ready-list*)))
(set! *ready-list* (append (cdr *ready-list*) (list reenter)))
(cont #f)))))
(define (fork fn . args)
(call/cc (lambda (abort)
(set! *ready-list* (cons abort *ready-list*))
(yield)
(apply fn args)
(let ((cont (car *ready-list*)))
(set! *ready-list* (cdr *ready-list*))
(cont #f)))))
(define (schedule)
(let loop ()
(if (not (null? *ready-list*)) (begin
(yield)
(loop)))))
这里的全局变量*ready-list*是就绪线程列表,它存储处于脱离(detached)状态的就绪线程的重入续体;在选择重入线程的时候,将就绪线程列表头部的续体从列表中取出,并应用它以重入对应线程。退让过程yield,捕获对应于调用者的当前续体,将其追加到就绪线程列表的尾部,取出并应用就绪线程列表头部的续体而使本线程脱离运行(operating)。
分叉过程fork,接受一个函数fn和相应的参数列表args,它首先捕获自身的当前续体并将其添加到就绪线程列表的头部;然后调用退让过程yield,从而创建了一个用来创建工人(worker)线程的线程,接着取出并应用就绪线程列表头部的续体而使本线程脱离运行;由于分叉过程自身的续体已经添加到了就绪线程列表头部,重入它而随即结束分叉过程的这次调用。当重入这个创建工人线程的线程之时,调用函数fn,预期这个函数在自身之中调用退让过程yield,从而创建重入函数fn内部的工人线程。当工人线程最终并未调用退让过程而从函数fn直接退出回到分叉过程之时,必须接着以取出并应用就绪线程列表头部的续体的方式来结束这个工人线程,因为对分叉过程的调用早已结束。
调度过程schedule,持续检测就绪线程列表,只要有任何其他线程等待就调用退让过程yield,取出并应用就绪线程列表头部的续体而使本线程脱离运行,最终在无就绪者等待之时结束。调度过程在每一轮并发运行循环中只运行一次。调度过程在所有分叉过程之后调用,它起到的根本作用是充当会合点,即并发运行的多个线程中的最终剩下的唯一线程。下面是上述代码的简单用例:
(import (srfi 28))
(define (echo-string-n-times str n)
(let loop ((i 0))
(if (< i n) (begin
(display (format "~a ~a~%" str i))
(yield)
(loop (+ i 1))))))
(define (main)
(fork echo-string-n-times "This is AAA" 3)
(fork echo-string-n-times "Hello from BBB" 2)
(schedule))
(main)
其输出为:
This is AAA 0
Hello from BBB 0
This is AAA 1
Hello from BBB 1
This is AAA 2
在这个用例的两个分叉过程中,前面的分叉过程先执行并且后结束,如果不介入调度过程转而完全由工人线程自行调度,会合于此处将导致非预期的情况出现,即除非就此退出这个进程,在其后的分叉过程会再次执行。
最后演示对上述协程代码的一种变化:将退让过程yield改成具有返回值,调用了退让过程的分叉过程fork也相应更改;将调度过程schedule改为采用弹跳床策略,它与前面代码的区别在于将调度过程自身的续体添加到就绪线程列表的头部;并为调度过程增加了一个函数参数fn,用这个函数来处理工人线程的返回值。这种调度过程也可以改名为分派过程dispatch:
(define *ready-list* '())
(define (yield x)
(call/cc (lambda (reenter)
(let ((cont (car *ready-list*)))
(set! *ready-list* (append (cdr *ready-list*) (list reenter)))
(cont x)))))
(define (fork fn . args)
(call/cc (lambda (abort)
(set! *ready-list* (cons abort *ready-list*))
(yield #f)
(apply fn args)
(let ((cont (car *ready-list*)))
(set! *ready-list* (cdr *ready-list*))
(cont #f)))))
(define (schedule fn)
(let loop ()
(if (not (null? *ready-list*)) (begin
(fn (call/cc (lambda (return)
(let ((cont (car *ready-list*)))
(set! *ready-list* (cons return (cdr *ready-list*)))
(cont #f)))))
(loop)))))
这种协程也称为“半协程”或“生成器”,它与前面例子中同名的生成器机制各有用途。下面是其用例:
(import (srfi 28))
(define (echo-string-n-times str n)
(let loop ((i 0))
(if (< i n) (begin
(yield (format "~a ~a~%" str i))
(loop (+ i 1))))))
(define (main)
(fork echo-string-n-times "This is AAA" 3)
(fork echo-string-n-times "Hello from BBB" 2)
(schedule display))
(main)
编程语言的直接支持
[编辑]除了Scheme、Racket和新泽西Standard ML之外,一些编程语言直接支持头等续体比如:
- Common Lisp:cl-cont[59],还可以使用定制宏
参见
[编辑]引用与注释
[编辑]- ^ https://link.springer.com/chapter/10.1007/978-3-642-03034-5_17
- ^ https://dl.acm.org/doi/10.5555/3327546.3327682
- ^ Klop, J. W. Term Rewriting Systems (PDF). Papers by Nachum Dershowitz and students. Tel Aviv University: 12. [14 August 2021]. (原始内容存档 (PDF)于15 August 2021).
- ^ Kenichi Asai & Oleg Kiselyov. Introduction to programming with shift and reset. 2011.
- ^ Palmer, Luke. undo()? ("continuation sandwich" example). perl.perl6.language (newsgroup). June 29, 2004 [2009-10-04]. (原始内容存档于2013-06-06).
- ^ Carl Bruggeman; Oscar Waddell; R. Kent Dybvig. Representing control in the presence of one-shot continuations. Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’96). Association for Computing Machinery: 99–107. 1996 [2025-11-16]. doi:10.1145/249069.231395.
- ^ Tcl Development Team. TIP #328: Coroutines. [2025-11-16] (英语).
- ^ KC Sivaramakrishnan; Stephen Dolan; Leo White; Tom Kelly; Sadiq Jaffer; Anil Madhavapeddy. Retrofitting Effect Handlers onto OCaml (PDF). Thu, 1 Apr 2021 [2025-11-16]. (原始内容存档于2025-11-16) (英语).
- ^ Chapter 6. Control Structures. Chez Scheme Version 10 User's Guide. Cisco Systems, Inc. 2025-10 [2025-11-16] (英语).
- ^ C. N. Pham; Martin Odersky. Stack-Copying Delimited Continuations for Scala Native. Proceedings of the 19th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems (ICOOOLPS ’24). Association for Computing Machinery. 2024 [2025-11-16]. doi:10.1145/3679005.3685979.
- ^ Cong Ma; Zhaoyi Ge; Max Jung; Yizhou Zhang. Zero-Overhead Lexical Effect Handlers. Proceedings of the ACM on Programming Languages (Association for Computing Machinery). 2025, 9 (OOPSLA2) [2025-11-16]. doi:10.1145/3763177.
- ^ Serkan Muhcu; Philipp Schuster; Michel Steuwer; Jonathan Immanuel Brachthäuser. Multiple Resumptions and Local Mutable State, Directly. Proceedings of the International Conference on Functional Programming (ICFP). Association for Computing Machinery. 2025 [2025-11-16]. doi:10.1145/3747529.
- ^ Ana Lúcia de Moura; Roberto Ierusalimschy. Revisiting Coroutines. ACM Transactions on Programming Languages and Systems. 2009, 31 (2): 6:1–6:31 [2025-11-16]. doi:10.1145/1462166.1462167.
- ^ R. P. James; Amr Sabry. Yield: Mainstream Delimited Continuations (PDF). Proceedings of the First International Workshop on the Theory and Practice of Delimited Continuations (TPDC ’11). 2011 [2025-11-16].
- ^ Kentaro Kobayashi; Yukiyoshi Kameyama. Expressive Power of One-Shot Control Operators and Coroutines. arXiv preprint. 2025,. arXiv:2509.11901 [2025-11-16] (英语).
- ^ Satoru Kawahara; Yukiyoshi Kameyama. One-shot Algebraic Effects as Coroutines (PDF). Trends in Functional Programming – 20th International Symposium, TFP 2020, Revised Selected Papers. Springer: ?–?. 2022 [2025-11-16]. ISBN 978-3-030-57760-5. doi:10.1007/978-3-030-57761-2_8.
- ^
John C. Reynolds. Definitional Interpreters for Higher-Order Programming Languages. 1972 [2024-02-24]. (原始内容存档于2024-02-24).
Now suppose we define an expression to be serious if there is any possibility that its evaluation might not terminate. Then a sufficient condition for order-of-application independence is that a program should contain no serious operands or declaring expressions. ……
Nevertheless, there is a method for transforming an arbitrary program into one which meets our apparently restrictive condition. …… Basically, one replaces each serious function fold (except the main program) by a new serious function fnew which accepts an additional argument called a continuation. The continuation will be a function itself, and fnew is expected to compute the same result as fold, apply the continuation to this result, and then return the result of the continuation, i.e.,
fnew(x1, …, xn, c) = c(fold(x1, …, xn)).
This introduction of continuations provides an additional "degree of freedom" which can be used to meet our condition for order-of-evaluation independence. Essentially, instead of performing further actions after a serious function has returned, one imbeds the further actions in the continuation which is passed to the serious function. - ^ Alonzo Church. The Calculi of Lambda-Conversion. Annals of Mathematics studies, no. 6. Lithoprinted. Princeton University Press, Princeton. 1941 [2021-09-24]. (原始内容存档于2022-05-19).
- ^
Gerald J. Sussman, Guy L. Steele Jr. Lambda: The Ultimate Imperative. 1976 [2021-11-11]. (原始内容存档于2022-04-10). “ Reynolds uses the term "continuation" in [Reynolds 72]. Church clearly understood the use of continuations; it is the only way to get anything accomplished at all in pure lambda calculus! For example, examine his definition of ordered pairs and triads on page 30 of [Church 41]. In SCHEME notation. this is:
[M, N]means(LAMBDA (A) (A M N))
21means(LAMBDA (A) (A (LAMBDA (B C) B)))
22means(LAMBDA (A) (A (LAMBDA (B C) C)))
where21e.g. selects the first element of a pair. (Note that these functions are isomorphic toCONS,CAR, andCDR!) ” - ^ Reynolds 1993
- ^ Adriaan van Wijngaarden. Recursive Definition of Syntax and Semantics (PDF). 1966 [2024-02-24]. (原始内容存档 (PDF)于2024-02-24).
- ^ IT History Society — Mr. Steve (Slug) Russell. [2024-02-24]. (原始内容存档于2024-02-24).
- ^
R. D. Tennent. The denotational semantics of programming languages. Communications of the ACM, Volume 19, Issue 8 Pages 437 - 453. 1976.
We may describe the interpretations to be considered here as prophetic since they must specify not merely the local result or effect of a construct, but its contribution to the final result of a complete program or process execution. ……
Now, consider interpreting an expression relative to a function which specifies what is to be done with the value of that expression if there is no escape. This function is called a continuation and in this context must be applicable to the value of an expression while returning an "answer"; i.e. the prophesized result of the whole program in which the expression is embedded. In a purely applicative language the answer must be an expressible value but for the sake of clarity and to allow for the generalizations that will soon be described, we introduce a generic domainAof answers which include expressible values and also other possible results such as error messages, intermediate output, and so on. Then we may construct the domain:
κ:K = E → Aexpression continuations
and the prophetic interpretation function'has functionality:
' : Exp → U → K → A
so that'⟦E⟧ρκis always the final answer yielded by executing the complete program of whichEis a part. ……
An escape is modeled by ignoring the "normal" continuation and applying instead an "abnormal" continuation that models the computational future from the proper exit point. ……
It is also easy to account for "error stops" ……
The use of continuations and prophetic interpretations is also possible when the object language required a store component in its semantic model. - ^
Michael J. C. Gordon. The denotational description of programming languages - an introduction. Springer-Verlag, Berlin, Heidelberg. 1979.
In a continuation semantics we make the denotations of constructs depend on the 'rest of the program' — or continuation — following them. The intuitive idea is that each construct decides for itself where to pass its result. Usually it will pass it to the continuation corresponding to the 'code' textually following it in the program — the normal continuation — but in some cases this will be ignored and the result passed to some other 'abnormal' continuation. For example:
(i) When an error occurs the normal continuation is ignored and control passes to a continuation corresponding to an error stop.
(ii) When a jump occurs the normal continuation is ignored and control passes to a continuation corresponding to the rest of the program following the label jumped to. - ^ 25.0 25.1
Christopher Strachey, Christopher P. Wadsworth. Continuations: a Mathematical semantics for handling full jumps (PDF). Technical Monograph PRG-11. Oxford University Computing Laboratory. Reprinted in Higher Order and Symbolic Computation, 13(1/2):135—152, 2000. January 1974.
In the semantics given in [13] the value of a command is a function which transforms the store, so that, in symbolic terms
⟦γ⟧(ρ) = θ
where is the semantic function mapping commands to their meanings,γis a command,ρthe environment which gives the denotations associated with the identifiers inγandθis a store transformation, i.e.
θ ∈ C = [S → S]
whereSis the domain of machine states (or stores). We use the double brackets⟦ ⟧as an aid to the eye to separate the program textγfrom the value domain expressions which form the rest of the equation. ……
We must define, instead, a semantic function which yields, for every commandγ, in a program, the state transformation which would be produced from there to the end of the program. We shall use letter for this function to distinguish it from the of [13]. In order to deal with the effect of the program followingγ, we need to supply an extra argument,θ, which is the state transformation corresponding to this part of the program. Ifγis jump-free, we shall then have for the program includingγ
⟦γ⟧(ρ)(θ) = θ∘⟦γ⟧(ρ)
which can be interpreted as saying that the state transformation for the whole program, starting from the commandγ, is that obtained by first performing the state transformation specified byγ(i.e.⟦γ⟧(ρ)) and then that specified by the rest of the program (i.e.θ). The argumentθis called a continuation (strictly a command continuation) and is of typeC = [S → S]. The semantic function thus has the functionality
: [Cmd → [Env → [C → [S → S]]]].
Suppose we have a state σ0; a continuationθwould mean that the final state of the machine at the end of the program would be
σ1' = θ(σ0).
If we now want to find the effect of performing the commandγwithθas its continuation, we should use the state transformationθ' = ⟦γ⟧(ρ)(θ)so that the final state would be:
σ1' = ⟦γ⟧(ρ)(θ)(σ0).
This sort of expression may be unfamiliar to some readers as it involves the use of higher order functions — that is, functions whose arguments and results are also functions. …… In this minimally bracketed form, we should write
σ1' = ⟦γ⟧ρθσ0
(note that we shall always retain the text brackets ⟦ ⟧). - ^
Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge. 1977.
The use of continuations was developed independently by Christopher Wadsworth and Lockwood Morris; it is inspired by the "tail functions" of Mazurkiewicz [29]. Mike Fischer [12] has also used essentially the same technique, but for a rather different purpose. The paper by Strachey and Wadsworth [59] gives a good exposition.
Our formalism has now become more curried than ever. Instead of⟦Γ⟧ρθσwe could have chosen to write
C⟨Γ, ρ, θ, σ⟩.
We could regard this quadruple as the state of some interpreter which goes through state transitions, and write
C⟨Γ, ρ, θ, σ⟩ = C⟨Γ', ρ', θ', σ'⟩
and so on. This would make it resemble the sharing machine of Peter Landin [24] (whereΓis the Control part,ρthe Environment,σthe sharing relation, andθa mixture of the Stack and the Dump with much housekeeping detail omitted). But we prefer the curried approach, partly for conciseness, but also because each successive stage of the currying has its own abstract meaning. ……
So far we have mentioned only the continuations of commands; we must now deal with expressions. The continuation of a command inherits only a state from its preceding activity; but the continuation of an expression inherits a result as well as a state. A command continuation was of type[S→S] = C; an expression continuation could therefore be of type[[E×S]→S], but we prefer to curry it:
κ ∈ K = [E→[S→S]] = [E→C]. - ^
Gerald J. Sussman, Guy L. Steele Jr..
Scheme: An Interpreter for Extended Lambda Calculus. 维基文库. 1975 (英文). CATCH- This is the "escape operator" which gives the user a handle on the control structure of the interpreter. The expression:
(CATCH <identifier> <expression>)
evaluates<expression>in an environment where<identifier>is bound to a continuation which is "just about to return from theCATCH"; that is, if the continuation is called as a function of one argument, then control proceeds as if theCATCHexpression had returned with the supplied (evaluated) argument as its value. ……
As another example, we can define aTHROWfunction, which may then be used withCATCHmuch as they are in LISP:
(DEFINE THROW (LAMBDA (TAG RESULT) (TAG RESULT))) - ^
William Clinger, Daniel P. Friedman, Mitchell Wand. A scheme for a higher-level semantic algebra. 1985.
Note that we have made "
call/cc" a constant. Thus theCATCHoperator in Scheme, which does both binding and catching, would be translated as
⟦catch <id> <exp>⟧ = (apply call/cc(abs<id>⟦<exp>⟧)) - ^
Guy L. Steele Jr. Debunking the 'Expensive Procedure Call' Myth, or, Procedure Call Implementations Considered Harmful, or, Lambda: The Ultimate GOTO. 1977 [2021-11-07]. (原始内容存档于2022-05-09).
In general, procedure calls may be usefully thought of as
GOTOstatements which also pass parameters, and can be uniformly encoded asJUMPinstructions. This is a simple, universal technique, to be contrasted with the more powerful recursion-removal techniques such as those in [Dar76]. Our approach results in all tail-recursive procedure calls being compiled as iterative code, almost without even trying, for it is more a matter of the code generation strategy than of a specific attempt to remove recursions. - ^
Steven S. Muchnick, Uwe F. Pleban. A semantic comparison of LISP and SCHEME. LFP '80: Proceedings of the 1980 ACM conference on LISP and functional programming. 1980.
The main data objects manipulated by the semantics are an environment
ρ(which models theALIST), a storeσ(which models the heap) and a locationα(which models the current point of control in the program stored in the heap). ……
A SCHEME environmentρ∈Uis a mapping from identifiers to locations or the special symbol "?" indicating an unbound identifier. A location in the store, in turn, may contain any expression value — an S-expression value, a function or an escape object. — along with a tag indicating whether the location is allocated or not.
Continuationsθ∈Cmap the current store configuration to the result (or answer) of the dynamic remainder of the program. Expression and declaration continuations describe the effect of evaluating an expression or elaborating a declaration, followed by executing the remainder of the program. ……
We shall discuss only two more of the equations, namely those forCATCHandTHROW, which are
⟦(CATCH id exp)⟧ =
λρ.λκ.λσ. tie(λ⟨α⟩σ'.
⟦exp⟧(ρ[α/id])κ(update α κ σ'))1σ
and
⟦(THROW id exp)⟧ =
λρ.λκ. ρ⟦id⟧ ≠ ? → ⟦exp⟧ρ{λε.λσ'.
β⋿K → (β|K)εσ', wrong σ'}, wrong
whereβ = map(ρ⟦id⟧)σ'CATCHallocates a locationαfor the variableidand stored the continuationκin the locationαin storeσ'; then it causesexpto be evaluated with the resulting environment and store.THROWcauses the identifieridto be look up in the environment and store; if its value is an escape objectβ⋿K, then the expressionexpis evaluated and passed to to escape object (which is a continuation); otherwise the error continuation is applied. From the semantic equations it is apparent that escape objects are storable. The possibility of assigning an escape object to a variable whose scope extends beyond theCATCHwhich created the object can be exploited to "return from theCATCH" more than once. Just as an upwardFUNARGin LISP may necessitate the retention of binding frames, so aCATCHmay cause the retention of control frames. Thus the control component of a program may be a tree instead of a stack. - ^
Mitchell Wand. Deriving Target Code as a Representation of Continuation Semantics. ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 4, Issue 3, Pages 496 - 517. 1982.
We have presented a method for deriving compilers and abstract machines from the continuation semantics for a language. The technique involves choosing special-purpose combinators to eliminate λ-variables in the semantics and discovering standard forms for the resulting terms to obtain target code which represents the meaning of the source code. The abstract machine's job is to interpret these representations as functions.
- ^
William Clinger. The scheme 311 compiler an exercise in denotational semantics. 1984.
For programming languages the highest level of abstraction speaks of environments, continuations, stores, expressed values, and so on. The next highest level of abstraction begins to speak of implementation concepts. ……
For Scheme 311 this level introduces code segments as well. Code segments are taken to be values in the domain
P = E → E* → UR → K → C
whereURis the domain of run-time environments [Figure 2]. ……
Continuations can now be represented in terms of code segments, sequences of expressed values, run-time environments, and continuations. The general form of a continuation in this new representation is
λε. πεε*ρRκ
whereπis a code segment. ……
This algorithm has been used in several implementations including Scheme 311 Versions 2 through 4 [5], Scheme 84 [6], and a byte code implementation for the Motorola 68000. - ^
Friedman, Daniel; Haynes, Christopher; Kohlbecker, Eugene. Programming with Continuations. 1984.
In Scheme 84 [1] the call-with-current-continuation expression described by the form
(call/cc (lambda (k) Exp))causes the expressionExpto be evaluated in an environment wherekis bound to the continuation of the entirecall/ccexpression. …… The control and environment information associated with continuations is recorded in storage that is dynamically allocated. It is reclaimed only when all references to the continuation have been abandoned. - ^
William Clinger, Daniel P. Friedman, Mitchell Wand. A scheme for a higher-level semantic algebra. 1985.
In order to model the behavior of a programming language, we must not only provide some domains, but also some operations on those domains. By doing this, we make the domains into an algebra. ……The starting point for this investigation was the programming language Scheme. ……The result is a Scheme-like semantic algebra. ……
Table 1 presents our domains and some useful functions on them. ……
K = Env × [V → C]Continuations ……
pair,lson,rson— primitives for pairings ……
send = λκv.rson κv……
The other unusual feature of the domains is the treatment of continuations. A continuation consists not only the usual[V → C](the "sequel") but also an environment, which is intended to keep fluid variables. …… In order to hide the internal structure of these continuations as much as possible, we introduce a number of help functions. We use "send" to supply a value to the sequel inside a continuation. ……
Tables 3 presents the meanings of the operations on the domains. ……
call/cc = const(λvκ1.v(λvκ2.send κ1v)κ1)……
Further control flow capabilities are provided by the "call/cc" operator. "call/cc" take as an argument an abstraction (either static or fluid) and passes to the abstraction another abstraction, which takes the role of a continuation. When this "continuation abstraction" is applied, it sends its argument to the continuation of the "call/cc". - ^
Daniel P. Friedman, Christopher T. Haynes. Constraining control. POPL '85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages: 245 - 254. 1985.
We now provide a sequence of examples that illustrate approaches to constraining continuation. …… First we demonstrate a version of
call/cc, referred to ascall/cc-one-shot, which delivers explicit continuations that may only be invoked once. ……
We now wish to enforce the constraint that when a continuation is invoked, neither it, nor any of its descendents may be invoked a second time. This suffices to ensure that control information may be stack rather than heap allocated. ……
In some contexts it may be necessary to restrict the range of control jumps to some dynamic context, which we refer to as a domain. - ^
Dana Scott, Christopher Strachey. Toward a mathematical semantics for computer languages. In Proc. of the Symposium on Computers and Automata, Polytechnic Institute of Brooklyn. Also as Technical Monograph PRG-6, Oxford University Computing Laboratory, Programming Research Group. 1971.
An identifier will be assigned an element either from
Cor fromVdepending on how it is to be used. This means that now we shall have to set:
Env = [Id → C + V].
Strictly speakingC,VandC + Vare all different domains even though the first two are matched with parts ofC + V. We shall require a more precise notation to indicate this matching. A completely precise symbolism would be cumbersome, so we write
(θ in [C + V])and(β in [C + V]),
whereθ ∈ Candβ ∈ Vto indicate the corresponding elements ofC + V. Forδ ∈ C + Vwe write
δ|Candδ|V,
to indicate the "projection" fromC + Vonto its two parts. - ^
Robert Milne, Christopher Strachey. Theory of Programming Language Semantics. Part A. Halsted Press, Div. of John Wiley & Sons, Inc. 605 Third Ave. New York, NY, United States. 1976.
If
εis a truth value whileω0∈Wandω1∈Ware members of a domain calledW, the conditional termε → ω0, ω1signifies a certain member ofW; it take the valueω0whenεis true and the valueω1whenεis false. ……
When{Wn|n≥0}is a sequence of domains, for everyn≥1we letW0×…×Wnbe a certain domain, a typical member of which might be written as⟨ω0,…,ωn⟩(whereωm∈Wmwhenn≥m≥0)…… When handling products we need not only the brackets⟨and⟩which were introduced above but also three operators,↓,†and§, which serve respectively to extract components from lists, to chop bits off lists and to concatenate lists. …… In the case of sums, for everyω∈W0+…+Wnand for everymhavingn≥m≥0we writeω⋿Wmfor test which indicates whetherωlies in the summandWmand we writeω|Wmfor the member ofWmwhich tallies withω……
As we indicated in 1.1.1, a member of a syntactic domain supplied to a function as an argument will generally be enclosed by special brackets, so whenIis an identifier belonging toIdeand whenρis an environment belonging toIde→Dwe shall writeρ⟦I⟧will be the value demoted byIinρ. …… WhenIis an identifier,ρis a environment andδis a typical member of the domain of denoted values,D, we shall letρ[δ/I]signify an environment derived formρby makeIdenoteδinstead ofρ⟦I⟧; in terms of the conditional expression introduced in 1.1.2 we can write
ρ[δ/I] = λI'. (I=I') → δ, ρ⟦I'⟧,
so that wheneverI'is an identifier(ρ[δ/I])⟦I'⟧isδifI'isIand(ρ[δ/I])⟦I'⟧isρ⟦I'⟧ifI'is notI. ……
Though frequently we shall not distinguishωmregarded as an element ofW0+…+Wnfromωmregarded as an element ofWm, whenωmis most naturally viewed in the first of these lights we shall sometimes writeωm|Wmfor then corresponding element ofWm. We shall not bother to mark out the element ofW0+…+Wncorresponding with any given entity,ωm, inWm, but will simply designate it byωm. ……
Whenωis used to denote a typical member ofW,ω*will be used to denote a typical member ofW*; the length of anyω*∈W*,#ω*, will be⊥ifω*=⊥,⊤ifω*=⊤,0ifω*=⟨⟩, andn+1ifω*=⟨ω0,…,ωn⟩for somen≥0. - ^
Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge. 1977.
6.35 Notation. If
D = D1+D2+…+Dnandxi∈Di(1≤i≤n), then(xi in D)denotes the corresponding element of the sum latticeD.
Ifx∈Dthenx|Didemotes the following element ofDi:
ifx ≡ ⊥Dthen(x|Di) ≡ ⊥Di;
ifx ≡ ⊤Dthen(x|Di) ≡ ⊤Di;
ifxcorresponds to an elementyof theDithen(x|Di) ≡ y; otherwise (ifxcorresponds to an element of some other summand lattice),(x|Di) ≡ ⊥Di.……
It must be admitted that the notation 6.35, and even the machinery underlying it, is not entirely satisfactory. It rapidly becomes exceedingly tedious to be continually distinguishing between a value considered as an element of a sum domain and then and the same value considered as an element of a component lattice. Some times this lead workers to omit entirely these operations ("injection" into a sum lattice and "projection" into a component space), on the grounds that they may be deduced from the context if required. Such informality in turn leads to difficulties for people developing programs which accept denotational semantic definitions as input and process them in some way automatically (for example, Mosses [37]). - ^ Bruce Duba, Robert Harper, David MacQueen. Typing first-class continuations in ML (PDF). 1991 [2021-10-11]. (原始内容存档 (PDF)于2022-01-29).
- ^ Standard ML of New Jersey — The CONT signature. 1998.
- ^ 41.0 41.1
Michael J. Fischer. Lambda Calculus Schemata. In Proceedings of an ACM Conference on Proving Assertions about Programs (1972) 104–109. 1972.
Thus, in a safe schema, we prohibit the value returned by an application or conditional from being passed on to another function as an argument. It follows that such a value can never be evaluated and must eventually propagate to the top level to become the final result of the whole evaluation. ……
Thus, our idea is to modify the schema so that for any sub-lambda-functiong, instead ofgpassing its result back to the caller, the caller is passed togas an additional functional argument,gthen applies the new argument to the result it used to return, thereby avoiding the necessity of returning immediately.
For example, given(f (g (h a))), we could turn it inside-out to get(h (λx.(g (λy.(f y)) x)) a), assuming thathandghad been modified accordingly. - ^
Carl Hewitt, Peter Bishop, Irene Greif, Brian Smith, Todd Matson, Richard Steiger. Actor induction and meta-evaluation. 1973 [2022-11-15]. (原始内容存档于2022-11-15).
Conceptually at least a new actor is created every time a message is sent. Consider sending to a target T a message M and a continuation C.
- ^ Gerald J. Sussman, Guy L. Steele Jr.
Scheme: An Interpreter for Extended Lambda Calculus. 维基文库. 1975 (英文). It is always possible, ……to perform any calculation in this way: rather than reducing to its value, it reduces to an application of a continuation to its value (cf. [Fischer]). That is, in this continuation-passing programming style, a function always "returns" its result by "sending" it to another function.
- ^ CS312. Continuations. Cornell University. 2006.
CS3110. Continuations and CPS Conversion. Cornell University. 2014.
Brandon Wu. SML Help — Continuation Passing Style. 2022. - ^ Guy L. Steele Jr. LAMBDA: The Ultimate Declarative. 1976 [2021-11-10]. (原始内容存档于2022-04-09).
Environment operators also take various forms. The most common are assignment to local variables and bind of arguments to functions, but there are others, such as pattern-matching operators (as in ……). It is usual to think of these operators as altering the contents of a named location, or of causing the value associated with a name to be changed.
In understanding the action of an environment operator it may be more fruitful to take a different point of view, which is that the value involved is given a new (additional) name. if the name had previously been used to denote another quantity, then that former use is shadowed; but this is not necessarily an essential property of an environment operator, for we can often use alpha-conversion ("uniquization" of variable names) to avoid such shadowing. It s not the names which are important to the computation, but rather the quantities; hence it is appropriate to focus on quantities and think of them as having one or more names over time, rather than thinking of a name as having one or more values over time. ……
Thus theLAMBDAnot only assigns names, but determines the extent of their significance (their scope). Note an interesting symmetry here: control constructs determine constraints in time (sequencing) in a program, while environment operators determine constraints in space (textual extent, or scope). - ^ Gerald J. Sussman, Guy L. Steele Jr. Lambda: The Ultimate Imperative. 1976 [2021-11-11]. (原始内容存档于2022-04-10).
We can redefine other functions to take continuations in the same way. For example, suppose we had arithmetic primitives which took continuations; to prevent confusion, call the version of "+" which take a continuation "++", etc.
Guy L. Steele Jr. LAMBDA: The Ultimate Declarative. 1976 [2021-11-10]. (原始内容存档于2022-04-09).Let us define a convenient set of continuation-passing primitives. Following the convention used in [Steele 76], we will let the last argument(s) to such a primitive be the continuation(s), where a continuation is simply a "function" of values delivered by the primitive.
- ^ Guy L. Steele Jr. LAMBDA: The Ultimate Declarative. 1976 [2021-11-10]. (原始内容存档于2022-04-09).
Here we present a set of functions, written in SCHEME, which convert a SCHEME expression from functional style to pure continuation-passing style.
- ^
John McCarthy. Recursive functions of symbolic expressions and their computation by machine, Part I. (PDF). Communications of the ACM (ACM New York, NY, USA). 1960, 3 (4): 184–195. doi:10.1145/367177.367199.
The Universal S-Function . There is an S-function with the property that if is an S-expression for an S-function and is a list of arguments of the form , where are arbitrary S-expressions, then and are defined for the same values of , and are equal when defined.
- ^
Gerald J. Sussman, Guy L. Steele Jr. The Art of the Interpreter of the Modularity Complex (Parts Zero, One, and Two). 1978 [2021-11-07]. (原始内容存档于2021-11-07).
The evaluator proper (see Figure 2) is is divided into two conceptual components:
EVALandAPPLY.EVALclassifies expressions and directs their evaluation. Simple expressions (such as constants and variables) can be evaluated directly. For the complex case of procedure invocations (technically called "combinations"),EVALlooks up the procedure definition, recursively evaluates the arguments (usingEVLIS), and then callsAPPLY.APPLYclassifies procedures and directs their application. Simple procedures (primitive operators) are applied directly. For the complex case of user-defined procedures,APPLYusesBINDto build an environment, a kind of symbol table, associating the formal parameters from the body of the procedure definition with the actual argument values provided byEVAL. The body of the procedure definition is the passed toEVAL, along with the environment just constructed, which is used to determine the values of variables occurring in the body. - ^
Matthias Felleisen, Daniel P. Friedman. Control Operators, the SECD-Machine, and the Lambda-Calculus. Department of Computer Science, Indiana University. 1986.
For historical reasons we use an abstract machine to formally define the semantics of Λc-programs. The machine is derived from Reynolds' extended interpreter IV [15]. It is similar to Landin's SECD-machine [8] but closer to denotational semantics and, hopefully, easier to understand. The Machine works on states which are triples composed of a control string, an environment, and a continuation code; it is accordingly referred to as the CEK-machine.
- ^
Christopher T. Haynes, Daniel P. Friedman, Mitchell Wand. Continuations and coroutines. LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional programming. 1984.“In a continuation semantics, every recursive procedure receives a continuation parameter. Rather than simply return, the procedure either passes its result directly to this continuation, or passes the continuation (possibly embellished) to some other procedure. ……
(define meaning (lambda (e r k) ; e = expression, r = environment, k = continuation (case (type-of-expression e) [constant (k e)] [identifier (k (R-lookup e r))] [lambda (k (lambda (actuals k) (evaluate-all (body-pts e) (extend-env r (formals-pt e) actuals) k)))] [if (meaning (test-pt e) r (lambda (v) (if v (meaning (then-pt e) r k) (meaning (else-pt e) r k))))] [set! (meaning (val-pt e) r (lambda (v) (k (store! (L-lookup (id-pt e) r) v))))] [call/cc (meaning (fn-pt e) r (lambda (f) (f (list (lambda (actuals dummy) (k (car actuals)))) k)))] [application (meaning-of-all (comb-parts e) r (lambda (vals) ((car vals) (cdr vals) k)))]))) (define evaluate-all (lambda (exp-list r k) (meaning (car exp-list) r (if (null? (cdr exp-list)) k (lambda (v) (evaluate-all (cdr exp-list) r k)))))) (define meaning-of-all (lambda (exp-list r k) (meaning (car exp-list) r (lambda (v) (if (null? (cdr exp-list)) (k (cons v nil)) (meaning-of-all (cdr exp-list) r (lambda (vr) (k (cons v vr)))))))))
Figure 1: Meta-circular interpreter for a subset of Scheme 84”
- ^ Guy L. Steele Jr. Common Lisp the Language, 2nd Edition. 1990 [2022-12-16]. ISBN 1-55558-041-6. (原始内容存档于2023-01-17).
In describing various features of the Common Lisp language, the notions of scope and extent are frequently useful. These notions arise when some object or construct must be referred to from some distant part of a program. Scope refers to the spatial or textual region of the program within which references may occur. Extent refers to the interval of time during which references may occur.
- ^
Andrew W. Appel. Compiling with Continuations (PDF). Cambridge University Press. 1992.
What follows is a straightforward continuation semantics written in Standard ML. ……
The first compilers that used continuation-passing style (CPS) as an intermediate language [83, 54] represented the CPS using Scheme [69] notation — in those compilers, a CPS expression was just a Scheme program satisfying certain syntactic properties. In the Standard ML of New Jersey compiler (and in this book) we use a more specialized representation. ……
After the language-specific optimizations and representation decisions have been made, the program being compiled is converted into continuation-passing style. This is done by a recursive traversal over the source-language abstract syntax tree; in Standard ML of New Jersey, we traverse the lambda-language expression that’s a simplified version of the abstract syntax tree. - ^
Olivier Danvy, Andrzej Filinski. Representing control: A study of the CPS transformation (PDF). Mathematical Structures in Computer Science, Volume 2, Issue 4, pp. 361–391. 1992.
The CPS transformation permits a simple definition of generalized escape constructs like Scheme's
call/cc. Such operators are often perceived to eliminate the need for explicit CPS programs. However, sometimes then greater generality of "genuine" CPS actually needed to express an algorithm (e.g., to implement backtracking (Mellish and Hardy 1984)). Our investigation of the CPS transform leads naturally to the introduction of two new control operators,shiftandrest, which allow the additional power of general CPS to be exploited in direct style programs. - ^
Andrew K. Wright, Matthias Felleisen. A syntactic approach to type soundness (PDF). Inf. Comput., 115 (1): 38–94. 1994.
A context
Cis is an expression with one subexpression replaced by a hole, denoted[ ]. The expressionC[e]results from placing an expressionein the hole ofC; this operation may involve capture of the free variables ofebyC. - ^
Robert Harper. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press. 2016.
A variant of structural dynamics, called contextual dynamics, is sometimes useful. …… The main idea is to isolate instruction steps as a special form of judgment, called instruction transition, and to formalize the process of locating the next instruction using a device called an evaluation context.
- ^ Xavier Leroy. Control structures in programming languages From goto to algebraic effects. 2025.
- ^ Christopher T. Haynes, Daniel P. Friedman, Mitchell Wand. Continuations and coroutines. LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional programming. 1984.
In this paper we demonstrate that a wide variety of coroutine mechanisms may easily be defined by the user given a single control abstraction, called a continuation. The power of continuations stems from their first class nature: they may be passed to and return from functions, be stored in data structures, and have indefinite extent.
- ^ cl-cont. [2021-10-11]. (原始内容存档于2012-03-30).
- ^ Factor handbook » The language » Continuations.
- ^ Control.Monad.Cont.
- ^ S. B. Wample, R. E. Griswold. Co-expression in Icon* (PDF). The Computer Journal, Volume 26, Issue 1, Pages 72–78. 1983.
- ^ kotlin-stdlib/kotlin.coroutines/Continuation.
- ^ R Documentation — callCC {base} — Call With Current Continuation.
- ^ class Continuation.
- ^ GNU Smalltalk Library Reference - Base classes — Continuation.
- ^ Eggs Unlimited (release branch 5) — F-operator.
延伸阅读
[编辑]- Peter Landin. A Generalization of Jumps and Labels (PDF). Report. UNIVAC Systems Programming Research. Reprinted in Higher Order and Symbolic Computation, 11(2):125-143, 1998, with a foreword by Hayo Thielecke. August 1965.
- Christopher Strachey, Christopher P. Wadsworth. Continuations: a Mathematical semantics for handling full jumps (PDF). Technical Monograph PRG-11. Oxford University Computing Laboratory. Reprinted in Higher Order and Symbolic Computation, 13(1/2):135—152, 2000. January 1974.
- Robert Milne, Christopher Strachey. Theory of Programming Language Semantics. Part A. Theory of Programming Language Semantics. Part B. Halsted Press, Div. of John Wiley & Sons, Inc. 605 Third Ave. New York, NY, United States. 1976.
- Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge. 1977.
- R. D. Tennent. The denotational semantics of programming languages. Communications of the ACM, Volume 19, Issue 8 Pages 437 - 453. 1976.
- Michael J. C. Gordon. The denotational description of programming languages - an introduction. Springer-Verlag, Berlin, Heidelberg. 1979.
- John C. Reynolds. Definitional Interpreters for Higher-Order Programming Languages. Proceedings of 25th ACM National Conference, pp. 717–740. Reprinted in Higher-Order and Symbolic Computation 11(4):363-397, 1998, with a foreword. 1972.
- John C. Reynolds. On the Relation between Direct and Continuation Semantics. Proceedings of Second Colloquium on Automata, Languages, and Programming. LNCS Vol. 14, pp. 141–156. 1974.
- John C. Reynolds. The Discoveries of Continuations (PDF). Lisp and Symbolic Computation. 1993, 6 (3/4): 233–248 [2021-10-11]. (原始内容存档 (PDF)于2022-03-20).
- Michael J. Fischer. Lambda-Calculus Schemata (PDF). LISP AND SYMBOLIC COMPUTATION: An International Journal, 6, 259–288. 1993 [2021-11-10]. (原始内容存档 (PDF)于2022-03-02).
- Robert Hieb, R. Kent Dybvig, Carl Bruggeman. Representing Control in the Presence of First-Class Continuations. Proceedings of the ACM SIGPLAN '90 Conference on Programming Language Design and Implementation, pp. 66–77. 1990.
- Jacob Matthews, Robert Bruce Findler. An operational semantics for Scheme (PDF). The Journal of Functional Programming, Volume 18, Number 1, 47-86. 2008.
外部链接
[编辑]- Ben Siraphob. A correct Scheme interpreter derived from the R5RS spec's formal semantics, written in Haskell.
- Bill Hails. Low level (C) implementation of a CEK machine with an additional "F" failure continuation supporting amb.
- Teach Yourself Scheme in Fixnum Days (页面存档备份,存于互联网档案馆) by Dorai Sitaram features a nice chapter on continuations.
- Spore, include-yy. 「翻译」Introduction to Programming with Shift and Reset. 知乎.