王垠：從工具的奴隸到工具的主人
我們每個人都是工具的奴隸。隨著我們的學習，我們不斷的加深自己對工具的認識，從而從它們里面解脫出來。現在我就來說一下我作為各種工具的奴隸，以及逐漸擺脫它們的“思想控制”的歷史吧。
當我高中畢業進入大學計算機系的時候，輔導員對我們說：“你們不要只學書本知識，也要多見識一下業界的動態，比如去電腦城看看人家怎么裝機。”當然他說我們要多動手，多長見識，這是對的。不過如果成天就研究怎么“裝機”，研究哪種主板配哪種 CPU 之類的東西，你恐怕以后就只有去電腦城賣電腦了。
本科的時候，我經常發現一些同學不來上數學課。后來卻發現他們在宿舍自己寫程序，對 MFC 之類的東西津津樂道，引以為豪。當然會用 MFC 沒有什么不好，可是如果你完全沉迷于這些東西，恐怕就完全局限于 Windows 的一些表面現象了。
所以我在大學的時候就開始折騰 Linux，因為它貌似讓我能夠“深入”到計算機內部。那個時候，書店里只有一本 Linux 的書，封面非常簡陋。這是一本非常古老的書，它教的是怎樣得到 Slackware Linux，然后把它從二三十張軟盤裝到電腦上。總之，我就是這樣開始使用 Linux 的。后來我就走火入魔了，有時候上課居然在看 GCC 的內部結構文檔。后來我又開始折騰 TeX，把 TeXbook 都看了兩遍，恁是用它寫了我的本科畢業論文。
后來進了清華，因為不滿意有人嘲笑我用 Linux 這種“像 DOS 的東西”，以及國內網站都對 Windows 和 IE 進行“優化”的情況，就寫了個“完全用 Linux 工作”。確實，會 Linux 的人現在更容易找到工作，更容易被人當成高手。但是那些工具同樣的奴役了我，經常以一些雕蟲小技而自豪，讓我看不到如何才能設計出新的，更好的東西。當它們的設計改變的時候，我就會像奴隸一樣被牽著鼻子走。
這也許就是為什么我在清華的圖書館發現 《SICP》 的時候如此的欣喜。那本書是嶄新的，后面的借書記錄幾乎是空白的。這些看似簡單的東西教會我的，卻比那些大部頭和各種 HOWTO 教會我的更多，因為它們教會我的是 WHY，而不只是 HOW。當時我就發現，雖然自認為是一個“資深”的研究生，學過那么多種程序語言，各種系統工具甚至內核實現，可是相對于 SICP 的認識深度，我其實幾乎完全不會寫程序！在第三章，SICP 教會了我如何實現一個面向對象系統。這是我***次感覺到自己真正的在開始認識和控制自己所用的工具。
因為通常人們認為 Scheme 不是一個“實用”的語言，沒有很多“庫”可以用，效率也不高，而 Common Lisp 是“工業標準”，再加上 Paul Graham 文章的慫恿，所以我就開始了解 Common Lisp。在那段時間，我看了 Paul Graham 的 《On Lisp》 和 Peter Norvig 的 《Paradigms of Artificial Intelligence Programming》。怎么說呢？當時我以為自己學到很多，可是現在看來，它們教會我的并沒有 《SICP》 的東西那么精髓和深刻。開頭以為一山還有一山高，***回頭望去，其實復雜的東西并不比簡單的好。現在當我再看 Paul Graham 和 Peter Norvig 的文章，就覺得相當幼稚了，而且有很大的宗教成分。
進入 Cornell 之后，因為 Cornell 的程序語言課是用 SML 的，我才真正的開始學習“靜態類型”的函數式語言。之前在清華的時候，有個同學建議我試試 ML 和 Haskell，可是因為我對 Lisp 的執著，把他的話當成了耳邊風。當然現在用上 SML 就免不了發現 ML 的類型系統的一些撓人的問題，所以我就開始了解 Haskell，并且由于它看似優美的設計，我把“***語言”的希望寄托于它。我開始著迷一些像 monads, type class, lazy evaluation 一類的東西，看 Simon Peyton Jones 的一些關于函數式語言編譯器的書。以至于走火入魔，對其它一切“常規”語言都持鄙視態度，看到什么都說“那只不過是個 monad”。雖然有些語言被鄙視是合理的，有些卻是被錯怪了的。后來我也發現 monad, type class, lazy evaluation 這些東西其實并不是什么包治百病的靈丹妙藥。
但是我很不喜歡 Cornell 的壓抑氣氛，所以***決定離開。在不知何去何從的時候，我發了一封 email 給曾經給過我 fellowship 的 IU 教授 Doug Hofstadter （《GEB》的作者）。我說我不知道該怎么辦，后悔來了 Cornell，我現在對函數式語言感興趣。他跟我說，IU 的 Dan Friedman 就是做函數式語言的啊，你跟他聯系一下，就說是我介紹你來的。我開頭看過一點 The Little Schemer，跟小人書似的，所以還以為 Friedman 是個年輕小伙。當我聯系上 Friedman 的時候，他貌似早就認識我了一樣。他說當年你的申請材料非常 impressive，可惜你***沒有選擇我們。你要知道，世界上最重要的不是名氣，而是找到賞識你，能夠跟你融洽共事的人。你的材料都還在，我會請委員會重新考慮你的申請。IU 的名氣實在不大，而 Friedman 實在是太謙虛了，所以連跟他打電話都沒有明確表態想來 IU，只是說“我考慮一下……”這就是我怎么進入 IU 的。
Friedman 的教學真的有一手。雖然每個人對他看法不同，但是有幾個最重要的地方他的指點是幫了我大忙的。有人可能想象不到，在 Scheme 這種動態類型語言的“老槽”，其實有人對“靜態類型系統”的理解如此深刻。也就是在 Friedman 的指點下，我發現類型推導系統不過是一種“抽象解釋”，而各種所謂的“typing rule”，不過是抽象解釋器里面的分支語句。我后來就通過這個“直覺”，再加上 Friedman 的邏輯語言 miniKanren 里面對邏輯變量和 unification 的實現，做出了一個 Hindley-Milner 類型推導系統（HM 系統），也就是 ML 和 Haskell 的類型系統。雖然我在 Cornell 的課程作業里實現過一個 HM 系統，但是直到 Friedman 的提點，我才明白了它“為什么”是那個樣子，以至于達到更加優美的實現。后來經他一句話點撥，我又寫出了一個 lazy evaluation 的解釋器（也就是 Haskell 的語義），才發現原來 SPJ 的書里所謂的“graph reduction”，不過就是如此簡單的思想。只不過在 SPJ 的書里，細節掩蓋了本質。后來我在之前的 HM 系統之上做了一個非常小的改動，就實現了 type class 的功能，并且比 Haskell 的實現更加靈活。所以，就此我基本上掌握了 ML 和 Haskell 的理論精髓。
可是類型系統卻貌似一個無止境的東西。在 ML 的系統之上，還有 System F，Fw, MLF，Martin Lof Type Theory，CIC，…… 怎么沒完沒了？我一直覺得這些東西過度復雜，有那個必要嗎？直到 Amal Ahmed 來到 IU，我才相信了自己的感覺。然而，這卻是以一種“反面”的方式達到的。
Amal 是著名的 Andrew Appel （“虎書”的作者）的學生，在類型系統和編譯器的邏輯驗證方面做過很多工作。可是她比較讓人受不了，她總是顯得好像自己是這里唯一懂得類型的人，而其他人都是類型白癡。她不時的提到跟 Bob Harper, Benjamin Pierce 等類型大牛一起合作的事情。如果你問她什么問題，她經常會回答你：“Bob Harper 說……”她提到一個術語的時候總是把它說得無比神奇，把它的提出者的名字叫得異常響亮。有一次她上課給我們講 System F，我問她，為什么這個系統有兩個“binder”，貌似太復雜了，為什么不能只用一個？她沒有正面回答，而是嘲諷似的說：“不是你說可以就可以的。它就是這個樣子的。”后來我卻發現其實有另外一個系統，它只有一個 binder，而且設計得更加簡潔。后來我又在課程的 mailing list 問了一個問題，質疑一個編譯器驗證方面的概念。本來是純粹的學術討論，卻發現這封 email 根本沒有發到全班同學信箱里，被 Amal 給 moderate 掉了！
看到這種種詭異的行為，我才意識到原來學術界存在各種“幫派”。即使一些人的理論完全被更簡單的理論超越，他們也會為“自己人”的理論說話，讓你搞不清到底什么好，什么不好。所以后來我對一些類型系統，以及 Hoare Logic 一類的“程序邏輯”產生了懷疑。我的課程 project 報告，就是指出 Hoare Logic 和 Separation Logic 所能完成的功能，其實用“符號執行”或者 “model checking” 就能完成。而這些程序邏輯所做的事情，不過是把程序翻譯成了等價的邏輯表達式而已。到時候你要得知這些邏輯表達式的真偽，又必須經過一個類似程序分析的過程，所以這些邏輯只不過讓你白走了一些彎路。當 Amal 聽完我的報告，勉強的笑著說：“你告訴了我們這個結論，可是你能用它來做什么呢？”我才發現原來透徹的看法，并不一定能帶來認同。人們都太喜歡“發明”東西，卻不喜歡“歸并”和“簡化”東西。
可是這類型系統的迷霧卻始終沒有散去，像一座大山壓在我頭上。我不滿意 Haskell 和 ML 的類型系統，又覺得 System F 等過于復雜。可是由于它們的“理論性”和它們創造者的“權威”，我不敢斷定自己的看法就不是偏頗的。對付疑惑和恐懼的辦法就是面對它們，看透它們，消滅它們。于是，我利用一個 independent study 的時間，獨立實現了一個類型系統。我試圖讓它極度的簡單，卻又“包羅萬象”。經過一番努力，這個類型系統“涵蓋”了 System F, MLF 以及另外一些類似系統的推導功能，卻不直接“實現”他們。后來我就開始試圖讓它涵蓋一種非常強大的類型系統，叫做 intersection types。這種類型系統的研究已經進行了 20 多年，它不需要程序員寫任何類型標記，卻可以給任何“停機”的程序以類型。著名的 Benjamin Pierce 當年的博士論文，就是有關 intersection types 的。沒幾天，我就對自己的系統稍作改動，讓它涵蓋了一種***大的 intersection type 系統（System I）的所有功能。然而我卻很快發現這個系統是不能實用的，因為它在進行類型推導的時候相當于是在運行這個程序，這樣類型推導的計算復雜度就會跟這個程序一樣。這肯定是完全不能接受的。后來我才發現，原來已經有人指出了 System I 的這個問題。但是由于我事先實現了這個系統，所以我直接的看到了這個結論，而不需要通過繁瑣的證明。
所以，我對類型推導的探索就這樣到達了一個終點。我的類型系統是如此的簡單，以至于我看到了類型推導的本質，而不需要記住復雜的符號和推理規則。我的系統在去掉了 intersection type 之后，仍然比 System F 和 MLF 都要強大。我也看到了 Hindley-Milner 系統里面的一個嚴重問題，它導致了這幾十年來很多對于相關類型系統的研究，其實是在解決一個根本不存在的問題。而自動定理證明的研究者們，卻直接的“繞過”了這個問題。這也就是我為什么開始對自動定理證明開始感興趣。
后來對自動定理證明, Partial Evaluation 和 supercompilation 的探索，讓我看到那些看似高深的 Martin Lof Type Theory, Linear Logic 等概念，其實不過也就是用不同的說法來重復相同的話題。具體的內容我現在還不想談，但是我清楚的看到在“形式化”的美麗外衣下，其實有很多等價的，重復的，無聊的東西。與其繼續“鉆研”它們，反復的叨咕差不多的內容，還不如用它們的“精髓”來做點有用的事情。
所以到現在，我已經基本上擺脫了幾乎所有程序語言，編譯器，類型系統，操作系統，邏輯推理系統給我設置的思維障礙。它們對我來說不再是什么神物，它們的設計者對我來說也不再是高不可攀的權威。我很開心，經過這段漫長的探索，讓我自己的思想得到了解放，翻身成為了這些工具的主人。雖然我看到某些理論工具的研究恐怕早就已經到達路的盡頭，然而它們里面隱含的美卻是無價和永恒的。這種美讓我對這個世界的許多其它方面有了煥然一新的看法。一個工具的價值不在于它自己，而在于你如何利用它創造出對人有益的東西，以及如何讓更多的人掌握它。這就是我打算現在去做的。
