call/cc 總結 | Scheme

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：

 

((P→Q)→P)→P((P→Q)→P)→P

 

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