当我高中毕业进入大学计算机系的时候，辅导员对我们说：“你们不要只学书本知识，也要多见识一下业界的动态，比如去电脑城看看人家怎么装机。”当然他说我们要多动手，多长见识，这是对的。不过如果成天就研究怎么“装机”，研究哪种主板配哪种 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 等概念，其实不过也就是用不同的说法来重复相同的话题。具体的内容我现在还不想谈，但是我清楚的看到在“形式化”的美丽外衣下，其实有很多等价的，重复的，无聊的东西。与其继续“钻研”它们，反复的叨咕差不多的内容，还不如用它们的“精髓”来做点有用的事情。
所以到现在，我已经基本上摆脱了几乎所有程序语言，编译器，类型系统，操作系统，逻辑推理系统给我设置的思维障碍。它们对我来说不再是什么神物，它们的设计者对我来说也不再是高不可攀的权威。我很开心，经过这段漫长的探索，让我自己的思想得到了解放，翻身成为了这些工具的主人。虽然我看到某些理论工具的研究恐怕早就已经到达路的尽头，然而它们里面隐含的美却是无价和永恒的。这种美让我对这个世界的许多其它方面有了焕然一新的看法。一个工具的价值不在于它自己，而在于你如何利用它创造出对人有益的东西，以及如何让更多的人掌握它。这就是我打算现在去做的。
原文：http://blog.sina.com.cn/s/blog_5d90e82f01018x95.html
