函數式編程中cps（continuation-passing style ）是什麼意思？

01-05

有沒有不基於lisp、c++的例子，最好是python的，也有lamdba expression嘛。

從另一個角度回答下吧。

帶 callcc 的 Lambda 演算（叫 $lambdamu$ 演算）可以經 Curry-Howard 同構到經典邏輯，而普通的 $lambda$ 演算只能同構到直覺邏輯。但是形式邏輯中有一個 Gilvenko 定理，它聲稱：

對任何命題 $p$ 和前提 $Gamma$ ，在經典邏輯中 $Gammavdash p$ 若且唯若在直覺邏輯中 $Gammavdash eg eg p$

在證明這個定理之後哥德爾（對，就是證明存在不確定命題的那個）和根岑（自然演繹和相繼式演算的發明人）發明了雙否定變換，也叫哥德爾-根岑變換，其規則是：

$alpha^{*}=(alpha ightarrowot) ightarrowot$

$(alpha ightarroweta)^*=alpha^* ightarrow eta^*$

注意到哥德爾-根岑變換任意命題都和原命題經典等價，但並非直覺等價（直覺邏輯本身否認 $eg egalpha ightarrowalpha$ ），但是按照 Gilvenko 定理，雙否定命題 $alpha^*$ 若在直覺邏輯體系中可證明為真，則在經典邏輯體系里 $alpha$ 必為真，反之亦然。

那麼按照 Curry-Howard 同構， $lambdamu$ 演算下的類型指派 $Gammavdash e:alpha$ 可以經過哥德爾-根岑變換得到一個 $lambda$ 演算類型指派： $Gamma^*vdash e^*:alpha^*$ ，將表達式（同構於證明過程） $e$ 變為 $e^*$ 的過程就是 CPS 變換。直接照搬哥德爾-根岑變換里的類型的話，我們有如下結果：

原子 $a^*=lambdakappa.kappa a$
調用 $(EF)^*=lambdakappa.E^*(lambda E$
抽象 $(lambda x.E)^*=lambdakappa.kappa(lambda x.lambda k. (e^*)k)$
call/cc 運算元 $mathrm{call/cc}=lambdakappa.kappa(lambda f.lambda k.f k k)$

可以證明， $E^*(lambda x.x) =_eta E$ ，即：CPS 變換不改變語義。

當然這個版本的 CPS 是非常冗長的，市面上見到的那些都是在變換是之後直接做了 $eta$ 規約，刪掉大堆 Redex 的。

上面這些再一次說明了，邏輯學和編程有多麼緊密的聯繫。

其實就是把

Fuckee FindFuckee() { return kula; }


void Fuck(Fuckee fuckee, int count)

{

    for(int i=0;i&
改成
void FindFuckee(Action& continuation)

{

    continuation(kula);

}

void Fuck_(Fuckee fuckee, int count, int i, Action continuation)

{

    if(i&Fuck_(fuckee, count, i+1, continuation);

    else continuation();

}
void Fuck(Fuckee fuckee, int count, Action continuation)

{

    Fuck_(fuckee, count, 0, continuation);

}
void Main(Action continuation)

{

    FindFuckee(fucker=&>Fuck(fucker, 100, continuation));

}


的過程，返回值都改成了callback，相應的循環就變成了遞歸

CPS把函數調用完之後接下來要執行的代碼通過閉包包裹並作為函數參數調用要執行的函數。
這幾篇文章寫的很好：
Continuation Passing Style Revisited, Part One
Continuation Passing Style Revisited Part Two: Handwaving about control flow
Continuation Passing Style Revisited Part Three: Musings about coroutines

 
Continuation Passing Style Revisited Part Four: Turning yourself inside out
Continuation Passing Style Revisited Part Five: CPS and Asynchrony

@Belleve的回答太抽象了，沒邏輯背景的人看不懂，
我在Quora上看到一個回答寫得挺好的，裡面從邏輯學的角度解釋的一節或許可以作為 @Belleve答案的補充：
What is continuation-passing style in functional programming?
粘貼一下邏輯學那一節：

 

cps（continuation-passing style）一定要舉例子的話用函數式語言舉例子更好。比如 Haskell 或者 OCaml。
比如先定義一些基本的函數（OCaml）：
let inck n k = k (n + 1);;

let deck n k = k (n - 1);;

let addk a b k = k (a + b);;

let subk a b k = k (a - b);;

let mulk a b k = k (a * b);;

let modk a b k = k (a mod b);;

let float_addk a b k = k (a +. b);;

let float_subk a b k = k (a -. b);;

let float_mulk a b k = k (a *. b);;

let concatk s1 s2 k = k (s1^s2);;

let truncatek n k = k (truncate n)


因為函數是第一等公民，這幾個還是挺好理解的。k 是函數的一個參數，k 自己也是一個函數，那麼 k (n + 1) 就是將 (n + 1) 傳給函數 k 求值 =&>  k(n+1)
有了這些基本函數之後隨便寫一個新函數：
write a function diff_flipk that takes one integer argument p and 「returns」 the expression 2 ? ((1 ? p) ? p).  

 
let diff_flipk p k =

subk 1 p (fun arg -&> mulk arg p  (fun arg2 -&> mulk arg2 2 k))


基本上就是按照 Evaluation Order 去函數套函數。
一個複雜一點的例子：
Write a function shiftk that takes a string arguments and a float argument.This function will calculate (q + 1.57)^2 using only arithmetic functions.
let shiftk s q k =

float_addk q 1.57 (

    fun arg1 -&> float_mulk arg1 arg1 (

        fun argT -&> truncatek argT (

            fun argS-&> string_of_intk argS (

                fun argC -&> concatk s argC (

                    fun argCC -&> concatk argCC s k) ))))


就可以這麼寫了。這些 arg1 argT argC argCC 就是隨意的參數名。truncatek 可能不太好理解，其他都是一樣的。
				

 
常用的語言中最適合舉例子的是  JavaScript，像是 C++ 之類的其實還挺尷尬的。JS 社區是用函數式特性用得最歡的社區了。
Reference: Elsa L Gunter

來個簡明補充。
這是個簡單函數計算輸出：
  static int Times3(int x)

    {

        return x * 3;

    }

   Console.WriteLine(Times3(5));


用CPS改造後：

 
static void Times3CPS(int x, Action& continuation)

    {

        continuation(x * 3);

    }

Times3CPS(5, (reslut) =&> Console.WriteLine(result));


CPS可以理解為把程序內部的部分邏輯控制，抽取出來暴露給外部。

（答案抄襲自http://www.cs.indiana.edu/cgi-pub/lkuper/c311/_media/cps-notes.scm）
 定義下面四個函數（為了保持和原答案一致，其實兩個就夠了）
def f(var0):

    pass

def g(var0, var1):

    return pass
def h(var0):

    return pass
def j(var0):

    return pass


若再定義函數
def h_cps(var0, fun0):

    return fun0(h(var0)) # 實際並不是調用h(var0)，只是做和h(var0)一樣的事


那麼f(g(h(1), j(2)))可變換成h_cps(1, lambda x: f(g(x, j(2))))，其中這個lambda x: f(g(x, j(2)))就是Continuation，這個變換就是cps。
另外一個具體的例子：
def rember8(ls):

    """

        返回去掉ls中第一個8的list

    """

    if ls == []:

        return []

    elif ls[0] == 8:

        return ls[1:]

    else:

        return [ls[0]] + rember8(ls[1:])


變一下：
def rember8_cps(ls, fun):

    if ls == []:

        return fun([])

    elif ls[0] == 8:

        return fun(ls[1:])

    else:

        return rember8_cps(ls[1:], lambda x: fun([ls[0]] + x))


假設我們調用下rember8_cps([1,2,8,4,1,5,8,4],lambda x:x)看看每次調用發生了什麼：
#第一次(增加下標以區別)

ls0=[1,2,8,4,1,5,8,4] fun0=lambda x:x

#第二次

ls1=[2,8,4,1,5,8,4] fun1=lambda x:fun0([1]+x)

#第三次

ls2=[8,4,1,5,8,4] fun2=lambda x:fun1([2]+x)


後就返回了fun2([4,1,5,8,4]),一層一層返回回去最後得到了[1,2,4,1,5,8,4]。
實際上就是把原來的一大坨棧變成了一大坨lambda，不知道這麼說對不對？

由於純函數式編程中，不允許使用變數，因此

 
for(int i=0; i &< count; i++) {
  ...

這樣的東西就不能用了，那怎麼辦呢？就用遞歸實現吧。
CPS就是把循環轉換成遞歸的一種形式而已。

CPS變換本質上就是調用一個函數的時候，給它傳入另一個函數（所以，語言必須得支持高階函數和閉包才行），被調函數不把結果返回調用者，而是將結果返回給通過參數傳進來的那個函數。
我不清楚這個概念在別的語言里有沒有實現，或者叫不同的名字。
這裡有個 scheme 的例子：call/cc 探秘

原來就是nodejs各種callback hell，但是這樣做的用途是什麼呢？？
不都是想辦法解決這種callback回調地獄問題么？？

iOS 里的completionHandler:(^blah blah)

 
  推薦閱讀：


※函數式語言的缺陷是什麼?
※為什麼 pattern matching 常常出現在函數式編程語言？
※python協程是什麼？
※為什麼會有函數式編程？
※函數式編程能否解決所有經典的演算法問題？
TAG:Python | 編程 | C | 函數式編程 | Lisp |