作者：王垠
? 當(dāng)我高中畢業(yè)進(jìn)入大學(xué)計(jì)算機(jī)系的時(shí)候公你，輔導(dǎo)員對(duì)我們說(shuō)：“你們不要只學(xué)書本知識(shí)慌植，也要多見(jiàn)識(shí)一下業(yè)界的動(dòng)態(tài)休雌，比如去電腦城看看人家怎么裝機(jī)灶壶。”當(dāng)然他說(shuō)我們要多動(dòng)手杈曲，多長(zhǎng)見(jiàn)識(shí)驰凛，這是對(duì)的。不過(guò)如果成天就研究怎么“裝機(jī)”担扑，研究哪種主板配哪種 CPU 之類的東西恰响，你恐怕以后就只有去電腦城賣電腦了。
本科的時(shí)候涌献，我經(jīng)常發(fā)現(xiàn)一些同學(xué)不來(lái)上數(shù)學(xué)課胚宦。后來(lái)卻發(fā)現(xiàn)他們?cè)谒奚嶙约簩懗绦颍瑢?duì)MFC之類的東西津津樂(lè)道燕垃，引以為豪枢劝。當(dāng)然會(huì)用MFC沒(méi)有什么不好，可是如果你完全沉迷于這些東西卜壕，恐怕就完全局限于Windows的一些表面現(xiàn)象了您旁。
? ?所以我在大學(xué)的時(shí)候就開(kāi)始折騰Linux，因?yàn)樗菜谱屛夷軌颉吧钊搿钡接?jì)算機(jī)內(nèi)部轴捎。那個(gè)時(shí)候鹤盒，書店里只有一本 Linux 的書，封面非常簡(jiǎn)陋侦副。這是一本非常古老的書侦锯，它教的是怎樣得到Slackware Linux，然后把它從二三十張軟盤裝到電腦上跃洛÷蚀ィ總之终议，我就是這樣開(kāi)始使用Linux的汇竭。后來(lái)我就走火入魔了，有時(shí)候上課居然在看GCC的內(nèi)部結(jié)構(gòu)文檔穴张。后來(lái)我又開(kāi)始折騰TeX细燎，把TeXbook都看了兩遍，恁是用它寫了我的本科畢業(yè)論文皂甘。
? 后來(lái)進(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é)過(guò)那么多種程序語(yǔ)言攻旦，各種系統(tǒng)工具甚至內(nèi)核實(shí)現(xiàn)，可是相對(duì)于SICP的認(rèn)識(shí)深度生逸，我其實(shí)幾乎完全不會(huì)寫程序牢屋！在第三章，SICP?教會(huì)了我如何實(shí)現(xiàn)一個(gè)面向?qū)ο笙到y(tǒng)槽袄。這是我第一次感覺(jué)到自己真正的在開(kāi)始認(rèn)識(shí)和控制自己所用的工具烙无。
? 因?yàn)橥ǔＨ藗冋J(rèn)為Scheme不是一個(gè)“實(shí)用”的語(yǔ)言，沒(méi)有很多“庫(kù)”可以用遍尺，效率也不高截酷，而Common Lisp是“工業(yè)標(biāo)準(zhǔn)”，再加上Paul Graham文章的慫恿乾戏，所以我就開(kāi)始了解Common Lisp迂苛。在那段時(shí)間，我看了Paul Graham的《On Lisp》和Peter Norvig的?《Paradigms of Artificial Intelligence Programming》鼓择。怎么說(shuō)呢三幻？當(dāng)時(shí)我以為自己學(xué)到很多，可是現(xiàn)在看來(lái)呐能，它們教會(huì)我的并沒(méi)有《SICP》的東西那么精髓和深刻念搬。開(kāi)頭以為一山還有一山高，最后回頭望去，其實(shí)復(fù)雜的東西并不比簡(jiǎn)單的好±驶玻現(xiàn)在當(dāng)我再看Paul Graham和Peter Norvig的文章首妖，就覺(jué)得相當(dāng)幼稚了，而且有很大的宗教成分爷恳。
? ?進(jìn)入Cornell之后悯搔，因?yàn)镃ornell的程序語(yǔ)言課是用SML的，我才真正的開(kāi)始學(xué)習(xí)“靜態(tài)類型”的函數(shù)式語(yǔ)言舌仍。之前在清華的時(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)的一些撓人的問(wèn)題，所以我就開(kāi)始了解Haskell节芥，并且由于它看似優(yōu)美的設(shè)計(jì)在刺，我把“終極語(yǔ)言”的希望寄托于它。我開(kāi)始著迷一些像monads头镊，type class蚣驼，lazy evaluation 一類的東西，看Simon Peyton Jones的一些關(guān)于函數(shù)式語(yǔ)言編譯器的書相艇。以至于走火入魔颖杏，對(duì)其它一切“常規(guī)”語(yǔ)言都持鄙視態(tài)度，看到什么都說(shuō)“那只不過(guò)是個(gè)monad”坛芽。雖然有些語(yǔ)言被鄙視是合理的留储，有些卻是被錯(cuò)怪了的。后來(lái)我也發(fā)現(xiàn)monad, type class, lazy evaluation這些東西其實(shí)并不是什么包治百病的靈丹妙藥咙轩。
? ? 但是我很不喜歡Cornell的壓抑氣氛获讳，所以最后決定離開(kāi)。在不知何去何從的時(shí)候活喊，我發(fā)了一封email給曾經(jīng)給過(guò)我fellowship的IU教授Doug Hofstadter（《GEB》的作者）丐膝。我說(shuō)我不知道該怎么辦，后悔來(lái)了 Cornell钾菊，我現(xiàn)在對(duì)函數(shù)式語(yǔ)言感興趣帅矗。他跟我說(shuō)，IU的Dan Friedman就是做函數(shù)式語(yǔ)言的啊结缚，你跟他聯(lián)系一下损晤，就說(shuō)是我介紹你來(lái)的。我開(kāi)頭看過(guò)一點(diǎn)The Little Schemer红竭，跟小人書似的，所以還以為Friedman是個(gè)年輕小伙。當(dāng)我聯(lián)系上Friedman的時(shí)候茵宪，他貌似早就認(rèn)識(shí)我了一樣最冰。他說(shuō)當(dāng)年你的申請(qǐng)材料非常impressive，可惜你最后沒(méi)有選擇我們稀火。你要知道暖哨，世界上最重要的不是名氣，而是找到賞識(shí)你凰狞，能夠跟你融洽共事的人篇裁。你的材料都還在，我會(huì)請(qǐng)委員會(huì)重新考慮你的申請(qǐng)赡若。IU 的名氣實(shí)在不大达布，而Friedman?實(shí)在是太謙虛了，所以連跟他打電話都沒(méi)有明確表態(tài)想來(lái)IU逾冬，只是說(shuō)“我考慮一下……”這就是我怎么進(jìn)入IU的黍聂。
? Friedman的教學(xué)真的有一手。雖然每個(gè)人對(duì)他看法不同身腻，但是有幾個(gè)最重要的地方他的指點(diǎn)是幫了我大忙的产还。有人可能想象不到，在Scheme這種動(dòng)態(tài)類型語(yǔ)言的“老槽”嘀趟，其實(shí)有人對(duì)“靜態(tài)類型系統(tǒng)”的理解如此深刻脐区。也就是在Friedman的指點(diǎn)下，我發(fā)現(xiàn)類型推導(dǎo)系統(tǒng)不過(guò)是一種“抽象解釋”她按，而各種所謂的“typing rule”坡椒，不過(guò)是抽象解釋器里面的分支語(yǔ)句。我后來(lái)就通過(guò)這個(gè)“直覺(jué)”尤溜，再加上Friedman的邏輯語(yǔ)言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)過(guò)一個(gè)HM系統(tǒng)丈攒，但是直到Friedman的提點(diǎn)，我才明白了它“為什么”是那個(gè)樣子授霸，以至于達(dá)到更加優(yōu)美的實(shí)現(xiàn)巡验。后來(lái)經(jīng)他一句話點(diǎn)撥，我又寫出了一個(gè)lazy evaluation的解釋器（也就是Haskell的語(yǔ)義）碘耳，才發(fā)現(xiàn)原來(lái)SPJ的書里所謂的“graph reduction”显设，不過(guò)就是如此簡(jiǎn)單的思想。只不過(guò)在SPJ的書里辛辨，細(xì)節(jié)掩蓋了本質(zhì)捕捂。后來(lái)我在之前的HM系統(tǒng)之上做了一個(gè)非常小的改動(dòng)瑟枫，就實(shí)現(xiàn)了type class的功能，并且比Haskell的實(shí)現(xiàn)更加靈活指攒。所以慷妙，就此我基本上掌握了ML和Haskell的理論精髓。
? ? ? 可是類型系統(tǒng)卻貌似一個(gè)無(wú)止境的東西允悦。在ML的系統(tǒng)之上膝擂，還有System F，F(xiàn)w隙弛，MLF架馋，Martin Lof Type Theory，CIC全闷，……怎么沒(méi)完沒(méi)了叉寂？我一直覺(jué)得這些東西過(guò)度復(fù)雜，有那個(gè)必要嗎室埋？直到Amal Ahmed來(lái)到IU办绝，我才相信了自己的感覺(jué)。然而姚淆，這卻是以一種“反面”的方式達(dá)到的孕蝉。
? ? Amal是著名的Andrew Appel（“虎書”的作者）的學(xué)生，在類型系統(tǒng)和編譯器的邏輯驗(yàn)證方面做過(guò)很多工作腌逢〗祷矗可是她比較讓人受不了，她總是顯得好像自己是這里唯一懂得類型的人搏讶，而其他人都是類型白癡佳鳖。她不時(shí)的提到跟Bob Harper, Benjamin Pierce等類型大牛一起合作的事情。如果你問(wèn)她什么問(wèn)題媒惕，她經(jīng)常會(huì)回答你：“Bob Harper說(shuō)……”她提到一個(gè)術(shù)語(yǔ)的時(shí)候總是把它說(shuō)得無(wú)比神奇系吩，把它的提出者的名字叫得異常響亮。有一次她上課給我們講System F妒蔚，我問(wèn)她穿挨，為什么這個(gè)系統(tǒng)有兩個(gè)“binder”，貌似太復(fù)雜了肴盏，為什么不能只用一個(gè)科盛？她沒(méi)有正面回答，而是嘲諷似的說(shuō)：“不是你說(shuō)可以就可以的菜皂。它就是這個(gè)樣子的贞绵。”后來(lái)我卻發(fā)現(xiàn)其實(shí)有另外一個(gè)系統(tǒng)恍飘，它只有一個(gè)binder榨崩，而且設(shè)計(jì)得更加簡(jiǎn)潔谴垫。后來(lái)我又在課程的 ailing list 了一個(gè)問(wèn)題，質(zhì)疑一個(gè)編譯器驗(yàn)證方面的概念蜡饵。本來(lái)是純粹的學(xué)術(shù)討論弹渔，卻發(fā)現(xiàn)這封email根本沒(méi)有發(fā)到全班同學(xué)信箱里胳施，被Amal給moderate掉了溯祸！
? ? ?看到這種種詭異的行為，我才意識(shí)到原來(lái)學(xué)術(shù)界存在各種“幫派”舞肆。即使一些人的理論完全被更簡(jiǎn)單的理論超越焦辅，他們也會(huì)為“自己人”的理論說(shuō)話，讓你搞不清到底什么好椿胯，什么不好筷登。所以后來(lái)我對(duì)一些類型系統(tǒng)，以及Hoare Logic一類的“程序邏輯”產(chǎn)生了懷疑哩盲。我的課程project報(bào)告前方，就是指出Hoare Logic和Separation Logic所能完成的功能，其實(shí)用“符號(hào)執(zhí)行”或者“model checking”就能完成廉油。而這些程序邏輯所做的事情惠险，不過(guò)是把程序翻譯成了等價(jià)的邏輯表達(dá)式而已。到時(shí)候你要得知這些邏輯表達(dá)式的真?zhèn)问阆撸直仨毥?jīng)過(guò)一個(gè)類似程序分析的過(guò)程班巩，所以這些邏輯只不過(guò)讓你白走了一些彎路。當(dāng)Amal聽(tīng)完我的報(bào)告嘶炭，勉強(qiáng)的笑著說(shuō)：“你告訴了我們這個(gè)結(jié)論抱慌，可是你能用它來(lái)做什么呢？”我才發(fā)現(xiàn)原來(lái)透徹的看法眨猎，并不一定能帶來(lái)認(rèn)同抑进。人們都太喜歡“發(fā)明”東西，卻不喜歡“歸并”和“簡(jiǎn)化”東西睡陪。
? ?可是這類型系統(tǒng)的迷霧卻始終沒(méi)有散去寺渗，像一座大山壓在我頭上。我不滿意Haskell和ML的類型系統(tǒng)宝穗，又覺(jué)得System F等過(guò)于復(fù)雜户秤。可是由于它們的“理論性”和它們創(chuàng)造者的“權(quán)威”逮矛，我不敢斷定自己的看法就不是偏頗的鸡号。對(duì)付疑惑和恐懼的辦法就是面對(duì)它們，看透它們须鼎，消滅它們鲸伴。于是府蔗，我利用一個(gè)independent study的時(shí)間，獨(dú)立實(shí)現(xiàn)了一個(gè)類型系統(tǒng)汞窗。我試圖讓它極度的簡(jiǎn)單姓赤，卻又“包羅萬(wàn)象”。經(jīng)過(guò)一番努力仲吏，這個(gè)類型系統(tǒng)“涵蓋”了System F, MLF 以及另外一些類似系統(tǒng)的推導(dǎo)功能不铆，卻不直接“實(shí)現(xiàn)”他們。后來(lái)我就開(kāi)始試圖讓它涵蓋一種非常強(qiáng)大的類型系統(tǒng)裹唆，叫做intersection types誓斥。這種類型系統(tǒng)的研究已經(jīng)進(jìn)行了20多年，它不需要程序員寫任何類型標(biāo)記许帐，卻可以給任何“停機(jī)”的程序以類型劳坑。著名的Benjamin Pierce當(dāng)年的博士論文，就是有關(guān)intersection types的成畦。沒(méi)幾天距芬，我就對(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è)程序一樣惧浴。這肯定是完全不能接受的存和。后來(lái)我才發(fā)現(xiàn)，原來(lái)已經(jīng)有人指出了 System I 的這個(gè)問(wèn)題衷旅。但是由于我事先實(shí)現(xiàn)了這個(gè)系統(tǒng)捐腿，所以我直接的看到了這個(gè)結(jié)論，而不需要通過(guò)繁瑣的證明柿顶。
? ? 所以茄袖，我對(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)重問(wèn)題，它導(dǎo)致了這幾十年來(lái)很多對(duì)于相關(guān)類型系統(tǒng)的研究仁锯，其實(shí)是在解決一個(gè)根本不存在的問(wèn)題耀找。而自動(dòng)定理證明的研究者們，卻直接的“繞過(guò)”了這個(gè)問(wèn)題业崖。這也就是我為什么開(kāi)始對(duì)自動(dòng)定理證明開(kāi)始感興趣野芒。
? ? ?后來(lái)對(duì)自動(dòng)定理證明蓄愁，Partial Evaluation 和 supercompilation的探索，讓我看到那些看似高深的Martin Lof Type Theory, Linear Logic等概念狞悲，其實(shí)不過(guò)也就是用不同的說(shuō)法來(lái)重復(fù)相同的話題撮抓。具體的內(nèi)容我現(xiàn)在還不想談，但是我清楚的看到在“形式化”的美麗外衣下摇锋，其實(shí)有很多等價(jià)的丹拯，重復(fù)的，無(wú)聊的東西乱投。與其繼續(xù)“鉆研”它們咽笼，反復(fù)的叨咕差不多的內(nèi)容顷编，還不如用它們的“精髓”來(lái)做點(diǎn)有用的事情戚炫。
? ?>所以到現(xiàn)在，我已經(jīng)基本上擺脫了幾乎所有程序語(yǔ)言媳纬，編譯器双肤，類型系統(tǒng)，操作系統(tǒng)钮惠，邏輯推理系統(tǒng)給我設(shè)置的思維障礙茅糜。它們對(duì)我來(lái)說(shuō)不再是什么神物，它們的設(shè)計(jì)者對(duì)我來(lái)說(shuō)也不再是高不可攀的權(quán)威素挽。我很開(kāi)心蔑赘，經(jīng)過(guò)這段漫長(zhǎng)的探索，讓我自己的思想得到了解放预明，翻身成為了這些工具的主人缩赛。雖然我看到某些理論工具的研究恐怕早就已經(jīng)到達(dá)路的盡頭，然而它們里面隱含的美卻是無(wú)價(jià)和永恒的撰糠。這種美讓我對(duì)這個(gè)世界的許多其它方面有了煥然一新的看法酥馍。一個(gè)工具的價(jià)值不在于它自己，而在于你如何利用它創(chuàng)造出對(duì)人有益的東西阅酪，以及如何讓更多的人掌握它旨袒。這就是我打算現(xiàn)在去做的。
