如何解釋 Lisp 中 call/cc 的概念？

---

大家都說得挺好了。我來補充一下 @Belleve 最後所說的「在 Curry-Howard 同構的層面，call/cc 對應皮爾士定律，它代表著排中律，這條定律是 Lambda 演算所對應的直覺邏輯里沒有的」是什麼意思。

第一部分，先說什麼是皮爾士定律（Peirce』s law）

按照wikipedia上的形式，在命題邏輯裡面這個是恆成立的：

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

大家可以列一下真值表驗證一下，就4種情況不難算的。這就是皮爾士定律。

然後一個特殊形式是把Q換成恆假命題⊥，則

(2) ((P→⊥)→P)→P

也是恆成立的。

Peirce』s law在直覺主義邏輯（構造性邏輯）里是不成立的，因為其特殊形式(2)可以推出排中律，而排中律在構造性邏輯里不成立。

第二部分，簡單介紹Curry-Howard 同構

一個程序對應一個證明，其證明的命題是這個程序的類型。要證明一個命題是否成立只需2步：1. 把這個命題寫出對應的類型；2. 看是否能構造一個程序滿足相應的類型（也叫做Type inhabitation problem）。

例子1：命題 「A → A」。顯然無論命題A是真是假，「A → A」這個命題總是成立的。Curry-Howard同構如下：

命題A 對應 類型A。注意「命題A可能真可能假」對應「類型A可能存在一個成員，也可能不存在任何成員」。

蘊含符號「→」對應函數定義符號「-&>」。

命題「A → A」對應一個新的類型，是一個函數類型「A -&> A」。

顯然我們可以構造函數

這個函數id直接返回其參數，所以無論參數的類型A是什麼，其返回值還是類型A。所以id函數是類型「A -&> A」的成員，所以命題「A → A」成立。

例子2：命題「A → B」。這個命題不成立，畫一下真值表可以知道。

你可以試試看能否寫出一個函數，對於任意類型A，B，給一個A類型的參數，返回一個B類型的值。應該是寫不出來的。

第三部分，「call/cc」這個特殊的東西的類型是什麼?

直接給答案：call/cc :: ((P -&> Q) -&> P) -&> P。

這個跟皮爾士定律的(1)式一模一樣！

解釋一下：你的current continuation （cc）需要一個輸入，不妨就把這個輸入的類型叫做P，然後這個cc可能算出某種Q類型的結果，至於Q是什麼我們根本不關心，Q完全可以是「⊥」（不停機）。所以這個cc的類型是 P -&> Q。

你的call/cc有唯一的參數f，這個f本身接受的參數是cc。所以f的類型應該是

f :: (P-&>Q) -&> X

這裡X是某種類型，但是我們不知道它是啥。沒關係，我們來分析一下它可能是啥：

call/cc最後會返回，而且其返回值的類型是 P。(按照 @王霄池 的說法就是當你「觸發回去的事件」，call/cc所處的位置被填充一個具體的值，其類型為P，然後計算接著進行下去。）

但是call/cc不能無中生有地得到一個P類型的值！怎麼才能得到呢？答案是它只能從它唯一的參數f裡面得到。我們再看一遍f的類型 f :: (P-&>Q) -&> X

其中，前一個P在逆變的位置，所以無法從中得到一個P類型的值，Q又完全可以跟P毫不相關，所以唯一能夠得到P類型值的地方就只有處於協變位置的X了！類似的推理可以看在Haskell里，每個類型都可以構造出來一個此類型的表達式嗎？ - 匿名用戶的回答 下面我的評論。

所以，X和P是一回事兒。f的類型是 (P-&>Q) -&> P。

那麼我們回頭來看 call/cc。它有一個參數f :: (P-&>Q) -&> P，然後當它「返回」的時候，給出一個值類型為P。所以

call/cc :: ((P -&> Q) -&> P) -&> P。這在Curry-Howard 同構里對應皮爾士定律。

又由於lambda演算對應直覺主義邏輯，而皮爾士定律在直覺主義邏輯裡面不成立，所以call/cc不能被lambda calculus表達。

我上面第三部分說的基本上是翻譯自此處：https://golem.ph.utexas.edu/category/2008/01/the_continuation_passing_trans.html#c044523。作者Joker_vD。

補充：如何由Peirce』s law的特殊形式(2)推出排中律。

有知友問到這個問題。我一開始還挺驚訝的，因為我用google搜「peirce"s law excluded middle」，第一頁就有很好的答案。

於是我用百度試了一下，用中文的「皮爾士定律 排中律」，或者加上一些「證明」，「推出」這樣的關鍵詞，確實找不到什麼有用的信息。

排中律是這個：

(3) P∨?P

其中 「?P」 實際上是 「P → ⊥」 的別名。

否定連接詞「?」是由蘊含（→）和恆假命題（⊥）定義的。即所謂「not P means that P implies absurdity」。

我們想要用Peirce』s law的特殊形式

(2) ((P→⊥)→P)→P

推出(3)式。

簡要的證明思路如下：

首先我們不加證明地使用三段論：如果 A→B 和 B→C 都成立，那麼可以推出 A→C 成立。

三段論的威力非常強大，一個用處是：如果我們已知一個蘊含命題 X → Y 成立，

那麼我們可以加強蘊含左邊的條件（就是說構造一個新命題X" 且證明 X" → X），則X" → Y依然成立。

或者我們可以減弱蘊含右邊的結論（就是說構造一個新命題Y" 且證明 Y → Y"），則X → Y"依然成立。

三段論可以完全使用MP（Modus ponens）推出來，這裡不贅述。

註：MP（Modus ponens），好像中文叫做「肯定前件」，是最重要的一條推演規則，就是說：

如果我們知道 A→B 和 A 這兩個命題都成立，則可以推出 B 這個命題也成立。

下面開始證明(3)式：

Step 1a: P → (P∨?P) 成立。 這是因為A → (A ∨ B) 對任意A,B都成立。

Step 1b: ((P→⊥)→P) → P 成立 （由(2)式）

我們首先把最後一個蘊含符號的結論減弱，從「P」減弱為「P∨?P」，則

(4) ((P→⊥)→P) → ( P∨?P) 成立

因為由 Step1a 可知，我們確實是減弱了最後一個蘊含符號右邊的結論。

Step 2a: 「⊥→P 」 成立。 這是因為恆假命題 ⊥ 可以推出任何命題。

Step 2b: 如果 (P→⊥)→⊥ 成立，則 (P→⊥)→P 成立。還是使用三段論，後一個命題只是把前一個命題的結論減弱。

Step 2c:

(5) ((P→⊥)→⊥) → ( (P→⊥)→P ) 成立

可以直接從Step 2b逆用MP得到。

Step 3a:

(6) ((P→⊥)→⊥) → ( P∨?P) 成立

這是因為 (4) 成立，然後從(5)我們知道：((P→⊥)→⊥) 是 ( (P→⊥)→P ) 的加強。然後用三段論。

Step 3b:

(7) ( (?P) →⊥) → ( P∨?P) 成立

因為?P是(P→⊥)的一個別名而已。我們只是把(6)式換了個馬甲，重新寫了一遍。

Step 4a: (?P) → (P∨ ?P) 。 這是因為 A → (A ∨ B) 對任意A,B都成立。

Step 4b: 如果 (P∨ ?P) →⊥成立，則 (?P) →⊥ 成立。後一個命題只是把前一個命題的條件加強。這跟 Step 2b 有點類似，也是使用三段論，但是是用了另外一個方向而已。

Step 4c:

(8) ( (P∨ ?P) →⊥ ) → ( (?P) →⊥ ) 成立

從Step 4b逆用MP rule。

Step 5:

(9) ( (P∨ ?P) →⊥ ) → ( P∨?P) 成立

因為 (7) 成立，從 (8) 知道：( (P∨ ?P) →⊥ ) 是 (?P) →⊥ 的加強。所以用三段論得出(9)。

Step 6:

(10) ( ( (P∨ ?P) →⊥ ) → ( P∨?P) ) → ( P∨?P) 成立

這就是皮爾士定理的特殊形式(2)，但是把 「(P∨ ?P) 」這個整體代入(2)式中的「P」。

Step 7:

(3) P∨?P 成立

直接使用 (9), (10) 和 MP。

這樣就證完了。需要注意的是：

上面這個證明並不是形式化的。我這裡的每一個步驟是可以嚴格翻譯成形式化的，基本是一一對應，但是如果其中用到三段論，則需要展開。另外過程里用到MP rule的也叫做「application」，逆用MP rule的也叫「implication」。

這個證明不是最短的。這裡主要是為了展示如何靈活運用三段論（時而增強條件，時而減弱結論）。

一個很短的，同時也是形式化的證明可以看這個Stack Exchange上的問題：

http://math.stackexchange.com/questions/447098/why-peirces-law-implies-law-of-excluded-middle

---

解釋call/cc有點困難啊，請允許我打一個比方。

假設有一個巫師，他知道一個咒語：call-with-current-continuation，這個咒語簡稱是 call/cc。每當他念出這個咒語，就會讓整個世界的時間暫停，並創建一個新的宇宙，在這個宇宙中，他只能做一個監聽者，其他的什麼都不能做。一旦他監聽到某個人叫了他的名字，他就將這個人帶走，帶回到自己的宇宙，並繼續自己的時間軸。

當然，如果你只聽這個故事，雖然挺好玩，可是並沒有什麼幫助！

讓我們正經的講一下這個函數。在這裡我使用c語言類似的定義方式，以便講清楚各種類型。

call/cc是這樣的函數，它接受一個reciver參數

call/cc(reciver)


這個reciver也是一個函數，它接受一個continuation參數。

reciver(continuation)


continuation是當前環境的一個打包。記錄了這個程序此時的所有狀態。還記得我們的那個時間靜止的比喻嗎？說的就是此時此刻。

當call/cc被調用的時候，它會自動打包當前的環境，然後調用reciver。

continuation就如同一個函數一樣，它接受一個參數

contiuation(value)


當continuation被調用的時候，程序就回到了被打包的時刻。並且call/cc也有了一個返回值，那就是value。

好了，理論到此已經全部講完了，我們來舉個例子吧。

(define (f return)
(return 2)
3)
(display (f whatever)) ;; 3
(display (call-with-current-continuation f)) ;; 2


第一個display輸出的是 3，毫無疑問。

但第二個display輸出的是2。這是為什麼呢？

當我們調用

(call-with-current-continuation f)


的時候，會首先打包整個環境，我們稱之為C，然後以之為參數，調用f

(f C)


看看 f 的定義就知道，得先對

(return 2)


求值。實參是C，所以

(C 2)


這就觸發了回去的事件，所以我們回到最初的程序。

(display (call-with-current-continuation f))


但是這次 call/cc是有值的，那就剛才C的參數，也就是2，那麼最後的程序就是

(display 2)


好了，這就是call/cc，如果你懂了，就請點個贊吧~

---

call/cc 是非常、非常特殊的，因為它根本無法用 Lambda 演算定義。

研究中使用了擴展的演算來處理這玩意。

演算引入了一個結構算符，以及標記項（它表示將表達式標記為 ），對算符的展開滿足

• 左結構嬗變：

• 右結構嬗變：

換言之，在「函數」被調用，或者被傳入其他函數的時候，其體內所有和參數同標記的標記項都會以相同的形式被「調用」或者「傳入其他函數」一次。算符可以將自己「外面」的東西翻到自己裡面來。

在有這個算符之後，我們就能定義。在式子里就是 Continuation，我們可以看下它會變化成怎樣：

• 被傳入：

• 被調用：

嗯……

在 Curry-Howard 同構的層面，call/cc 對應皮爾士定律，它代表著排中律，這條定律是 Lambda 演算所對應的直覺邏輯里沒有的。演算經過 C-H 同構可以得到經典邏輯。

---

就是一種超級 goto ，支持 Continuation 的語言允許顯式的創建一種叫做 Continuation 的對象，將創建時系統所有的上下文信息保存在裡面，然後程序員可以在需要的任何時候回到這個狀態繼續執行下面的代碼。

舉個簡單的例子，Ruby版：

require "continuation"

def choose(*choices)
choices.each do |choice|
callcc do |cont|
if choice.respond_to? :call
return choice.call
else
return choice
end
end
end
end


方法 Kernel#callcc 產生一個當前位置的 Continuation 對象，其實例方法 Continuation#call 能夠回到創建該對象的位置，並從創建它的 callcc 塊之後的代碼開始執行 。

---

本來應該執行A，但call/cc（流程）跳轉執行到另外一個地方，且把A傳遞過去，以後再通過調用A返回到原來A的執行流程。

整個執行流程是以樹的形式表達，而不是傳統C/C++堆幀的形式。

---

先提一個不同的、但可以幫助理解 call/cc 的東西：CPS （Continuation-Passing Style）。

我們可以把一個程序「接下來要做的事情」放進一個閉包里。

這樣做的好處是，調用另一個函數的時候，前一個函數已經執行到最後了（之後要執行的代碼放進閉包了嘛），於是我們就不用管這個函數的幀了。

更厲害的是，內層的函數可以隨心所欲控制接下來要做的事情（儘管這不是 CPS 的本來目的）。如果「接下來要做的事情」很重要，那我們讓它做三遍也是可以的。

這裡拿 JS 來寫：

function a(x) {
y = b(x);
z = c(y);
d(z);
}


魔改一下，讓 b 和 c 都接受一個回調函數作為參數。變成這樣：

function a_cps(x) {
b_cps(x, function (y) {
c_cps(y, function (z) {
d(z);
});
});
}


b_cps 可以長這樣：

function b_cps(x, callback) {
callback(b(x));
}


是不是感覺很眼熟？對，如果你有一塊不能豎過來的寬屏幕，一定會喜歡上 JS 的 Callback Hell 的（誤），於是就對這種寫法眼熟啦。

當然，CPS 和非同步回調還是有區別的。非同步回調不強制所有調用都要變換，而 CPS 必須做完整。我們談論的 CPS，也更多是在不考慮非同步的環境下。

那麼調用完函數 a 之後，如果還有別的代碼要跑，比如我們要把 d(z) 的結果返回給之後的代碼進一步處理，怎麼辦？

我們可以讓 a 和 d 也接受一個回調函數，把調用 a 之後要做的事情交給 d：

function a_cps_2(x, callback) {
b_cps(x, function (y) {
c_cps(y, function (z) {
d_cps(z, callback);
});
});
}


但這樣寫是很麻煩的，不然垠神為什麼要寫四十行代碼呢，是吧。在有複雜控制流的語言里，CPS 的代碼就更沒法看了，就算你在 IMAX 影院里寫代碼也不行。

怎麼辦？我們魔改一下 JS，往函數里加兩個「裂縫」，實際上把整個函數剖成了三段。然後，把裂縫出口傳給內層的函數，問題就解決了：

function a_magic(x) {
y = 大裂縫0 &<===&> b_magic(x, 大裂縫出口0);
z = 大裂縫1 &<===&> c_magic(y, 大裂縫出口1);
d(z);
}


call/cc 就是一種實現裂縫的方式：

function a_callcc(x) {
y = callcc b_callcc(x);
z = callcc c_callcc(y);
d(z);
}


調用 callcc 的時候，當前的上下文（程序執行到的位置，調用鏈上的每一幀）全被打包進了一個回調函數，然後交給內層函數處理：

function b_callcc(x, return_func) {
return_func(b(x));
}


return_func 會直接把傳入的 b(x) 的值交給之前保存的上下文，從 y = callcc ... 這裡接著執行下去，即 y = b(x)。

藉助 call/cc，我們可以控制程序接下來的執行方式：

function 選特首(支持董先生, 歷史的行程) {
if (支持董先生 == "支持!") {
歷史的行程("吼啊!");
} else {
// 悶聲大發財
}
}

console.log(callcc 選特首("支持!")); // 輸出 吼啊!
// or:
console.log(callcc 選特首("不支持!")); // 什麼也沒有發生


實際 call/cc 可以實現很多複雜的執行流程。比如在一個走迷宮（搜索）的程序里，你可以把當前走到的位置（上下文）餵給 call/cc，然後就能在任何時候瞬間移回到這個點繼續走下去（調用 return_func）。

這樣的代價是，函數的幀不再是棧，而是一棵樹。因此，要麼有性能 overhead，要麼編譯器/解釋器就得做很多分析工作來消除 overhead。

---

這是一種特定用途的逃逸結構.

如果不從理論來講,直接看r5rs規範中的例子,可以先有個直觀的理解:

(call-with-current-continuation
(lambda (exit)
(for-each (lambda (x)
(if (negative? x) (exit x) `()))
`(54 0 37 -3 245 19));;在-3處結束
#t))
=? -3

;;如果把-3改為3
(call-with-current-continuation
(lambda (exit)
(for-each (lambda (x)
(if (negative? x) (exit x) `()))
`(54 0 37 3 245 19));;-3-&>3,由於沒有直接滿足的,所以結束時是exit的值
#t))
=? #t


也就是類似break的效果.

由於沒有break,scheme想要實現跳轉的方式,當for-each中的條件滿足時,也就是被求值時,過程就結束了.

調用call/cc時,產生一個等待參數的過程,在參數(這裡的exit)之後的程序稱為current-continuation.

Racket文檔中的詳細定義是這樣的:

10.4 Continuations

(call-with-current-continuation proc

[prompt-tag]) → any

proc : (continuation? . -&> . any)

prompt-tag : continuation-prompt-tag?

= (default-continuation-prompt-tag)

Captures the current continuation up to the nearest prompt tagged by prompt-tag; if no such prompt exists, the exn:fail:contract:continuation exception is raised. The truncated continuation includes only continuation marks and dynamic-wind frames installed since the prompt.

The capture continuation is delivered to proc, which is called in tail position with respect to the call-with-current-continuation call.

If the continuation argument to proc is ever applied, then it removes the portion of the current continuation up to the nearest prompt tagged by prompt-tag (not including the prompt; if no such prompt exists, the exn:fail:contract:continuation exception is raised), or up to the nearest continuation frame (if any) shared by the current and captured continuations—whichever is first. While removing continuation frames,dynamic-wind post-thunks are executed. Finally, the (unshared portion of the) captured continuation is appended to the remaining continuation, applying dynamic-wind pre-thunks.

The arguments supplied to an applied procedure become the result values for the restored continuation. In particular, if multiple arguments are supplied, then the continuation receives multiple results.

If, at application time, a continuation barrier would be introduced by replacing the current continuation with the applied one, then the exn:fail:contract:continuation exception is raised.

A continuation can be invoked from the thread (see Threads) other than the one where it was captured.

---

baozii , Irons Du , 丁偉傑 各位回答都有啟發性

現在還不能完全想明白。

我現在是這樣理解的：

continuation內部可能有這些狀態：

code：對應要執行的代碼的s表達式

ip：下一句要執行的代碼，對應code中的某個節點

stk: 代碼執行的堆棧（每個函數調用應當都會對應一個堆棧幀吧？）

call-frame: 對應調用call/cc的函數的堆棧幀

continuation的運行流程：

continuation是一個函數（他要求一個參數）（在這個函數環境中包含了上述這些狀態變數）

在調用一個continuation的時候要傳入一個參數，這個參數求值的結果就是(call/cc ...)節點求值的結果，並被放到continuation:call-frame堆棧幀中某個位置。

然後要調整堆棧，丟棄continuation:call-frame之上的所有堆棧幀。

然後從continuation:ip對應的位置繼續執行代碼

(define r #f)

(begin

(display " hello ")

(display

(+ 1

(call/cc

(lambda (k)

(set! r k)

(+ 2 (k 3))

)

)

)

)

(display " world ")

(newline)

)

=&> helllo 4 world

上面這段代碼可以這樣解釋：

在執行call/cc的時候

首先是創建了一個continuation ，其中：

continuation:code對應於(begin ....)這段代碼。

continuation:ip指向call/cc對應節點執行完後要執行的節點，這裡應當對應的是 (display " world ")節點。

continuation:stk 怎麼初始化？？？？

continuation:call-frame 應當對應調用(call/cc...)節點的函數的堆棧幀

然後call/cc會調用(lambda (k)...)並將新創建的這個continuation 過程傳給他作為參數，這樣當(k 3)被調用時就比較好解釋了

(r 5)

=&> 6 world

這個也比較好理解。

(+ 3 (r 5))

=&> 6 world

這個地方為什麼不是9
world 呢？？？？？？

---

(call/cc (lambda (k) BODY))


或者少點括弧用這個

(let/cc k BODY)


continuation是「然後要做的事情」，「要做的事情」我們用什麼表示？當然是函數，所以說k是個函數。

如果我們在BODY里呼叫了(k ...)，那麼會立即跳出(let/cc k BODY)，去做下一個括弧/外層括弧的事。

那麼剛才(let/cc k BODY)沒執行完，它的返回值是什麼呢？就是你傳給k的參數。

---

其實想要解釋callCC, 用haskell非常簡單

callCC f = cont $ h -&> runCont (f (a -&> cont $ _ -&> h a)) h

關鍵是\_這個地方， 明白了這個，就明白了一切。

\_可以概括為， 調用f的瞬間， 就忽略了接下來的continuation, 把a直接傳給了h。

參考

Haskell/Continuation passing style

call/cc implementation?

---

lisp里提供操控continuation的operator有許多，好像沒有call/cc

scheme選了call/cc，是因為這幫人對語言追求精緻，所以找了一個威力最大的

其實call/cc的syntax挺醜陋的，他們自己也承認的

---

SpringerFriedman的Scheme and the art of programming-chapter16 中有對call/cc的詳細解釋，可以參考。

那裡引入了context（上下文）和escaper（逃逸子）兩個過程，有助於理解。

首先context是一個單參過程,比如(+ 2 (* 3 4))中3的context就是:

(lambda (hole)
(+ 2 (* hole 4)))


其次escaper就是將一個過程逃逸地調用,比如

(+ 1 2 (* 3 ((escaper sin) 4)))
;;=&>
(sin 4)


,也就是說無論escaper外面的環境怎樣,表達式只計算被escaper包含的過程所要計算的部分,也就是逃逸了.

call/cc的含義就是把(call/cc receiver)所在的上下文(是一個過程)做成逃逸形式,並且被另一個過程receiver調用:

(.. (call/cc receiver) ..)
;;=&>
(.. (receiver (escaper (context))) ..)
;;其中context就是(call/cc receiver)的上下文,即
(lambda (hole) (.. hole ..))
;;continuation 就是逃逸的上下文: (escaper (context))


---

整個執行流程是以樹的形式表達，而不是傳統C/C++堆幀的形式。

推薦看一下continuation的概念

---

我的理解是 相當於註冊一個callback

---

推薦閱讀：