我們每個(gè)人都是工具的奴隸。隨著我們的學(xué)習(xí)，我們不斷的加深自己對(duì)工具的認(rèn)識(shí)，從而從它們里面解脫出來。現(xiàn)在我就來說一下我作為各種工具的奴隸，以及逐漸擺脫它們的“思想控制”的歷史吧。

　　當(dāng)我高中畢業(yè)進(jìn)入大學(xué)計(jì)算機(jī)系的時(shí)候，輔導(dǎo)員對(duì)我們說：“你們不要只學(xué)書本知識(shí)，也要多見識(shí)一下業(yè)界的動(dòng)態(tài)，比如去電腦城看看人家怎么裝機(jī)。”當(dāng)然他說我們要多動(dòng)手，多長(zhǎng)見識(shí)，這是對(duì)的。不過如果成天就研究怎么“裝機(jī)”，研究哪種主板配哪種 CPU 之類的東西，你恐怕以后就只有去電腦城賣電腦了。

　　本科的時(shí)候，我經(jīng)常發(fā)現(xiàn)一些同學(xué)不來上數(shù)學(xué)課。后來卻發(fā)現(xiàn)他們?cè)谒奚嶙约簩懗绦颍瑢?duì) MFC 之類的東西津津樂道，引以為豪。當(dāng)然會(huì)用 MFC 沒有什么不好，可是如果你完全沉迷于這些東西，恐怕就完全局限于 Windows 的一些表面現(xiàn)象了。

　　所以我在大學(xué)的時(shí)候就開始折騰 Linux，因?yàn)樗菜谱屛夷軌?ldquo;深入”到計(jì)算機(jī)內(nèi)部。那個(gè)時(shí)候，書店里只有一本 Linux 的書，封面非常簡(jiǎn)陋。這是一本非常古老的書，它教的是怎樣得到 Slackware Linux，然后把它從二三十張軟盤裝到電腦上。總之，我就是這樣開始使用 Linux 的。后來我就走火入魔了，有時(shí)候上課居然在看 GCC 的內(nèi)部結(jié)構(gòu)文檔。后來我又開始折騰 TeX，把 TeXbook 都看了兩遍，恁是用它寫了我的本科畢業(yè)論文。

　　后來進(jìn)了清華，因?yàn)椴粷M意有人嘲笑我用 Linux 這種“像 DOS 的東西”，以及國內(nèi)網(wǎng)站都對(duì) Windows 和 IE 進(jìn)行“優(yōu)化”的情況，就寫了個(gè)“完全用 Linux 工作”。確實(shí)，會(huì) Linux 的人現(xiàn)在更容易找到工作，更容易被人當(dāng)成高手。但是那些工具同樣的奴役了我，經(jīng)常以一些雕蟲小技而自豪，讓我看不到如何才能設(shè)計(jì)出新的，更好的東西。當(dāng)它們的設(shè)計(jì)改變的時(shí)候，我就會(huì)像奴隸一樣被牽著鼻子走。

　　這也許就是為什么我在清華的圖書館發(fā)現(xiàn) 《SICP》 的時(shí)候如此的欣喜。那本書是嶄新的，后面的借書記錄幾乎是空白的。這些看似簡(jiǎn)單的東西教會(huì)我的，卻比那些大部頭和各種 HOWTO 教會(huì)我的更多，因?yàn)樗鼈兘虝?huì)我的是 WHY，而不只是 HOW。當(dāng)時(shí)我就發(fā)現(xiàn)，雖然自認(rèn)為是一個(gè)“資深”的研究生，學(xué)過那么多種程序語言，各種系統(tǒng)工具甚至內(nèi)核實(shí)現(xiàn)，可是相對(duì)于 SICP 的認(rèn)識(shí)深度，我其實(shí)幾乎完全不會(huì)寫程序！在第三章，SICP 教會(huì)了我如何實(shí)現(xiàn)一個(gè)面向?qū)ο笙到y(tǒng)。這是我第一次感覺到自己真正的在開始認(rèn)識(shí)和控制自己所用的工具。

　　因?yàn)橥ǔＨ藗冋J(rèn)為 Scheme 不是一個(gè)“實(shí)用”的語言，沒有很多“庫”可以用，效率也不高，而 Common Lisp 是“工業(yè)標(biāo)準(zhǔn)”，再加上 Paul Graham 文章的慫恿，所以我就開始了解 Common Lisp。在那段時(shí)間，我看了 Paul Graham 的 《On Lisp》 和 Peter Norvig 的 《Paradigms of Artificial Intelligence Programming》。怎么說呢？當(dāng)時(shí)我以為自己學(xué)到很多，可是現(xiàn)在看來，它們教會(huì)我的并沒有 《SICP》 的東西那么精髓和深刻。開頭以為一山還有一山高，最后回頭望去，其實(shí)復(fù)雜的東西并不比簡(jiǎn)單的好。現(xiàn)在當(dāng)我再看 Paul Graham 和 Peter Norvig 的文章，就覺得相當(dāng)幼稚了，而且有很大的宗教成分。

　　進(jìn)入 Cornell 之后，因?yàn)?Cornell 的程序語言課是用 SML 的，我才真正的開始學(xué)習(xí)“靜態(tài)類型”的函數(shù)式語言。之前在清華的時(shí)候，有個(gè)同學(xué)建議我試試 ML 和 Haskell，可是因?yàn)槲覍?duì) Lisp 的執(zhí)著，把他的話當(dāng)成了耳邊風(fēng)。當(dāng)然現(xiàn)在用上 SML 就免不了發(fā)現(xiàn) ML 的類型系統(tǒng)的一些撓人的問題，所以我就開始了解 Haskell，并且由于它看似優(yōu)美的設(shè)計(jì)，我把“終極語言”的希望寄托于它。我開始著迷一些像 monads, type class, lazy evaluation 一類的東西，看 Simon Peyton Jones 的一些關(guān)于函數(shù)式語言編譯器的書。以至于走火入魔，對(duì)其它一切“常規(guī)”語言都持鄙視態(tài)度，看到什么都說“那只不過是個(gè) monad”。雖然有些語言被鄙視是合理的，有些卻是被錯(cuò)怪了的。后來我也發(fā)現(xiàn) monad, type class, lazy evaluation 這些東西其實(shí)并不是什么包治百病的靈丹妙藥。

　　但是我很不喜歡 Cornell 的壓抑氣氛，所以最后決定離開。在不知何去何從的時(shí)候，我發(fā)了一封 email 給曾經(jīng)給過我 fellowship 的 IU 教授 Doug Hofstadter （《GEB》的作者）。我說我不知道該怎么辦，后悔來了 Cornell，我現(xiàn)在對(duì)函數(shù)式語言感興趣。他跟我說，IU 的 Dan Friedman 就是做函數(shù)式語言的啊，你跟他聯(lián)系一下，就說是我介紹你來的。我開頭看過一點(diǎn) The Little Schemer，跟小人書似的，所以還以為 Friedman 是個(gè)年輕小伙。當(dāng)我聯(lián)系上 Friedman 的時(shí)候，他貌似早就認(rèn)識(shí)我了一樣。他說當(dāng)年你的申請(qǐng)材料非常 impressive，可惜你最后沒有選擇我們。你要知道，世界上最重要的不是名氣，而是找到賞識(shí)你，能夠跟你融洽共事的人。你的材料都還在，我會(huì)請(qǐng)委員會(huì)重新考慮你的申請(qǐng)。IU 的名氣實(shí)在不大，而 Friedman 實(shí)在是太謙虛了，所以連跟他打電話都沒有明確表態(tài)想來 IU，只是說“我考慮一下……”這就是我怎么進(jìn)入 IU 的。

　　Friedman 的教學(xué)真的有一手。雖然每個(gè)人對(duì)他看法不同，但是有幾個(gè)最重要的地方他的指點(diǎn)是幫了我大忙的。有人可能想象不到，在 Scheme 這種動(dòng)態(tài)類型語言的“老槽”，其實(shí)有人對(duì)“靜態(tài)類型系統(tǒng)”的理解如此深刻。也就是在 Friedman 的指點(diǎn)下，我發(fā)現(xiàn)類型推導(dǎo)系統(tǒng)不過是一種“抽象解釋”，而各種所謂的“typing rule”，不過是抽象解釋器里面的分支語句。我后來就通過這個(gè)“直覺”，再加上 Friedman 的邏輯語言 miniKanren 里面對(duì)邏輯變量和 unification 的實(shí)現(xiàn)，做出了一個(gè) Hindley-Milner 類型推導(dǎo)系統(tǒng)（HM 系統(tǒng)），也就是 ML 和 Haskell 的類型系統(tǒng)。雖然我在 Cornell 的課程作業(yè)里實(shí)現(xiàn)過一個(gè) HM 系統(tǒng)，但是直到 Friedman 的提點(diǎn)，我才明白了它“為什么”是那個(gè)樣子，以至于達(dá)到更加優(yōu)美的實(shí)現(xiàn)。后來經(jīng)他一句話點(diǎn)撥，我又寫出了一個(gè) lazy evaluation 的解釋器（也就是 Haskell 的語義），才發(fā)現(xiàn)原來 SPJ 的書里所謂的“graph reduction”，不過就是如此簡(jiǎn)單的思想。只不過在 SPJ 的書里，細(xì)節(jié)掩蓋了本質(zhì)。后來我在之前的 HM 系統(tǒng)之上做了一個(gè)非常小的改動(dòng)，就實(shí)現(xiàn)了 type class 的功能，并且比 Haskell 的實(shí)現(xiàn)更加靈活。所以，就此我基本上掌握了 ML 和 Haskell 的理論精髓。

　　可是類型系統(tǒng)卻貌似一個(gè)無止境的東西。在 ML 的系統(tǒng)之上，還有 System F，F(xiàn)w, MLF，Martin Lof Type Theory，CIC，…… 怎么沒完沒了？我一直覺得這些東西過度復(fù)雜，有那個(gè)必要嗎？直到 Amal Ahmed 來到 IU，我才相信了自己的感覺。然而，這卻是以一種“反面”的方式達(dá)到的。

　　Amal 是著名的 Andrew Appel （“虎書”的作者）的學(xué)生，在類型系統(tǒng)和編譯器的邏輯驗(yàn)證方面做過很多工作。可是她比較讓人受不了，她總是顯得好像自己是這里唯一懂得類型的人，而其他人都是類型白癡。她不時(shí)的提到跟 Bob Harper, Benjamin Pierce 等類型大牛一起合作的事情。如果你問她什么問題，她經(jīng)常會(huì)回答你：“Bob Harper 說……”她提到一個(gè)術(shù)語的時(shí)候總是把它說得無比神奇，把它的提出者的名字叫得異常響亮。有一次她上課給我們講 System F，我問她，為什么這個(gè)系統(tǒng)有兩個(gè)“binder”，貌似太復(fù)雜了，為什么不能只用一個(gè)？她沒有正面回答，而是嘲諷似的說：“不是你說可以就可以的。它就是這個(gè)樣子的。”后來我卻發(fā)現(xiàn)其實(shí)有另外一個(gè)系統(tǒng)，它只有一個(gè) binder，而且設(shè)計(jì)得更加簡(jiǎn)潔。后來我又在課程的 mailing list 問了一個(gè)問題，質(zhì)疑一個(gè)編譯器驗(yàn)證方面的概念。本來是純粹的學(xué)術(shù)討論，卻發(fā)現(xiàn)這封 email 根本沒有發(fā)到全班同學(xué)信箱里，被 Amal 給 moderate 掉了！

　　看到這種種詭異的行為，我才意識(shí)到原來學(xué)術(shù)界存在各種“幫派”。即使一些人的理論完全被更簡(jiǎn)單的理論超越，他們也會(huì)為“自己人”的理論說話，讓你搞不清到底什么好，什么不好。所以后來我對(duì)一些類型系統(tǒng)，以及 Hoare Logic 一類的“程序邏輯”產(chǎn)生了懷疑。我的課程 project 報(bào)告，就是指出 Hoare Logic 和 Separation Logic 所能完成的功能，其實(shí)用“符號(hào)執(zhí)行”或者 “model checking” 就能完成。而這些程序邏輯所做的事情，不過是把程序翻譯成了等價(jià)的邏輯表達(dá)式而已。到時(shí)候你要得知這些邏輯表達(dá)式的真?zhèn)危直仨毥?jīng)過一個(gè)類似程序分析的過程，所以這些邏輯只不過讓你白走了一些彎路。當(dāng) Amal 聽完我的報(bào)告，勉強(qiáng)的笑著說：“你告訴了我們這個(gè)結(jié)論，可是你能用它來做什么呢？”我才發(fā)現(xiàn)原來透徹的看法，并不一定能帶來認(rèn)同。人們都太喜歡“發(fā)明”東西，卻不喜歡“歸并”和“簡(jiǎn)化”東西。

　　可是這類型系統(tǒng)的迷霧卻始終沒有散去，像一座大山壓在我頭上。我不滿意 Haskell 和 ML 的類型系統(tǒng)，又覺得 System F 等過于復(fù)雜。可是由于它們的“理論性”和它們創(chuàng)造者的“權(quán)威”，我不敢斷定自己的看法就不是偏頗的。對(duì)付疑惑和恐懼的辦法就是面對(duì)它們，看透它們，消滅它們。于是，我利用一個(gè) independent study 的時(shí)間，獨(dú)立實(shí)現(xiàn)了一個(gè)類型系統(tǒng)。我試圖讓它極度的簡(jiǎn)單，卻又“包羅萬象”。經(jīng)過一番努力，這個(gè)類型系統(tǒng)“涵蓋”了 System F, MLF 以及另外一些類似系統(tǒng)的推導(dǎo)功能，卻不直接“實(shí)現(xiàn)”他們。后來我就開始試圖讓它涵蓋一種非常強(qiáng)大的類型系統(tǒng)，叫做 intersection types。這種類型系統(tǒng)的研究已經(jīng)進(jìn)行了 20 多年，它不需要程序員寫任何類型標(biāo)記，卻可以給任何“停機(jī)”的程序以類型。著名的 Benjamin Pierce 當(dāng)年的博士論文，就是有關(guān) intersection types 的。沒幾天，我就對(duì)自己的系統(tǒng)稍作改動(dòng)，讓它涵蓋了一種最強(qiáng)大的 intersection type 系統(tǒng)（System I）的所有功能。然而我卻很快發(fā)現(xiàn)這個(gè)系統(tǒng)是不能實(shí)用的，因?yàn)樗谶M(jìn)行類型推導(dǎo)的時(shí)候相當(dāng)于是在運(yùn)行這個(gè)程序，這樣類型推導(dǎo)的計(jì)算復(fù)雜度就會(huì)跟這個(gè)程序一樣。這肯定是完全不能接受的。后來我才發(fā)現(xiàn)，原來已經(jīng)有人指出了 System I 的這個(gè)問題。但是由于我事先實(shí)現(xiàn)了這個(gè)系統(tǒng)，所以我直接的看到了這個(gè)結(jié)論，而不需要通過繁瑣的證明。

　　所以，我對(duì)類型推導(dǎo)的探索就這樣到達(dá)了一個(gè)終點(diǎn)。我的類型系統(tǒng)是如此的簡(jiǎn)單，以至于我看到了類型推導(dǎo)的本質(zhì)，而不需要記住復(fù)雜的符號(hào)和推理規(guī)則。我的系統(tǒng)在去掉了 intersection type 之后，仍然比 System F 和 MLF 都要強(qiáng)大。我也看到了 Hindley-Milner 系統(tǒng)里面的一個(gè)嚴(yán)重問題，它導(dǎo)致了這幾十年來很多對(duì)于相關(guān)類型系統(tǒng)的研究，其實(shí)是在解決一個(gè)根本不存在的問題。而自動(dòng)定理證明的研究者們，卻直接的“繞過”了這個(gè)問題。這也就是我為什么開始對(duì)自動(dòng)定理證明開始感興趣。

　　后來對(duì)自動(dòng)定理證明, Partial Evaluation 和 supercompilation 的探索，讓我看到那些看似高深的 Martin Lof Type Theory, Linear Logic 等概念，其實(shí)不過也就是用不同的說法來重復(fù)相同的話題。具體的內(nèi)容我現(xiàn)在還不想談，但是我清楚的看到在“形式化”的美麗外衣下，其實(shí)有很多等價(jià)的，重復(fù)的，無聊的東西。與其繼續(xù)“鉆研”它們，反復(fù)的叨咕差不多的內(nèi)容，還不如用它們的“精髓”來做點(diǎn)有用的事情。

　　所以到現(xiàn)在，我已經(jīng)基本上擺脫了幾乎所有程序語言，編譯器，類型系統(tǒng)，操作系統(tǒng)，邏輯推理系統(tǒng)給我設(shè)置的思維障礙。它們對(duì)我來說不再是什么神物，它們的設(shè)計(jì)者對(duì)我來說也不再是高不可攀的權(quán)威。我很開心，經(jīng)過這段漫長(zhǎng)的探索，讓我自己的思想得到了解放，翻身成為了這些工具的主人。雖然我看到對(duì)這些理論工具的研究恐怕早就已經(jīng)到達(dá)路的盡頭，然而它們里面隱含的美卻是無價(jià)和永恒的。這種美讓我對(duì)這個(gè)世界的許多其它方面有了煥然一新的看法。一個(gè)工具的價(jià)值不在于它自己，而在于你如何利用它創(chuàng)造出對(duì)人有益的東西，以及如何讓更多的人掌握它。這就是我打算現(xiàn)在去做的。

it知識(shí)庫：從工具的奴隸到工具的主人，轉(zhuǎn)載需保留來源！

鄭重聲明：本文版權(quán)歸原作者所有，轉(zhuǎn)載文章僅為傳播更多信息之目的，如作者信息標(biāo)記有誤，請(qǐng)第一時(shí)間聯(lián)系我們修改或刪除，多謝。