王垠 http://blog.sina.com.cn/yinwang0 2012-07-04 22:34:38

0. 寫小人書的老頑童

Dan Friedman 是 Indiana 大學(xué)的教授，Lisp (Scheme)語言的主要研究者之一。他主要的著作《The Little Schemer》（前身叫《The Little Lisper》)是程序語言界最具影響力的書籍之一。現(xiàn)在很多程序語言界的元老級(jí)人物，當(dāng)年都是看這本“小人書”學(xué)會(huì)了Lisp/Scheme，才決心進(jìn)入這一領(lǐng)域。

他對(duì)程序語言的理解，可以說是世界的最高標(biāo)準(zhǔn)。很可惜的是，由于他個(gè)人的低調(diào)（你看這些書的名字，封面，頁數(shù)，價(jià)格，以及里面哄小孩的話，就看得出來），他受到很多人的誤解。很多人以為他只懂得Scheme這種“類型系統(tǒng)落后的語言”。有些人覺得他只顧自己玩，不求“上進(jìn)”，覺得他的研究閉門造車，不“前沿”。我也誤解過他，甚至在見面之前，根據(jù)這些書的封面，我斷定他肯定是個(gè)年輕小伙。結(jié)果呢，第一次見到他的時(shí)候，他已經(jīng)過了60歲大壽。

程序語言的研究者們往往追逐一些“新概念”，卻未能想到，很多這些新概念早在幾十年前就被Friedman 想到了。舉個(gè)例子，Haskell 所用的 lazy evaluation模型，最早就是他在 1976 年在與 David Wise 合寫的論文“CONS should not Evaluate its Arguments”中提出來的。

雖然寫了 The Little Schemer， 但 Friedman 的學(xué)識(shí)并不限于Scheme。他不斷地實(shí)驗(yàn)各種其它的語言設(shè)計(jì)，包括像 ML一類的含有靜態(tài)類型系統(tǒng)的函數(shù)式語言，邏輯式語言，面向?qū)ο笳Z言，用于定理證明的語言等等。在每次的試驗(yàn)之后，他幾乎都會(huì)寫一本書，揭示這些語言最精要的部分。

覺得 ML 比 Scheme 先進(jìn)很多的人們應(yīng)該看看 Friedman 這本書：The Little MLer：想要真正理解 Java 設(shè)計(jì)模式的人，可以看看這本：A Little Java, A Few Patterns: 這些東西的優(yōu)點(diǎn)和弱點(diǎn)，仿佛在他心里都有數(shù)。他幾乎總是指向正確的前進(jìn)方向。

1. 你知道些什么？

可惜的是，由于個(gè)人原因，F(xiàn)riedman 始終沒有成為我正式的導(dǎo)師：Friedman“超然物外”，幾乎完全不關(guān)心自己的學(xué)生什么時(shí)候能畢業(yè)。但他確實(shí)是這一生中教會(huì)我最多東西的人，所以我想寫一些關(guān)于他的小故事。也許你能從中看出，一個(gè)真正的教育者是什么樣子的。我來IU 之前，一位師兄告訴我，Dan Friedman 就像指環(huán)王里的甘道夫(Gandalf)，來了之后發(fā)現(xiàn)確實(shí)很像。

第一次在辦公室見到 Friedman的時(shí)候，他對(duì)我說：“來，給我講講你知道些什么？”我自豪地說：“我在 Cornell上過研究生的程序語言課，會(huì)用 ML 和 Haskell，看過 Paul Graham 的 On Lisp，Peter Norvig 的 Paradigms of Artificial Intelligence Programming, Richard Gabriel 的一些文章...” 他看著我笑了：“不錯(cuò)，你已經(jīng)有一定基礎(chǔ)……”

這么幾年以后，我才發(fā)現(xiàn)他善良的微笑里面，隱藏著難以啟齒的秘密：當(dāng)時(shí)的我是多么的幼稚。在他的這種循循善誘之下，我才逐漸的明白了，知識(shí)的深度是無止境的。他的水平，遠(yuǎn)在以上這些人之上！可是出于謙虛，他不能自己把這話說出來。

2. 反向運(yùn)行

Dan Friedman已經(jīng)遠(yuǎn)遠(yuǎn)超過了退休年齡，仍然堅(jiān)持教學(xué)。他的本科生程序語言課程 C311 是 IU的“星級(jí)課程”。我最敬佩的，是他那孩子般的好奇心和探索精神。幾乎每一年的C311，他都會(huì)發(fā)明不同的東西來充實(shí)課程內(nèi)容。有時(shí)候是一種新的邏輯編程語言(叫 miniKanren)，有時(shí)候是些小技巧 （比如把 Scheme 編譯成 C卻不會(huì)堆棧溢出），等等……

Friedman研究一個(gè)東西的時(shí)候總是全身心的投入，執(zhí)著的熱愛。自從開始設(shè)計(jì)一個(gè)叫miniKanren 的邏輯編程語言，F(xiàn)riedman 多了一句口頭禪：“Does it run backwards?”（能反向運(yùn)行嗎？）因?yàn)檫壿嬍降恼Z言（像Prolog）的程序，都是能“反向運(yùn)行”的。普通程序語言寫的程序，如果你給它一個(gè)輸入，它會(huì)給你一個(gè)輸出。但是邏輯式語言很特別，如果你給它一個(gè)輸出，它可以反過來運(yùn)行，給你所有可能的輸入。但是 Friedman真的走火入魔了。不管別人在講什么，經(jīng)常最后都會(huì)被他問一句：“Does it run backwards?”讓你哭笑不得。

Friedman 有一個(gè)本領(lǐng)域的人都知道的“弱點(diǎn)”——他不喜歡靜態(tài)類型系統(tǒng) (static type system)。其實(shí) Scheme專家們大部分都不喜歡靜態(tài)類型系統(tǒng)。為此，他深受“類型專家”們的誤解甚至鄙視，可是他都從容對(duì)待之。

有一次在他的進(jìn)階課程 B621 上，他給我們出了一道題：用 Scheme 實(shí)現(xiàn) ML 和Haskell 所用的 Hindley-Milner類型系統(tǒng)。這種類型系統(tǒng)的工作原理一般是，輸入一個(gè)程序，它經(jīng)過對(duì)程序進(jìn)行類型推導(dǎo)（type inference），輸出一個(gè)類型。如果程序里有類型錯(cuò)誤，它就會(huì)報(bào)錯(cuò)。由于之前在Cornell 用 ML 實(shí)現(xiàn)過這東西，再加上來到 IU 之后對(duì)抽象解釋 (abstract interpretation) 的進(jìn)一步理解，我很快做出了這個(gè)東西，而且比在 Cornell的時(shí)候做的還要優(yōu)雅。

他知道我做出來了，很高興的樣子，讓我給全班同學(xué)（也就8，9個(gè)人）講我的做法。當(dāng)我自豪的講完，他問：“Does it run backwards?如果我給它一個(gè)類型，它能自動(dòng)生成出符合這個(gè)類型的程序來嗎？”我愣了，欲哭無淚啊，“不能……”他往沙發(fā)靠背上一躺，得意的笑了：“我的系統(tǒng)可以！哈哈！我當(dāng)年寫的那個(gè)類型系統(tǒng)比你這個(gè)還要短呢。我早就知道這些類型系統(tǒng)怎么做，可我就是不喜歡。哈哈哈哈……”

前幾天看了 Stephen Kleene的一篇論文，才發(fā)現(xiàn)原來他說的這種由類型反向算出程序的做法叫做“realizability”，是一個(gè)很深刻的理論，可以用來幫助自動(dòng)證明數(shù)學(xué)定理。而我后來對(duì)類型系統(tǒng)的進(jìn)一步研究顯示，Hindley-Milner類型系統(tǒng)確實(shí)有很多不必要的問題，才導(dǎo)致了他不喜歡。

他就是這樣一個(gè)老頑童。他喜歡先把你捧上天，再把你打下來，讓你知道天外有天:-)

3. miniCoq

你永遠(yuǎn)想象不到 Dan Friedman的思想的極限在哪里。當(dāng)你認(rèn)為他是一個(gè)函數(shù)式語言專家的時(shí)候，他設(shè)計(jì)了miniKanren，一種邏輯式編程語言 (logic programming language)，并且寫出《The Reasoned Schemer》，用于教授邏輯編程。當(dāng)你認(rèn)為他不懂類型系統(tǒng)的時(shí)候，他開始搗鼓最尖端的 Martin-L?f 類型理論，并且開始設(shè)計(jì)機(jī)器證明系統(tǒng)。而他做這些，完全是出于自己的興趣。他從來不在乎別人在這個(gè)方向已經(jīng)做到了什么程度，卻經(jīng)常能出乎意料的簡化別人的設(shè)計(jì)。

有一次系里舉辦教授們的“閃電式演講”(lightening talk)，每位教授只有5分鐘時(shí)間上去介紹自己的研究。輪到 Friedman的時(shí)候，他慢條斯理的走上去，說：“我不著急。我只有幾句話要說。我不知道我能不能拖夠5分鐘……”大家都笑了。他接著說：“我現(xiàn)在最喜歡的東西是 Curry-Howard correspondence 和定理證明。我覺得現(xiàn)在的機(jī)器證明系統(tǒng)太復(fù)雜了，比如Coq 有 nnnnn 行代碼。我想在 x 年之內(nèi)，簡化 Coq，得到一個(gè) miniCoq……”

miniCoq... 聽到這個(gè)詞全場(chǎng)都笑翻了。為什么呢？自己去聯(lián)想Dan \Friedman \的故事 \(3)鈥斺攎iniCoq 從此，“Dan Friedman 的 miniCoq” 成為了 IU 的程序語言學(xué)生茶余飯后的笑話。

但是他沒有吹牛，他總是說到做到。他已經(jīng)寫出一個(gè)簡單的定理證明工具叫JBob（迫于社會(huì)輿論壓力，不能叫 miniCoq），而且正在寫一本書叫 《The Little Prover》，用來教授最重要的定理證明思想。他開始在 C311上給本科生教授這些內(nèi)容。我看了那本書的初稿，獲益至深，那是很多 Coq的教材都不涉及的最精華的道理。它不僅教會(huì)我如何使用定理證明系統(tǒng)，而且教會(huì)了我如何設(shè)計(jì)一個(gè)定理證明系統(tǒng)。我對(duì)他說：“你總是有新的東西教給我們。每隔兩年，我們就得重新上一次你的課！”

4. C311

當(dāng)我剛從 Cornell 轉(zhuǎn)學(xué)到 IU 的時(shí)候，Dan Friedman叫我去上他的研究生程序語言課 B521。我當(dāng)時(shí)以自己在 Cornell上過程序語言課程為由，想不去上他的課。Friedman把我叫到他的辦公室，讓我在他旁邊坐下來，和藹的對(duì)我說：“王垠，我知道你在Cornell 上過這種課。我也知道 Cornell 是比 IU好很多的學(xué)校?？墒敲總€(gè)老師的教學(xué)方法都是不一樣的，你應(yīng)該來上我的課。我和我的朋友們?cè)谶@里做教授，不是因?yàn)橄矚g這個(gè)學(xué)校，而是因?yàn)槲覀兊募胰撕团笥讯荚谶@里。”后來由于跟Amr Sabry（我現(xiàn)在的導(dǎo)師）的課程 B522 時(shí)間重合，他特別安排我坐在本科生的C311的課堂上，卻拿研究生課程的學(xué)分。后來發(fā)現(xiàn)，這兩門課的內(nèi)容基本沒有區(qū)別，只不過研究生的作業(yè)要多一些。

在第一堂課上，他說了一句讓我記憶至今的話：“《The Little Schemer》和《Essentials of Programming Languages》是這門課的參考教材，但是我上課從來不講我的書里的內(nèi)容。”剛一開始，我就發(fā)現(xiàn)這門課跟我在Cornell 學(xué)到的東西很不一樣。雖然有些概念，比如 closure，CPS，我在 Cornell都學(xué)過，在他的課堂上，我卻看到這些概念完全不同的一面，以至于我覺得其實(shí)我之前完全不懂這些概念！這是因?yàn)樵贑ornell 學(xué)到這些東西的時(shí)候只是用來應(yīng)付作業(yè)，而在 Friedman的課上，我利用它們來完成有實(shí)際意義的目標(biāo)，所以才真正的體會(huì)到這些概念的內(nèi)涵和價(jià)值。

一個(gè)例子就是課程進(jìn)入到?jīng)]幾個(gè)星期的時(shí)候，我們開始寫解釋器來執(zhí)行簡單的Scheme 程序。然后我們把這個(gè)解釋器進(jìn)行 CPS 變換，引入全局變量作為"寄存器"(register)，把 CPS 產(chǎn)生的 continuation轉(zhuǎn)換成數(shù)據(jù)結(jié)構(gòu)（也就是堆棧）。最后我們得到的是一個(gè)抽象機(jī) (abstract machine)，而這在本質(zhì)上相當(dāng)于一個(gè)真實(shí)機(jī)器里的中央處理器（CPU）或者虛擬機(jī)（比如JVM）。所以我們其實(shí)從無到有，“發(fā)明”了CPU！從這里，我才真正的理解到寄存器，堆棧等的本質(zhì)，以及我們?yōu)槭裁葱枰鼈儭Ｎ也耪嬲拿靼琢?，馮諾依曼體系構(gòu)架為什么要設(shè)計(jì)成這個(gè)樣子。后來他讓我們?nèi)タ匆黄暮门笥袿livier Danvy 的論文，講述如何從各種不同的解釋器經(jīng)過 CPS變換得出不同種類的抽象機(jī)模型。這是我第一次感覺到程序語言的理論對(duì)于現(xiàn)實(shí)世界的巨大威力，也讓我理解到，機(jī)器并不是計(jì)算的本質(zhì)。機(jī)器可以用任何可行的技術(shù)實(shí)現(xiàn)，比如集成電路，激光，分子，DNA……

但是無論用什么作為機(jī)器的材料，我們所要表達(dá)的語義，也就是計(jì)算的本質(zhì)，卻是不變的。而這些還不是我那屆 C311 全部的內(nèi)容。后半學(xué)期，我們開始學(xué)習(xí)miniKanren，一種他自己設(shè)計(jì)的用于教學(xué)的邏輯式語言 (logic programming language)。這個(gè)語言類似 Prolog，但是它把 Prolog的很多缺點(diǎn)給去掉了，而且變得更加容易理解。教材是免費(fèi)送給我們的《The Reasoned Schemer》。在書的最后，兩頁紙的篇幅，就是整個(gè) miniKanren語言的實(shí)現(xiàn)！我學(xué)得比較快，后來就開始搗鼓這個(gè)實(shí)現(xiàn)，把有些部分重新設(shè)計(jì)了一下，然后加入了一些我想要的功能。這樣的教學(xué)，給了我設(shè)計(jì)邏輯式語言的能力，而不只是停留于一個(gè)使用者。這是學(xué)習(xí)Prolog 不可能做到的事情，因?yàn)?Prolog實(shí)現(xiàn)的復(fù)雜性，會(huì)讓初學(xué)者無從下手，只能停留在使用者的階段。

我很幸運(yùn)當(dāng)初聽了他的話，去上了這門課，否則我就不會(huì)是今天的我。

5. 獨(dú)立思維

Dan Friedman是一個(gè)不隨波逐流，有獨(dú)立思想的人。他的眼里容不下過于復(fù)雜的東西，他喜歡把一個(gè)東西簡化到容得進(jìn)幾行程序，把相關(guān)的問題理解得非常清楚。他的書是一種獨(dú)特的“問答式”的結(jié)構(gòu)，很像孔夫子或者蘇格拉底的講學(xué)方式。他的教學(xué)方式也非常獨(dú)特。這在本科生課程C311 里已經(jīng)有一些表現(xiàn)，但是在研究生的課程 B621 里，才全部的顯示出來。

我寫過的最滿意的一個(gè)程序，自動(dòng) CPS 變換，就是在C311 產(chǎn)生的。在 C311 的作業(yè)里，F(xiàn)riedman 經(jīng)常加入一些“智力題”（brain teaser），做出來了可以加分。因?yàn)槲乙呀?jīng)有一定基礎(chǔ)，所以我有精力來做那些智力題。開頭那些題還不是很難，直到開始學(xué)CPS 的時(shí)候，出現(xiàn)了這么一道：“請(qǐng)寫出一個(gè)叫 CPSer 的程序，它的作用是自動(dòng)的把Scheme 程序轉(zhuǎn)換成 CPS形式。”那次作業(yè)的其它題目都是要求手動(dòng)把程序變成 CPS形式，這道智力題卻要求一個(gè)自動(dòng)的——用一個(gè)程序來轉(zhuǎn)換另一個(gè)程序。我覺得很有意思。如果能寫出一個(gè)自動(dòng)的 CPS轉(zhuǎn)換程序，那我豈不是可以用它完成所有其它的題目了！所以我就開始搗鼓這個(gè)東西，最初的想法其實(shí)就是“模擬”一個(gè)手動(dòng)轉(zhuǎn)換的過程。然后我發(fā)現(xiàn)這真是個(gè)怪物，就那么幾十行程序，不是這里不對(duì)勁，就是那里不對(duì)勁。這里按下去一個(gè)bug，那里又冒出來一個(gè)，從來沒見過這么麻煩的東西。我就跟它死磕了，廢寢忘食幾乎一星期。經(jīng)常走進(jìn)死胡同，就只有重新開始，不知道推翻重來了多少次。到快要交作業(yè)的時(shí)候，我把它給弄出來了。最后我用它生成了所有其它的答案，產(chǎn)生的CPS代碼跟手工轉(zhuǎn)換出來的看不出任何區(qū)別。當(dāng)然我這次我又得了滿分（因?yàn)槊看味甲鲋橇︻}，我的分?jǐn)?shù)總是在100以上）。

作業(yè)發(fā)下來那天下課后，我跟 Friedman 一起走回 Lindley Hall（IU計(jì)算機(jī)系的樓）。半路上他問我：“這次的 brain teaser做了沒有。”我說：“做了。這是個(gè)好東西啊，幫我把其它作業(yè)都做出來了?！彼悬c(diǎn)吃驚，又有點(diǎn)將信將疑的樣子：“你確信你做對(duì)了？”我說：“不確信它是完全正確，但是轉(zhuǎn)換后的作業(yè)程序全都跟手工做的一樣?！弊呋剞k公室之后，他給了我一篇30多頁的論文“Representing control: a study of the CPS transformation”，作者是 OlivierDanvy 和 AndrzejFilinski。然后我才了解到，這是這個(gè)方向最厲害的兩個(gè)人。正是這篇論文，解決了這個(gè)懸而不決十多年的難題。而自動(dòng)的CPS 轉(zhuǎn)換，可以被用于實(shí)現(xiàn)高效的函數(shù)式語言編譯器。Princeton 的 Andrew Appel教授寫了一本書叫《Compiling with Continuations》，就是專門講這個(gè)問題的。而 Amr Sabry（我現(xiàn)在的導(dǎo)師）當(dāng)年的博士論文就是一個(gè)比 CPS還要簡單的變換（叫做 ANF）。憑這個(gè)東西，他幾乎滅掉了這整個(gè)CPS 領(lǐng)域，并且拿到了終身教授職位。Friedman啊，把這樣一個(gè)問題作為“智力題”，真有你的！我開玩笑地對(duì)他說：“我保證，我不會(huì)把這個(gè)程序開源，不然你以后的C311 學(xué)生們就可以拿來作弊了 :-)”回到家，我開始看那篇 Danvy 和 Filinski的論文。這篇 1991 年的論文的想法，是從 1975 年一篇 Gordon Plotkin的論文的基礎(chǔ)上，經(jīng)過一系列繁瑣的推導(dǎo)得出來的。而它最后的結(jié)果，幾乎跟我的程序一模一樣，只不過我的程序可以處理更加復(fù)雜的Scheme，而不只是 lambda calculus。我之前完全不知道 Plotkin的做法，就直接得到了最新的結(jié)果。這是我第一次認(rèn)識(shí)到自己頭腦的威力。

第二個(gè)學(xué)期，當(dāng)我去上 Friedman 的進(jìn)階課程 B621的時(shí)候，他給我們出了同樣的題目。兩個(gè)星期下來，沒有其它人真正的做對(duì)了。最后他對(duì)全班同學(xué)說：“現(xiàn)在請(qǐng)王垠給大家講一下他的做法。你們要聽仔細(xì)了哦。這個(gè)程序價(jià)值100美元！”而這還不是 B621 的全部，每一個(gè)星期，F(xiàn)riedman會(huì)在黑板上寫下一道很難的題目。他不讓你看書或者看論文。他有時(shí)甚至不告訴你題目里相關(guān)概念的名字，或者給它們起個(gè)新名字，讓你想查都查不到。他要求你完全靠自己把這些難題解出來，下一個(gè)星期的時(shí)候在黑板上給其它同學(xué)講解。他沒有明確的評(píng)分標(biāo)準(zhǔn)，讓你感覺完全沒有成績的壓力。這些題目包括很難的一些問題，比如 church numeral 的前驅(qū)(predecessor)。這個(gè)問題，當(dāng)年是 Stephen Kleene花了三個(gè)月冥思苦想才做出來的。不幸的是，我早就學(xué)到了 Kleene的做法，造成了思維的定勢(shì)，所以這個(gè)訓(xùn)練當(dāng)時(shí)對(duì)我來說失去了意義。而我們班上卻有一個(gè)數(shù)學(xué)系的同學(xué)，出人意料的在一個(gè)星期之內(nèi)做出了一個(gè)比Kleene 還要簡單的方法。其它的問題包括從 lambda calculus 到 SKI combinator 的編譯器，邏輯式（可逆）CPS變換，實(shí)現(xiàn) Hindley-Milner 類型系統(tǒng)，等等。我發(fā)現(xiàn)，就算自認(rèn)為明白了的東西，經(jīng)過一番思索，認(rèn)識(shí)居然還可以更進(jìn)一步。

當(dāng)然，重新發(fā)明東西并不會(huì)給我?guī)碚撐陌l(fā)表，但是它卻給我?guī)砹烁匾臇|西，這就是獨(dú)立的思考能力。一旦一個(gè)東西被你“想”出來，而不是從別人那里“學(xué)”過來，那么你就知道這個(gè)想法是如何產(chǎn)生的。這比起直接學(xué)會(huì)這個(gè)想法要有用很多，因?yàn)槟阒肋@里面所有的細(xì)節(jié)和犯過的錯(cuò)誤。而最重要的，其實(shí)是由此得到的直覺。如果直接去看別人的書或者論文，你就很難得到這種直覺，因?yàn)橐话闳藢懻撐亩紩?huì)把直覺埋藏在一堆符號(hào)公式之下，讓你看不到背后的真實(shí)想法。如果得到了直覺，下一次遇到類似的問題，你就有可能很快的利用已有的直覺來解決新的問題。

而這一切都已經(jīng)發(fā)生在我身上。比如，在聽說 ANF 之后，我沒有看 Amr Sabry的論文，只把原來的 CPSer 程序改了一點(diǎn)點(diǎn)，就得到了 ANF變換，整個(gè)過程只花了十幾分鐘。而在 R. Kent Dybvig 的編譯器課程上，我利用CPS 變換里面的直覺，改造和合并了 Dybvig 提供的編譯器框架的好幾個(gè)pass，使得它們變得比原來短小好幾倍，而且生成很不錯(cuò)的代碼。

現(xiàn)在我仍然是這樣，喜歡故意重新發(fā)明一些東西，探索不止一個(gè)領(lǐng)域。這讓我獲得了直覺，不再受別人思想的限制，節(jié)省了看論文的時(shí)間，而且多了一些樂趣。一個(gè)問題，當(dāng)我相信自己能想得出來，一般都能解決。雖然我經(jīng)常不把我埋頭做出來的東西放在心上，把它們叫做“重新發(fā)明”(reinvention)，但是出乎意料的是，最近我發(fā)現(xiàn)這里面其實(shí)很是隱藏了一些真正的發(fā)明。我準(zhǔn)備慢慢把其中一些想法發(fā)掘整理出來，發(fā)表成論文，或者做成產(chǎn)品。

俗話說，“授人以魚，不如授人以漁?！本褪沁@個(gè)道理吧。Dan Friedman，謝謝你教會(huì)我釣魚。

本文地址：http://blog.sina.com.cn/s/blog\_5d90e82f010177qx.html