摘要：我們每個(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è)谒奚嶙约簩懗绦?#xff0c;對(duì)MFC之類的東西津津樂道，引以為豪。當(dāng)然會(huì)用MFC沒有什么不好，可是如果你完全沉迷于這些東西，恐怕就完全局限于Windows的一些表面現(xiàn)象了。

所以我在大學(xué)的時(shí)候就開始折騰Linux，因?yàn)樗菜谱屛夷軌颉吧钊搿钡接?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的東西”，以及國(guó)內(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í)用”的語言，沒有很多“庫(kù)”可以用，效率也不高，而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)镃ornell的程序語言課是用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，Fw，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)潔。后來我又在課程的 ailing 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)?#xff0c;又必須經(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)的探索，讓我自己的思想得到了解放，翻身成為了這些工具的主人。雖然我看到某些理論工具的研究恐怕早就已經(jīng)到達(dá)路的盡頭，然而它們里面隱含的美卻是無價(jià)和永恒的。這種美讓我對(duì)這個(gè)世界的許多其它方面有了煥然一新的看法。一個(gè)工具的價(jià)值不在于它自己，而在于你如何利用它創(chuàng)造出對(duì)人有益的東西，以及如何讓更多的人掌握它。這就是我打算現(xiàn)在去做的。

總結(jié)

以上是生活随笔為你收集整理的从工具的奴隶到工具的主人的全部?jī)?nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。