call/cc 總結 | Scheme
來源 https://www.sczyh30.com/posts/Functional-Programming/call-with-current-continuation/
Continuation
Continuation 也是一個老生常談的東西了,我們來回顧一下。首先我們看一下 TSPL4 中定義的表達式求值需要做的事:
During the evaluation of a Scheme expression, the implementation must keep track of two things: (1) what to evaluate and (2) what to do with the value.
Continuation 即為其中的(2),即表達式被求值以后,接下來要對表達式做的計算。R5RS 中 continuation 的定義為:
The continuation represents an entire (default) future for the computation.
比如 (+ (* 2 3) (+ 1 7))
表達式中,(* 2 3)
的 continuation 為:保存 (* 2 3)
計算出的值 6
,然后計算 (+ 1 7)
的值,最后將兩表達式的值相加,結束;(+ 1 7)
的 continuation 為:保存 (+ 1 7)
的值 8
,將其與前面計算出的 6
相加,結束。
Scheme 中的 continuation 是 first-class 的,也就是說它可以被當做參數進行傳遞和返回;並且 Scheme 中可以將 continuation 視為一個 procedure,也就是說可以調用 continuation 執行后續的運算。
call/cc
每個表達式在求值的時候,都會有一個對應的 current continuation,它在等着當前表達式求值完畢然后把值傳遞給它。那么如何捕捉 current continuation 呢?這就要用到 Scheme 中強大的 call/cc
了。call/cc
的全名是 call-with-current-continuation
,它可以捕捉當前環境下的 current continuation 並利用它做各種各樣的事情,如改變控制流,實現非本地退出(non-local exit)、協程(coroutine)、多任務(multi-tasking)等,非常方便。注意這里的 continuation 將當前 context 一並打包保存起來了,而不只是保存程序運行的位置。下面我們來舉幾個例子說明一下 call/cc
的用法。
current continuation
我們先來看個最簡單的例子 —— 用它來捕捉 current continuation 並作為 procedure 調用。call/cc
接受一個函數,該函數接受一個參數,此參數即為 current continuation。以之前 (+ (* 2 3) (+ 1 7))
表達式中 (* 2 3)
的 continuation 為例:
1
2
3
4
5
|
(
define cc #f)
(
+ (call/cc (lambda (return)
(
set! cc return)
(
* 2 3)))
(
+ 1 7))
|
我們將 (* 2 3)
的 current continuation (用(+ ? (+ 1 7))
表示) 綁定給 cc
變量。現在 cc
就對應了一個 continuation ,它相當於過程 (define (cc x) (+ (x) (+ 1 7)))
,等待一個值然后進行后續的運算:
1
2
3
4
5
6
|
> cc
#<continuation>
> (cc 10)
18
> (cc (* 2 3))
14
|
這個例子很好理解,我們下面引入 call/cc
的本質 —— 控制流變換。在 Scheme 中,假設 call/cc
捕捉到的 current continuation 為 cc
(位於 lambda
中),如果 cc
作為過程 直接或間接地被調用(即給它傳值),call/cc
會立即返回,返回值即為傳入 cc
的值。即一旦 current continuation 被調用,控制流會跳到 call/cc
處。因此,利用 call/cc
,我們可以擺脫順序執行的限制,在程序中跳來跳去,非常靈活。下面我們舉幾個 non-local exit 的例子來說明。
Non-local exit
Scheme 中沒有 break
和 return
關鍵字,因此在循環中如果想 break
並提前返回的話就得借助 call/cc
。比如下面的例子尋找傳入的 list
中是否包含 5
:
1
2
3
4
5
6
7
8
9
10
11
12
|
(
define (do-with element return)
(
if (= element 5)
(
return 'find-five)
(
void)))
(
define (check-lst lst)
(
call/cc (lambda (return)
(
for-each (lambda (element)
(
do-with element return)
(
printf "~a~%" element))
lst)
'not-found)))
|
測試:
1
2
3
4
5
6
7
8
9
|
> (check-lst '(0 2 4))
0
2
4
'not-found
> (check-lst '(0 3 5 1))
0
3
'find-five
|
check-lst
過程會遍歷列表中的元素,每次都會將 current continuation 傳給 do-with
過程並進行調用,一旦do-with
遇到 5
,我們就將結果傳給 current continuation (即 return
),此時控制流會馬上跳回 check-lst
過程中的 call/cc
處,這時候就已經終止遍歷了(跳出了循環)。call/cc
的返回值為 'find-five
,所以最后會在控制台上打印出 'find-five
。
我們再來看一個經典的 generator 的例子,它非常像 Python 和 ES 6 中的 yield
,每次調用的時候都會返回 list 中的一個元素:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(
define (generate-one-element-at-a-time lst)
;; Hand the next item from a-list to "return" or an end-of-list marker
(
define (control-state return)
(
for-each
(
lambda (element)
(
set! return (call/cc
(
lambda (resume-here)
;; Grab the current continuation
(
set! control-state resume-here)
(
return element)))))
lst)
(
return 'you-fell-off-the-end))
;; This is the actual generator, producing one item from a-list at a time
(
define (generator)
(
call/cc control-state))
;; Return the generator
generator)
(
define generate-digit
(
generate-one-element-at-a-time '(0 1 2)))
|
調用:
1
2
3
4
5
6
7
8
|
> (generate-digit)
0
> (generate-digit)
1
> (generate-digit)
2
> (generate-digit)
'you-fell-off-the-end
|
注意到這個例子里有兩個 call/cc
,大家剛看到的時候可能會有點暈,其實這兩個 call/cc
各司其職,互不干擾。第一個 call/cc
負責保存遍歷的狀態(從此處恢復),而 generator
中的 call/cc
才是真正生成值的地方(非本地退出)。其中一個需要注意的地方就是 control-state
,它在第一次調用的時候還是個 procedure,在第一次調用的過程中它就被重新綁定成一個 continuation
,之后再調用 generator
生成器的時候,控制流就可以跳到之前遍歷的位置繼續執行下面的過程,從而達到生成器的效果。
陰陽謎題
continuation 環境嵌套。后面有時間專開一篇分析~
1
2
3
4
5
|
(
let* ((yin
((
lambda (cc) (display #\@) cc) (call-with-current-continuation (lambda (c) c))))
(
yang
((
lambda (cc) (display #\*) cc) (call-with-current-continuation (lambda (c) c)))))
(
yin yang))
|
call/cc與數理邏輯
這里簡單提一下 call/cc
與類型系統和數理邏輯的聯系。call/cc
的類型是 ((P → Q) → P) → P
,通過 Curry-Howard 同構,它可以對應到經典邏輯中的 Peirce’s law:
Peirce’s law 代表排中律 P∧¬PP∧¬P,這條邏輯無法在 λ演算所對應的直覺邏輯中表示(直覺邏輯中雙重否定不成立),因此 call/cc
無法用 λ表達式定義。通常我們用擴展后的 λμ calculusλμ calculus 來定義 call/cc
,λμ calculusλμ calculus 經 Curry-Howard 同構可以得到經典邏輯。
References
- The Scheme Programming Language, 4th Edition
- Short introduction to call-with-current-continuation
- The Revised Revised Revised Revised Revised Report on the Algorithmic Language Scheme (R5RS)
- The Racket Guide, 10.3 Continuations
- Call-with-current-continuation, Wikipedia
- The Continuation Passing Transform and the Yoneda Embedding
- What is continuation-passing style in functional programming? - Quora
call/cc的類型是什么
原文:https://blog.csdn.net/nklofy/article/details/48999417
這篇來自我在某問答網站上的一個回答。但我覺得這個問題很有價值,我思考和寫作的時間花費了很久。所以我覺得應該保存起來。
問題是,call/cc的類型是什么。我們知道,(call/cc (lambda (k) p))有兩種用法,一種是(call/cc (lambda (k) (k a))),例如(+ 1(call/cc (lambda (k) (k 2))));一種是(call/cc (lambda (k) k)),例如(let a (call/cc (lambda (k) k))) 或 (define (get-cc) (call/cc (lambda (c) c))) 。第一種返回a,並送入continuation計算;第二種直接返回一個continuation。
所以很明顯,call/cc不是只有一種返回類型。兩種用法對應兩種不同類型。第一個類型是((T1 -> T2) -> T1) -> (T1 -> T2) -> T1,第二種是( (T1 -> T2) -> (T1 -> T2) ) -> (T1 -> T2) -> (T1 -> T2)。
一個簡單的聯想是,假設x類型是T1->T2, a類型是T1,那么 ((λ(k) (k a) ) x)和 (λ(k) (k) ) x)分別返回什么類型?前者是T2,后者是T1->T2。這就是所謂函數一等公民。
回到call/cc。首先要分析整個程序到call/cc之前的位置,按照TAPL的表達方式,此時的continuation類型是:
λ k: T1 . T1 -> T2
從這個位置開始,call/cc被調用,evaluation rules可表示為:
call/cc [k |-> continuation ] λ k. k a --> a。 E-APP1 (第一種情況)
call/cc [k |-> continuation ] λ k. k --> continuation。 E-APP2 (第二種情況)
第一種情況下,type rule為:
Γ├ continuation: T1->T2 Γ├ a: T1 Γ├ λ k: T1 -> T2 . k a
-------------------------------------------------------------------------------------- T-APP1
Γ├ (call/cc ( λ k . k a )) continuation : T1
call/cc過程返回類型T1。原因是evaluation rule對應的是E-APP1。
第二種情況下type rule:
Γ├ continuation: T1->T2 Γ├ λ k: T1 -> T2 . k
-------------------------------------------------------------------------------------- T-APP2
Γ├ (call/cc ( λ k . k)) continuation : T1->T2
即該情況下應該返回T1->T2。
所以結論就是,兩種情況下,返回的類型是不一樣的。call/cc有兩種可能的返回類型,返回哪一種根據不同的(λ (k) process)匹配。一種匹配 k a,另一種匹配 k。是的,這就類似於(λ x . x a ) 與(λ x . x ) 的區別,返回類型不一樣很正常。
在第二種情況下process 直接返回k,但其實程序中call/cc 前后通常會有個let、set!或者其他賦值函數,將這個continuation保存到某個變量x,程序后面會調用(x a)的形式。對於(x a)或者之前的(continuation a),都回到了(T1 -> T2) -> T1 -> T2的套路上,程序最終運行完時兩種情況殊途同歸。
PS,在我看來,call/cc更接近於宏而非函數,往往純用於結構跳轉而非求值,例如call/cc (lambda (k) (if(something) (k #t)))...)這種用法。它的精華放在(k #t)以外的地方,控制運行還是跳轉。還有,scheme本來就是動態類型系統,類型可以任意的變,分析起來非常痛苦。若當作宏來看就順眼多了,(...call/cc ...)這個括號里的內容整體用k一個符號代替。然后無論哪種用法,遇到k a或k b時,從整個程序中挖掉call/cc括號內容后,a或b代入k所在位置就能得到結果。
參考文獻:<types and programming languages>
================= End