函數式編程的早期歷史

有個叫 David Hilbert (希爾伯特)的德國人，1900 年在巴黎數學家大會上拋出了 10 個世紀難題，會後又加了一堆，合稱 Hilbert 23 problems。

其中Hilbert 第 10 問題 (指的是 23 問題清單上的第 10 個)，一直懸而未決。1928 年在 義大利波倫亞舉行的數學家大會上，Hilbert 和 Wilhelm Ackermann (阿克曼)發表了 "Principles of Mathematical Logic"，其中 Hilbert 10th 問題給出了更為形式化的描述，細化成三個子問題：

First, was mathematics complete ... Second, was mathematics consistent ... And thirdly, was mathematics decidable?" (Hodges p. 91, Hawking p. 1121)

時年 22 歲的 Kurt G?del (哥德爾)在會上聽了 Hilbert 的演講後，就決定拿這個問題做博士論文了。1929 年他完成了論文，證明了一階謂詞演算中所有邏輯上有效的公式都是可以證明的。這個一階謂詞演算完備性，也就被稱為哥德爾完備性定理。然後，1930 年他順利地在維也納拿到了博士學位。

1930 年 9 月 8 日，在德國柯尼斯堡召開了一次三個科學社區的聯合會議。已經 68 歲、被哥廷根(G?ttingen)大學強制退休的 Hilbert 做開幕致辭，也是他的退休演講。這次會議第三天的一個圓桌討論上 Kurt G?del 闡述了他的不完備性定理，解決了前兩點，並於次年發表了題為「On Formally Undecidable Propositions in Principia Mathematica and Related Systems I」的論文，正如名字所示，他當時想著要寫個 II 的，不過從來沒真正動手寫。

在這部長篇大論里，G?del 首先證明了一個形式系統中的所有公式都可以表示為自然數，並可以從自然數反過來得出相應的公式。這對於今天的程序員都來說，數字編碼、程序即數據計算機原理，這些最核心、最基本的常識，在那個時代卻是腦洞大開的創見。運用這個編碼系統，G?del 證明在系統 T 內可以形式化定義命題 P (我在系統 T 內不可被證明)，從而給確定性問題給出了否定回答。(過程太啰嗦，想了解細節請看劉未鵬的長文)

第3點則被稱為 Entscheidungsproblem (發音 [?nt??a??d??sp?o?ble?m], 是 decision problem 的德文說法)。要解決 Entscheidungsproblem 問題，首先要提供 effective computation 的數學定義。

Entscheidungsproblem 引起了許多數學家的興趣。其中有兩個現在廣為人知，一個叫 Alan Turing (圖靈)，一個叫 Alonzo Church (丘奇)，兩人在同在1936年獨立給出了否定答案。

Alan Turing 1935 年跑去聽 Max Newman (紐曼)講「數學的基礎」高級課程，從而迷上了確定性問題，並發明了圖靈機模型來定義有效計算。Universal turing machine 模型是一個通用計算機模型，這是劃時代的進步。圖靈機隱含了存儲計算的機器模型，這深刻的影響了 Manchester、EDVAC、ENIAC 等機器的建造者，圖靈本人後來還親自操刀了 ACE 機器的設計。總之，基於存儲計算的通用計算機由此發源，然後才有了日後興旺發達的編程行業。

而 Church 在 1933 年就搞出來一套以純λ演算為基礎的邏輯，以期對數學進行形式化描述，他學生 Stephen Kleene 和J. Barkley Rosser 隨後提出 Kleene–Rosser 悖論，證明最初的系統不自洽。好在純λ演算部分是自洽的，Kleene 試圖在λ演算系統里重現 G?del 不完備定理時，搞定了用 λ 演算來表達算術和遞歸函數。這些成績將 λ演算的研究引向了λ可定義性(definability)。

1934 年 G?del 來到普林斯頓訪問。3 月時，Church 向他提出可以用 λ可定義來表達有效運算的猜想， G?del 對此深表懷疑。1931 年 G?del 在不完全定理論文中已經引了入原始遞歸函數(primitive recursive function)， 這時候他進一步將其一般化成為通用遞歸函數，加上了兩個約束而使之成為有效的(effective)，形成了通用遞歸模型。

由於 G?del 1934 年演講時表示核心概念來自 Jacques Herbrand (厄布朗)在 4 月 7 日 信件里跟他探討的內容，所以稱為 G?del-Herbrand recursive function。本來這裡有一段凄美的故事，丫拖到當年 7.25 才給 Herbrand 回信，可惜 Herbrand 7.27 就在 Alps 登山時意外身亡了，1932 年 Herbrand 前一年提交的論文在身後發表。不過呢，最早那封信 1986 年被人翻出來了，2004年 CMU 的 Wilfried Sieg 研究後發現，貌似 G?del 記錯了，信裡面討論的其實是 G?del 第二不完備定理與 Hilbert 形式系統的衝突，這個通用遞歸系統極有可能是 G?del 自己折騰出來的 (https://www.cmu.edu/dietrich/philosophy/docs/tech-reports/152_Sieg.pdf)。不過，這倒不影響 Herbrand 的天才啦，雖然 23 歲就英年早逝，但發的兩篇論文已經對數學的基礎做出根本性的貢獻，有用他名字命名的定理。那為毛 Wilfried Sieg 後來要專門寫個文公布這事兒呢？因為他 1994 年寫了篇文章說 Herbrand 跟 G?del 之間這樁軼事，還老被人引用，這誰能受得了呀。

而 G?del 對 Church 的λ演算系統的懷疑，也促使 Church 師徒去證明任何遞歸函數都是都是 λ可定義的，這就是 λ可定義模型。1935 年 Church 向數學界宣布他的論題時其實還不是很確定，直到 1936 年發表的文章才正真確認了這一論點。

簡單說來，λ演算是一個更符合數學公式表達習慣的系統，因此在 1960 年代之前，這套東東主要是數學家們玩，跟計算機編程沒啥關聯。而 G?del 更欣賞 Turing 的模型，是因為圖靈機對計算的表達更加直接。

1935/36 這個時間段上，我們有了三個有效計算模型：通用圖靈機、通用遞歸函數、λ可定義。Rosser 1939 年正式確認這三個模型是等效的。

值得一提的是，圖靈 1936 年 5.28 向"Proceedings of the London Mathematical Society"提交了論文"On Computable Numbers, with an application to the Entscheidungsproblem"，不過因為 Church 在美國早一步發表了"An unsolvable problem in elementary number theory"，這篇對基礎數學和計算機兩個領域都極其重要的文章發表得並不順利。儘管 Newman 費勁巴拉的解釋兩者的方法完全不同，圖靈還是不得不修改論文，加了個附錄引述了 Church 的工作，並證明兩者是等價的，1936 年 11 月 12 日正式提交，1937 年才得以付印出版。在修改過程中，圖靈了解到普林斯頓那邊兒除了 Church 還有 G?del, Kleene (克萊尼), Rosser (羅瑟) 以及 Bernays (奈斯)等一堆邏輯學研究者，於是興沖沖跑去當 graduated student，去了才失望的發現除了 Church 其他人前一年都離開了。而 Church 也就當收了個掛單和尚，所以兩個人關係並不親密。圖靈在這裡拿到了博士學位，學位論文里意外的提到了一個不動點組合子Θ，這是第一個公開發表的不動點組合子。

前邊已經多次提到函數，這全都是數學意義上的函數，最早的定義可以追溯到 1889 年 Giuseppe Peano (皮亞諾)，儘管對函數和類(指變數值的集合)的抽象符號一直在發展，但都沒有對 substitution 和 convension 提供形式化定義，要等到 1920 年代組合子邏輯和更晚的 λ演算出現時才給出。

Hilbert 研究組裡的 Sch?nfinkel 1920 年 12.7 演講中就已經提出了組合子邏輯(combinatory logic)，1924 年他的同事 Heinrich Behmann (貝曼)整理成文發表了。不過他後來回了莫斯科，1927年發現他因為精神疾病而在住院治療，只在 1929 發過一篇論文，最終在 1942 年貧病而死。二戰惡劣的生存環境下鄰居拿他的研究手稿去燒火取暖…… 一直等到 Curry Haskell (柯里) 1927 在普林斯頓大學當講師時，才重新發現了 Moses Sch?nfinkel 關於組合子邏輯的成果。Moses Sch?nfinkel 的成果預言了很多 Curry 在做的研究，於是他就跑去哥廷根大學與熟悉 Moses Sch?nfinkel 工作的 Heinrich Behmann、Paul Bernays 兩人一起工作，並於 1930 年以一篇組合子邏輯的論文拿到了博士學位。

Curry Brooks Haskell 整個職業生涯都在研究組合子，實際開創了這個研究領域，λ演算中用單參數函數來表示多個參數函數的方法被稱為 Currying (柯里化)，雖然 Curry 同學多次指出這個其實是 Sch?nfinkel 已經搞出來的，不過其他人都是因為他用了才知道，所以這名字就這定下來了；後來有三門編程語言以他的名字命名，分別是：Curry, Brooks, Haskell。

Curry 在 1928 開始開發類型系統，他搞的是基於組合子的 polymorphic，Church 則建立了基於函數的簡單類型系統。

程序正確性證明和程序驗證，它的一些基本概念和方法是 40 年代後期諾伊曼和圖靈等人提出的。諾伊曼等在一篇論文中提出藉助於證明來驗證程序正確性的方法。後來圖靈又證明了一個子程序的正確性。不過圖靈的這一成果長期不受重視。

通用計算機誕生之後，大家都發現直接折騰機器碼實在是沒效率了，於是搞出了符號彙編語言，但是表達邏輯還是太不直接了。於是 1952 年 Halcombe Laning 提出了直接輸入數學公式的設想，並製作了 GEORGE 編譯器演示該想法。受這個想法啟發，1953 年 IBM 的 John Backus 組建了一支強大的隊伍開始給 IBM 704 主機研發數學公式翻譯系統，1954 年中發布了規範草稿，並在 1956 年 10 月編製出使用手冊，第一個 FORTRAN (FORmula TRANslating 的縮寫)編譯器 1957.4 正式發行。FORTRAN 程序的代碼行數比彙編少 20 倍，儘管大家懷疑編譯器生成代碼的性能會不如手寫(那會兒機時很貴)，還是迅速流行開了。

FORTRAN 的成功，讓很多人認識到直接把代數公式輸入進電腦是可行的，並開始渴望能用某種形式語言直接把自己的研究內容輸入到電腦里進行運算。

John McCarthy 1956 年在 Dartmouth 的一台 IBM 704 上搞人工智慧研究時，就想到要一個代數列表處理(algebraic list processing)語言。他的項目需要用某種形式語言來編寫語句，以記錄關於世界的信息，而他感覺列表結構這種形式挺合適，既方便編寫，也方便推演。做為 IBM plane geometry 項目的顧問，他先忽悠 Herbert Gelernter 和 Carl Gerberin 給 FORTRAN 加上了 list processing，搞出了 FLPL (FORTRAN List Processing Language)，並在該項目中成功應用。

** 正因為是在 IBM 704 上開搞的，所以 LISP 的表處理函數才會有奇葩的名字： car/cdr 什麼的。其實是取 IBM704 機器字的不同部分，c=content of，r=register number, a=address part, d=decrement part (http://www.iwriteiam.nl/HaCAR_CDR.html)

不過 1957~58 年間親自拿 FORTRAN 寫了個國際象棋程序之後，覺得還是太麻煩，於是他 58 年整個夏天都泡在 IBM 的信息研究部琢磨新的語言，以免去自己人工將列表結構翻譯成 FORTRAN 程序的麻煩。這種新的編程語言有很多創造性的特性，John McCarthy 提到：

* 用條件表達式來寫遞歸函數 (Church 是用高階函數的)

* 使用 Church 1941 的符號來表示函數，以便將函數做為參數傳遞

* 因為看不懂 Church 書里其餘的部分，所以就不掂記著實現他那個更通用的函數定義方式了

(也就是除了用 lambda 關鍵字，其實 最早的 LISP 不是基於 λ演算實現的，理論基礎是 Kleene 的一階遞歸函數，不過現在的 LISP 實現都是基於 lambda calculus 的了)

這個列表處理語言就叫 LISP。等等，好不容易想得挺美了，可是 IBM 的傢伙們對 FLPL 已經很滿意了，居然忽悠不動了！

1958 秋天，John McCarthy 在 MIT EE 混上了 Assistant Professor，跟數學系的 Marvin Minsky 一起立了個人工智慧的項目，開始自己實現 LISP 。這段故事很長，自己去看吧，這裡就提一個，數學上的函數應該結果只跟傳入的參數有關，不受其它狀態的影響，除了返回值也不影響其它地方的狀態，這叫沒有副作用，但是實際程序里副作用卻能極為方便的提升執行效率，糾結呀，最後 LISP 里還是有副作用的。不過有數學潔癖的這幫傢伙後來(1976~1978)論證了 Pure LISP 是可以不支持副作用的，這樣才能方便的用一階謂語邏輯去證明程序的性質。

John McCarthy 對圖靈機當然也是很熟悉的，他還很得意的指出， 要顯擺 LISP 比圖靈機簡潔，實現一下 universal LISP function 就明白了嘛，比 universal Turing machine 要簡潔好理解就對了。這個就是 LISP 的 eval 函數啦。結果為了實現 eval，Nathaniel Rochester 先發明了 LABEL，以便可以用 LISP 數據來表示 LISP 函數，D.M.R. Part 接著指出用 Church 的 Y 運算元其實光用 λ 不用 LABEL 也能搞定。然後， S.R. Russell 發現，這個 eval 實現完全可以當 LISP 解釋器嘛。

LISP 開發者們機智的採用了逐步 bootstrap LISP 的實現策略，後來又有了解釋器，最後 Timothy Hart and Michael Levin 拿 LISP 寫出了第一個能工作的 LISP 編譯器，這也是世界上第一個用被編譯語言寫的編譯器。LISP 影響很大，後來衍生出 CommonLisp, Scheme 等許多方言。1978 年對自由變數綁定問題(FUNARG)的分析，讓大家認識到元編程與高階編程是不一樣的，這也是 LISP 的一大貢獻。

不過，儘管 LISP 各種牛叉，在數字計算上比 FORTRAN 慢 10 到 100 倍也是要了命了。而且，遞歸式的表達式，看起來也沒有命令式的直觀易懂。所以，在工程應用方面應用比較有限。

1955 年開始，搞演算法研究的人們就在探討能直接書寫演算法的編程語言，歐美的計算機科學家們 1958 年在 ETH Zurich 開了個會，建立了一個委員會來定義一種通用高級編程語言，稱為 ALGOL (ALGOrithmic Language) ，1958 年首次發表的報告稱為 ALGOL58。1959 年在巴黎又開了次會，定下了 ALGOL60，這個才真正有實現，後來還有個 ALGOL68 不過沒人鳥，所以今天說 ALGOL 就是指 ALGOL60。

John Backus 為了形式化的描述 ALGOL58 語法規範，發明了 Backus normal form，Peter Naur 在描述 ALGOL60 時進行了修改和擴展，後來 Donald Knuth 建議改名為 Backus-Naur normal form，簡稱 BNF範式，搞文法的都少不了要用到的。Naur 等在研究 Label 實現時搞出來 program point 的概念，後來演變成了 continuation。Niklaus Wirth 1966年發展了 ALGOL W，因為 IBM 覺得太超前沒要，他後來改吧改吧變成了 Pascal 。

ALGOL 是相當超前的，這是第一個結合了命令式和 λ演算的編程語言。儘管一般不認為 ALGOL 是函數式語言，但是它確實實現了 call-by-name，Naur 1964 更訂版 ALGOL60 規範精確定義了過程調用的效果，跟 λ演算的 β-reduction 完全一致，它的變數綁定也跟 λ 的規則很相近，1964 年 Landin 給實現了 closure 。

從 1964 年的"The Mechanical Evaluation of Expressions"開始，Landin 寫了一系列論文研究編程語言與 λ演算之間的關係，並發明了第一個函數式抽像機器 SECD(1965 Correspondence between ALGOL 60 and Churchs Lambda-notation I/II)，並從 66 年的The Next 700 Programming Languages"開始闡述他理想中的編程語言 ISWIM(if you see what I mean)，基本上就是sugared lambda + assignment + control 。

John Backus 在1970年代搞了 FP 語言，1977 年發表。雖然這門語言並不是最早的函數式編程語言，但他是 Functional Programming 這個詞兒的創造者， 1977 年他的圖靈獎演講題為(Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs)。

1973 年 Robin Milner 的研究組在 Edinburgh University 搞了 ML (Meta Language) 用以研究 LCF(Logic for Computable Functions)，後來演變出 OCaml 和 Standard ML。[From LCF to HCL](http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf)

1974 年 MIT 的 Barbara Liskov 帶著學生搞出了 CLU 語言，這個語言帶有 cluster (早期的類實現)、異常處理機制、iterator、最早的 generator (yield)。

76年左右，大家開始關注 Laziness。

而 1987 年從美國俄勒岡州波特蘭(in Portland, Oregon)召開的函數式編程語言與計算架構會議(FPCA 87 )開始，建立函數式編程開放標準的運動開始了，形成了 Haskell，不過只是書面規範，要到 1990 才開始有實現。

參考資料：(參考了太多，有一些隨手記過來了，更多的當時沒有記，現在也懶得再一一找回來了，見諒。)

推薦閱讀：