當我高中畢業(yè)進入大學計算機系的時候为狸，輔導員對我們說：“你們不要只學書本知識，也要多見識一下業(yè)界的動態(tài)挨厚，比如去電腦城看看人家怎么裝機堡僻。”當然他說我們要多動手疫剃，多長見識，這是對的硼讽。不過如果成天就研究怎么“裝機”巢价，研究哪種主板配哪種 CPU 之類的東西，你恐怕以后就只有去電腦城賣電腦了。
本科的時候壤躲，我經常發(fā)現(xiàn)一些同學不來上數(shù)學課城菊。后來卻發(fā)現(xiàn)他們在宿舍自己寫程序，對MFC之類的東西津津樂道碉克，引以為豪凌唬。當然會用MFC沒有什么不好，可是如果你完全沉迷于這些東西漏麦，恐怕就完全局限于Windows的一些表面現(xiàn)象了客税。
所以我在大學的時候就開始折騰Linux，因為它貌似讓我能夠“深入”到計算機內部撕贞。那個時候更耻，書店里只有一本 Linux 的書，封面非常簡陋捏膨。這是一本非常古老的書秧均，它教的是怎樣得到Slackware Linux，然后把它從二三十張軟盤裝到電腦上号涯∧亢總之，我就是這樣開始使用Linux的链快。后來我就走火入魔了讶隐，有時候上課居然在看GCC的內部結構文檔。后來我又開始折騰TeX久又，把TeXbook都看了兩遍巫延，恁是用它寫了我的本科畢業(yè)論文。
后來進了清華地消，因為不滿意有人嘲笑我用Linux這種“像DOS的東西”炉峰，以及國內網站都對Windows和IE進行“優(yōu)化”的情況，就寫了個“完全用Linux工作”脉执。確實疼阔，會Linux的人現(xiàn)在更容易找到工作，更容易被人當成高手半夷。但是那些工具同樣的奴役了我婆廊，經常以一些雕蟲小技而自豪，讓我看不到如何才能設計出新的巫橄，更好的東西淘邻。當它們的設計改變的時候，我就會像奴隸一樣被牽著鼻子走湘换。
這也許就是為什么我在清華的圖書館發(fā)現(xiàn)《SICP》的時候如此的欣喜宾舅。那本書是嶄新的统阿，后面的借書記錄幾乎是空白的。這些看似簡單的東西教會我的筹我，卻比那些大部頭和各種 HOWTO 教會我的更多扶平，因為它們教會我的是WHY，而不只是HOW蔬蕊。當時我就發(fā)現(xiàn)结澄，雖然自認為是一個“資深”的研究生，學過那么多種程序語言岸夯，各種系統(tǒng)工具甚至內核實現(xiàn)麻献，可是相對于SICP的認識深度，我其實幾乎完全不會寫程序囱修！在第三章赎瑰，SICP?教會了我如何實現(xiàn)一個面向對象系統(tǒng)。這是我第一次感覺到自己真正的在開始認識和控制自己所用的工具破镰。
因為通常人們認為Scheme不是一個“實用”的語言餐曼，沒有很多“庫”可以用，效率也不高鲜漩，而Common Lisp是“工業(yè)標準”源譬，再加上Paul Graham文章的慫恿，所以我就開始了解Common Lisp孕似。在那段時間踩娘，我看了Paul Graham的《On Lisp》和Peter Norvig的?《Paradigms of Artificial Intelligence Programming》。怎么說呢喉祭？當時我以為自己學到很多养渴，可是現(xiàn)在看來，它們教會我的并沒有《SICP》的東西那么精髓和深刻泛烙。開頭以為一山還有一山高理卑，最后回頭望去，其實復雜的東西并不比簡單的好”伟保現(xiàn)在當我再看Paul Graham和Peter Norvig的文章藐唠，就覺得相當幼稚了，而且有很大的宗教成分鹉究。
進入Cornell之后宇立，因為Cornell的程序語言課是用SML的，我才真正的開始學習“靜態(tài)類型”的函數(shù)式語言自赔。之前在清華的時候妈嘹，有個同學建議我試試ML和Haskell，可是因為我對Lisp 的執(zhí)著匿级，把他的話當成了耳邊風蟋滴。當然現(xiàn)在用上SML就免不了發(fā)現(xiàn)ML的類型系統(tǒng)的一些撓人的問題染厅，所以我就開始了解Haskell痘绎，并且由于它看似優(yōu)美的設計津函，我把“終極語言”的希望寄托于它。我開始著迷一些像monads孤页，type class尔苦，lazy evaluation 一類的東西，看Simon Peyton Jones的一些關于函數(shù)式語言編譯器的書行施。以至于走火入魔允坚，對其它一切“常規(guī)”語言都持鄙視態(tài)度，看到什么都說“那只不過是個monad”蛾号。雖然有些語言被鄙視是合理的稠项，有些卻是被錯怪了的。后來我也發(fā)現(xiàn)monad, type class, lazy evaluation這些東西其實并不是什么包治百病的靈丹妙藥鲜结。
但是我很不喜歡Cornell的壓抑氣氛展运，所以最后決定離開。在不知何去何從的時候精刷，我發(fā)了一封email給曾經給過我fellowship的IU教授Doug Hofstadter（《GEB》的作者）拗胜。我說我不知道該怎么辦，后悔來了 Cornell怒允，我現(xiàn)在對函數(shù)式語言感興趣埂软。他跟我說，IU的Dan Friedman就是做函數(shù)式語言的啊纫事，你跟他聯(lián)系一下勘畔，就說是我介紹你來的。我開頭看過一點The Little Schemer丽惶，跟小人書似的炫七，所以還以為Friedman是個年輕小伙。當我聯(lián)系上Friedman的時候蚊夫，他貌似早就認識我了一樣诉字。他說當年你的申請材料非常impressive，可惜你最后沒有選擇我們知纷。你要知道壤圃，世界上最重要的不是名氣，而是找到賞識你琅轧，能夠跟你融洽共事的人伍绳。你的材料都還在，我會請委員會重新考慮你的申請乍桂。IU 的名氣實在不大冲杀，而Friedman?實在是太謙虛了效床，所以連跟他打電話都沒有明確表態(tài)想來IU，只是說“我考慮一下……”這就是我怎么進入IU的权谁。
Friedman的教學真的有一手剩檀。雖然每個人對他看法不同，但是有幾個最重要的地方他的指點是幫了我大忙的旺芽。有人可能想象不到沪猴，在Scheme這種動態(tài)類型語言的“老槽”，其實有人對“靜態(tài)類型系統(tǒng)”的理解如此深刻采章。也就是在Friedman的指點下运嗜，我發(fā)現(xiàn)類型推導系統(tǒng)不過是一種“抽象解釋”，而各種所謂的“typing rule”悯舟，不過是抽象解釋器里面的分支語句担租。我后來就通過這個“直覺”，再加上Friedman的邏輯語言miniKanren里面對邏輯變量和unification的實現(xiàn)抵怎，做出了一個Hindley-Milner類型推導系統(tǒng)（HM 系統(tǒng)）奋救，也就是ML和 Haskell的類型系統(tǒng)。雖然我在Cornell的課程作業(yè)里實現(xiàn)過一個HM系統(tǒng)便贵，但是直到Friedman的提點菠镇，我才明白了它“為什么”是那個樣子，以至于達到更加優(yōu)美的實現(xiàn)承璃。后來經他一句話點撥利耍，我又寫出了一個lazy evaluation的解釋器（也就是Haskell的語義），才發(fā)現(xiàn)原來SPJ的書里所謂的“graph reduction”盔粹，不過就是如此簡單的思想隘梨。只不過在SPJ的書里，細節(jié)掩蓋了本質舷嗡。后來我在之前的HM系統(tǒng)之上做了一個非常小的改動轴猎，就實現(xiàn)了type class的功能，并且比Haskell的實現(xiàn)更加靈活进萄。所以捻脖，就此我基本上掌握了ML和Haskell的理論精髓。
可是類型系統(tǒng)卻貌似一個無止境的東西中鼠。在ML的系統(tǒng)之上可婶，還有System F，F(xiàn)w援雇，MLF矛渴，Martin Lof Type Theory，CIC惫搏，……怎么沒完沒了具温？我一直覺得這些東西過度復雜蚕涤，有那個必要嗎？直到Amal Ahmed來到IU铣猩，我才相信了自己的感覺揖铜。然而，這卻是以一種“反面”的方式達到的剂习。
Amal是著名的Andrew Appel（“虎書”的作者）的學生蛮位，在類型系統(tǒng)和編譯器的邏輯驗證方面做過很多工作较沪×廴疲可是她比較讓人受不了，她總是顯得好像自己是這里唯一懂得類型的人尸曼，而其他人都是類型白癡们何。她不時的提到跟Bob Harper, Benjamin Pierce等類型大牛一起合作的事情。如果你問她什么問題控轿，她經常會回答你：“Bob Harper說……”她提到一個術語的時候總是把它說得無比神奇冤竹，把它的提出者的名字叫得異常響亮。有一次她上課給我們講System F茬射，我問她鹦蠕，為什么這個系統(tǒng)有兩個“binder”，貌似太復雜了在抛，為什么不能只用一個钟病？她沒有正面回答，而是嘲諷似的說：“不是你說可以就可以的刚梭。它就是這個樣子的肠阱。”后來我卻發(fā)現(xiàn)其實有另外一個系統(tǒng)朴读，它只有一個binder屹徘，而且設計得更加簡潔。后來我又在課程的 ailing list 了一個問題衅金，質疑一個編譯器驗證方面的概念噪伊。本來是純粹的學術討論，卻發(fā)現(xiàn)這封email根本沒有發(fā)到全班同學信箱里氮唯，被Amal給moderate掉了鉴吹！
看到這種種詭異的行為，我才意識到原來學術界存在各種“幫派”您觉。即使一些人的理論完全被更簡單的理論超越拙寡，他們也會為“自己人”的理論說話，讓你搞不清到底什么好琳水，什么不好肆糕。所以后來我對一些類型系統(tǒng)般堆，以及Hoare Logic一類的“程序邏輯”產生了懷疑。我的課程project報告诚啃，就是指出Hoare Logic和Separation Logic所能完成的功能淮摔，其實用“符號執(zhí)行”或者“model checking”就能完成。而這些程序邏輯所做的事情始赎，不過是把程序翻譯成了等價的邏輯表達式而已和橙。到時候你要得知這些邏輯表達式的真?zhèn)危直仨毥涍^一個類似程序分析的過程造垛，所以這些邏輯只不過讓你白走了一些彎路魔招。當Amal聽完我的報告，勉強的笑著說：“你告訴了我們這個結論五辽，可是你能用它來做什么呢办斑？”我才發(fā)現(xiàn)原來透徹的看法，并不一定能帶來認同杆逗。人們都太喜歡“發(fā)明”東西乡翅，卻不喜歡“歸并”和“簡化”東西。
可是這類型系統(tǒng)的迷霧卻始終沒有散去罪郊，像一座大山壓在我頭上蠕蚜。我不滿意Haskell和ML的類型系統(tǒng)，又覺得System F等過于復雜悔橄“欣郏可是由于它們的“理論性”和它們創(chuàng)造者的“權威”，我不敢斷定自己的看法就不是偏頗的橄维。對付疑惑和恐懼的辦法就是面對它們尺铣，看透它們，消滅它們争舞。于是凛忿，我利用一個independent study的時間，獨立實現(xiàn)了一個類型系統(tǒng)竞川。我試圖讓它極度的簡單店溢，卻又“包羅萬象”。經過一番努力委乌，這個類型系統(tǒng)“涵蓋”了System F, MLF 以及另外一些類似系統(tǒng)的推導功能床牧，卻不直接“實現(xiàn)”他們。后來我就開始試圖讓它涵蓋一種非常強大的類型系統(tǒng)遭贸，叫做intersection types戈咳。這種類型系統(tǒng)的研究已經進行了20多年，它不需要程序員寫任何類型標記，卻可以給任何“停機”的程序以類型著蛙。著名的Benjamin Pierce當年的博士論文删铃，就是有關intersection types的。沒幾天踏堡，我就對自己的系統(tǒng)稍作改動猎唁，讓它涵蓋了一種最強大的intersection type系統(tǒng)（System I）的所有功能。然而我卻很快發(fā)現(xiàn)這個系統(tǒng)是不能實用的顷蟆，因為它在進行類型推導的時候相當于是在運行這個程序诫隅，這樣類型推導的計算復雜度就會跟這個程序一樣。這肯定是完全不能接受的帐偎。后來我才發(fā)現(xiàn)逐纬，原來已經有人指出了 System I 的這個問題。但是由于我事先實現(xiàn)了這個系統(tǒng)肮街，所以我直接的看到了這個結論风题，而不需要通過繁瑣的證明。
所以嫉父，我對類型推導的探索就這樣到達了一個終點。我的類型系統(tǒng)是如此的簡單眼刃，以至于我看到了類型推導的本質绕辖，而不需要記住復雜的符號和推理規(guī)則。我的系統(tǒng)在去掉了intersection type之后擂红，仍然比System F和MLF都要強大仪际。我也看到了Hindley-Milner系統(tǒng)里面的一個嚴重問題，它導致了這幾十年來很多對于相關類型系統(tǒng)的研究昵骤，其實是在解決一個根本不存在的問題树碱。而自動定理證明的研究者們，卻直接的“繞過”了這個問題变秦。這也就是我為什么開始對自動定理證明開始感興趣成榜。
后來對自動定理證明，Partial Evaluation 和 supercompilation的探索蹦玫，讓我看到那些看似高深的Martin Lof Type Theory, Linear Logic等概念赎婚，其實不過也就是用不同的說法來重復相同的話題。具體的內容我現(xiàn)在還不想談樱溉，但是我清楚的看到在“形式化”的美麗外衣下挣输，其實有很多等價的，重復的福贞，無聊的東西撩嚼。與其繼續(xù)“鉆研”它們，反復的叨咕差不多的內容，還不如用它們的“精髓”來做點有用的事情完丽。
所以到現(xiàn)在竞帽，我已經基本上擺脫了幾乎所有程序語言踩衩，編譯器，類型系統(tǒng)，操作系統(tǒng)革为，邏輯推理系統(tǒng)給我設置的思維障礙。它們對我來說不再是什么神物太伊，它們的設計者對我來說也不再是高不可攀的權威妻怎。我很開心，經過這段漫長的探索搁痛，讓我自己的思想得到了解放长搀，翻身成為了這些工具的主人。雖然我看到某些理論工具的研究恐怕早就已經到達路的盡頭鸡典，然而它們里面隱含的美卻是無價和永恒的源请。這種美讓我對這個世界的許多其它方面有了煥然一新的看法。一個工具的價值不在于它自己彻况，而在于你如何利用它創(chuàng)造出對人有益的東西谁尸，以及如何讓更多的人掌握它。這就是我打算現(xiàn)在去做的纽甘。
