到底是谁在欺负我们读书少？
发表了之前的文章《我为什么不再做PL人》之后，我发现有人在知乎上发表文章诬蔑我。本来不想理知乎上的东西，但作者把各种刚从论文上学来的术语，似懂非懂，照本宣科列了一大堆，挺能唬人的，说起来很像那么回事儿，所以我只好破例回应一下，但是下不为例。
现在我把这篇文章，题名『王垠，请别再欺负我们读书少』的链接放在这里，供大家观看。评论的第4，第6页有我的回复，技术性比较强，不过有兴趣的人可以看看。为了方便，我也把评论整理和拷贝到这篇文章第二节。
历史和事实
文章作者彭飞自称导师是 Jens Palsberg，然而 Palsberg 的主页上列出自己所有的学生，却没有彭飞的名字。Palsberg 似乎曾在 CFA 领域做过一点研究，但我印象不深，我也从来没有在批评 CFA 的时候点过 Palsberg 的名。但由于我指出了 CFA 领域的弊病，彭飞可能就是一心研究这个的，所以觉得“祖业”受到了攻击，想要反驳我，支持 CFA 的“先进性”，这样以后可以在学术界更好的混下去。这可以理解，然而彭飞的文章，其实破绽很多，处处显示出他自己的一知半解和本本主义。
CFA 领域的理论从来没有成功实现，展示过它的功效。CFA 最强大的版本，CFA2 的作者 Dimitris Vardoulakis，当年在 Mozilla 实习的时候试图在 JavaScript 上实现 CFA2 算法。最后的产物叫做“DoctorJS”，还做了一个网站让人试用。可是在不久之后 DoctorJS 不了了之，消失了。Dimitris 这人也挺爱吹嘘的，自己的主页上和简历上，都在很靠近自己姓名的地方自豪的写着“CFA2的发明者”字样，仿佛 CFA2 是什么众所周知的伟大发明，是自己毕生唯一的杰作一样。
后来跟 Mozilla 的 research director 聊天时，他告诉我 DoctorJS 其实根本不好用，理论过度复杂，实现起来非常困难，而且达不到号称可以达到的效果，所以以后不想再赞助相关的项目了。Mozilla 现在已经不再维护 DoctorJS 的代码，这两封 email 就是我们能找到的关于 Mozilla+DoctorJS 最后的信息:
当然，Dave Herman 是很会说套话的。要让别人接手这样的项目，你不可能说它不好用或者很难维护，所以当然要假装它有价值。然而字里行间你却可以看出来，这理论其实非常难以实现，实现了也很容易出错，不知道到底是否正确。最后没人敢碰这样的代码，所以就不了了之了。
之前在 Sourcegraph 的时候，两位 founder 也试图采用 DoctorJS 来做 JavaScript 的分析，后来发现不好用，改用了 Tern，才产生了有用一点的信息。
PySonar2（写于2010年）是跟 CFA2 差不多的时间出现的，而 P4F 的发表比 PySonar2 晚了好几年。可是 PySonar2 到今天仍然比 CFA2，P4F 都要准确和简单。原因很简单，因为它根本没有 CFA所用的 continuation passing style（CPS变换）所带来的所谓“call/return 匹配问题”。所有的 call 和它们的 return，被抽象解释器（abstract interpreter）自然而然的匹配好了，根本不可能错位。
我很惊讶的是 CFA 领域研究了 20 年，就在解决这种根本不存在的问题，把简单的问题搞复杂，然后又让它简单一些，来来回回的。PySonar2 一开头就很简单，从来没出现过 CFA 那些乱七八糟的问题，直接就把问题给解决了。彭飞抓住 PySonar2 表面上的一些小问题指指点点，貌似好大个事情，而其实很多都是由于他自己理解不够深入。详情请见我的评论。
另外，我真的对 Python，Ruby，JavaScript 这些动态语言做 type inference 不感兴趣了。PySonar2 虽然比 CFA2 和P4F 都简单和强大，但是我从来没想维护 PySonar2 的“先进性”，我从来没想推广 PySonar2，我绝对不会在自己的名字旁边写上“PySonar 发明者”的字样。因为我根本不在乎 Python，也没把 PySonar2 当回事。给 Python 这样的语言做一个很好的类型推导工具，有什么意义吗？未来的方向是直接写上 type annotation，就像 Java 和 C# 那样，让类型检查简单，迅速又准确。所以 PySonar2 和 CFA 领域做的其实都是无用功，只不过我没浪费 20 年时间研究 CFA，只用了加起来几个月时间，而且还比他们做得更好。
我在 2014 年末的样子给 CFA 的“祖师爷” Olin Shivers 写了封 email，讨论合作机会。我跟他讲述了 PySonar2 的做法，而且问他为什么 CFA 的 call/return match 用那么复杂的方法来做，然而他没有回我的 email。这是一个不祥的预兆，因为我一直在犹豫是否应该告诉这些人，有简单很多倍的办法，可以达到同样的目的。他们完全可以“借鉴”我的做法，然后写进论文里面发表。所以如果他们的 2016 论文加入了我的想法，也不足为怪。但是真的不在乎这些了，学术界随便胡搞就胡搞呗，反正也不可能有什么大的用处。这些东西，其实做 static analysis 的人早就明白， CFA 远远落后，只能在自己的圈子里发表点 paper。
彭飞错误地认为我很把 PySonar2 当回事，然而它只是我曾经做过的一个小玩具。我一直在探索和展望更加实在，对人可以产生真正效益的领域。只是随便提了一下 CFA，就得到如此强烈而具体的攻击，我对某些自诩“PL 学院派”的自我保护意识真的很惊讶。这里给“PL 学院派”打引号的原因是，CFA 领域其实从来就不是 PL 学院派里面很重要的方向，就那么几个人形成了一个小圈子，每次发出来的论文只有他们几个人看，每次开 POPL 自己开个小 workshop。其它的 PL 人总是听说这些名字，却其实从来不关心，也不知道他们在说什么。CFA 的人从来不跟更广泛的“静态分析”领域对比和引用，其实他们的那些作法的关键部分，在其它语言（比如 C）的静态分析工具里面早就有了。
技术部分
以下是针对彭飞提出的 pysonar 的“技术缺陷”的逐一回应。说成什么“命门缺陷”，其实只有最后第 4 个例子发现了一个小 bug，被我改了几行代码就修好了。
关于命门缺陷1
（注意上面的夸大其词 ;-）
回复：推导出的 int -> int | bool ->bool 表示的确实是一个 intersection type，而不是 union type。只不过我中间用的|记号跟 union type 一样，所以看起来比较混淆，然而内部实现确实是 intersection type，而不是 union type。
现在我把中间的分隔符改成了 unicode 字符 ∧，跟 intersection type 的论文上一样。我想这下他该满意了吧？也就是个表面现象而已。
我怀疑彭飞到底明不明白什么是 intersection type。这个 type 表示这个函数(id)“同时”是int->int和bool->bool，而不是表示它“有时”是int->int，而另外的时候是bool->bool。所以如果你调用id(1)，推导出的输出一定是int。如果你输入id(True)，它推导出的一定是bool。
如果这是一个 union type 的话，调用id(1)会报错，因为id的类型有可能是bool->bool，不能接受int的输入。调用id(True)也会报错，因为id的类型也有可能是int->int，不能接受bool的输入。所以就左右不是人。
其实如果彭飞仔细看那两个变量a和b的类型，就会发现这是 intersection type，而不是 union type。
可能有人对这里的 intersection type 有所误解。int -> int ∧ bool ->bool，在这里其实不是表示这个函数只能接受int或者bool的输入，而只是表示这个函数在某些调用的地方输入了int或者bool，然后分别输出了int和bool。所以在“官方意义”下，这并不是这个函数的类型。那么这个函数的类型是什么呢？pysonar 的哲学是这样：每一个函数的类型，就是这个函数本身。没有比函数本身更能够描述函数的特征的类型，这就是静态分析领域跟类型理论（type theory）领域的区别。虽然 pysonar 的分析标记出的类型并不是函数的“本质类型”，然而这并不会削弱对类型错误的检测，反而会增强它。这是因为 pysonar 直接通过对函数体进行分析，找到类型错误。函数体比通常的类型包含更精确的信息，所以 pysonar 的类型分析，其实比普通的类型系统更加精确。所以可以说，静态分析是比类型理论更加细致和精华的领域。
另外，pysonar 本来就是放弃了他所谓的“Haskell 那种 polymorphic type inference”，故意要用“concrete type inference”，因为 Haskell 那种 type inference 对于 Python 是不能用的。有些人很喜欢随口冒出术语，可是 Haskell 那种其实不叫“polymorphic type inference”，而叫Hindley-Milner 类型系统（HM）。这种类型系统最早出现在 SML，后来也被 OCaml 和 Haskell 借鉴。我不知道彭飞为什么抓住“polymorphic”这个词不放，pysonar 的 type inference 其实也是polymorphic 的，因为它允许函数接受多种类型的输入。
彭飞指出函数id可以推导出类似 HM 系统的forall a. a -> a这样的类型。对于id这么简单的函数是可以，然而对于稍微复杂点的 Python 代码，HM 系统是不可行的。PySonar 早在 2009 年的第一版，就做过 HM 那样的系统，确实能把id推出forall a. a -> a那样的类型，但是后来发现遇到复杂点的 Python 代码就不行了。所以后来我干脆把 HM 系统去掉了，只留下正向的跨过程（interprocedual）类型推导。
HM 类型系统的问题是根本性的，早在 ML 之 类的语言里面出现过了，然后出现了一系列变通（workaround），比如所谓“let-polymorphism”，“value restriction”等等，却不能从根本上解决问题。彭飞似乎没有看过相关的内容，或者把这些丑陋的变通，当成了博大精深的发明吧？:)
举个简单的例子好了。下面这段完全合法的 Python 代码，你就没法用 HM 那样的系统推导出类型：
def foo(f):
return f(1), f(True)
def id(x):
return x
a = foo(id)
print(a) # prints "(1, True)"
这段代码会毫无问题的打印出(1, True)，然而它却不能通过HM系统的类型检查。如果你不信，那你可以写出等价的 Haskell 代码：
foo f = (f 1, f True) a = foo id
你把这段代码交给 Haskell 的编译器，它会报错：
No instance for (Num Bool) arising from the literal ‘1’
In the first argument of ‘f’, namely ‘1’
In the expression: f 1
In the expression: (f 1, f True)
这是因为 Haskell 所用的 HM 系统，无法知道foo的参数f是一个什么样的函数，它是同时能接受int和bool，还是其实能接受所有类型，也就是forall a. a->a呢？类型推导不能确定这个范围，所以只能假设f不可以是一个 polymorphic 的函数，所以发现f被同时输入了1和True，就报错了。
这是一个 HM 系统根本无法解决的问题。SML，OCaml 和 Haskell 里面所谓的“let-polymorphism”，就是一个对此的非常局限的变通。
相比之下，pysonar 的类型推导，却可以正确判断出这个代码其实没有问题。它能准确地推断出a的类型是tuple类型(int, bool)。
所以说得倒容易，我们请有本事的彭飞同学用 CFA 家族的算法，给我们 show 一下推导出 forall类型？:)
关于命门缺陷2：
回复：打开错误报告的开关（-report），彭飞这个例子里的类型错误就会被标记出来。
像所有动态语言的类型推导器一样，pysonar 的类型推导会出现 false positive，所以 pysonar 现在主要用于代码检索，而不是报告类型错误。为了防止这些类型错误信息干扰视线，pysonar 现在并不缺省在 demo 中标记类型错误，因为 demo 只是作为一个 indexer 提供信息。然而打开错误报告的开关（-report）之后，彭飞这个例子里的类型错误还是可以被发现的。
目前的 UI 会在有类型错误的地方放上一个下划线，鼠标移上去之后，会显示那里的问题。然而现在的 Web UI 有个问题，因为下划线离变量的链接太近，所以鼠标指到变量之上，就会提示变量的类型，而不是错误。如果你打开浏览器的 inspector，就可以看到报告的错误：“warning: attribute not found in type: A”。
我知道报错链接的放置位置不是很合理，而且鼠标 UI 设计不大好，不过这只是一个粗糙的 demo，也许以后有时间再改进吧。然而这并不是什么“命门缺陷”，因为类型错误确实是被发现了的。
关于缺陷3：
回复：有一个链接没有指向，是因为当时在 Sourcegraph，由于 UI 和数据库存储的限制，他们需要 HTML 里面的链接只跳转到一个地方，所以 UI 上同时指向两个地方的功能就被去掉了。然而内存里面的 reference 其实都是可以有多个的，这个你只需要看看 pysonar 的内部数据结构就可以发现。或者用更简单的办法，你只需要看一下a的类型：
a的类型是{B | A}，这说明什么呢？这说明 pysonar 完全知道a.x可能引用两个地方，A.x和B.x。
为了这么点 UI 的事情，就说“作者没有理解静态分析的本质”，然后拿各种术语，什么“抽象值”（abstract value），或者引用书本上的定义来吓唬人，这说明他根本没有试图搞明白 pysonar 的工作原理。“抽象值”是非常基础的概念，觉得我连这个都不理解，这种人还真以为自己学会了点术语了 :)
pysonar 运行的时候，里面到处跑的都是抽象值，就没有几个东西不是抽象值的。小朋友可能从来没实现过类似的东西，所以很是把这些基础概念当回事。死记硬背了点书本知识，就自以为了不起。从来没有试图了解实情，有了疑惑也不来信虚心请教。抓到一点肤浅的“疑似把柄”，就背地里拿出来说成天大的事。
关于缺陷4：
回复：这个“看似很严重的 bug”确实是一个 bug，然而它不像他说的那么严重。而且不像他说的那样，需要另外一遍“语义分析”。pysonar 是一个强大的抽象解释器，它完全可以只做一遍分析就找到这些名字，引用和类型。
所以，只改了几行代码之后，现在已经能显示所有变量n的类型为int。pysonar 大的原理和结构都是非常好的，这些小问题真是不值一提，很容易修好。
反复的提到“语义分析”（semantic analysis）这些空洞的名词，显示了彭飞刚入道不久，学艺肤浅。“把每个变量和它的定义联系起来”，这种做法其实是所谓 data flow analysis 常用的。Data flow analysis 速度快，可是非常的粗略，不精确。JavaScript 的分析器 Tern 就是用的这种方法。这种做法根本不可能达到 pysonar 的带有控制流信息的分析精确程度。
另外，彭飞还有一些闭着眼睛肆意的歪曲，比如说 pysonar 的代码冗长复杂。他恐怕根本就没看过 pysonar 的代码，不然他可以发现 pysonar 的类型分析器总共只有 1200 行代码，而且结构非常简单干净。
他说 pysonar 不是 sound 的，而 CFA2 是 sound 的，可我从来没说过 PySonar2 是 sound 的。其实 CFA2 和 P4F，对于 Python 也不可能是 sound 的，因为对这样的语言做类型推导，本来就是 undecidable 的问题。这些工具能做的，只是最大限度的发现类型错误而已。它们并不能完全排除类型错误。它们的类型推导都有很多 false positive，所以不可能用在编译器优化等方向。
不得不引用一下 Linus 的话（虽然我鄙视这句话）：Talk is cheap. Show me some code。我请彭飞把 P4F 实现出来，给我们展示一下它能生成什么样的结果？哈哈。CFA2 的发明人已经在 Mozilla 试过了不是吗？过度复杂的理论，根本不能实现和产生实际效果。实话说吧，CFA 家族的算法恐怕要再发展好几年，仔细研究 PySonar2 的实现，才有可能达到 PySonar2 的地步。
到底是谁在欺负你们书读得少？
彭飞的文章标题为『王垠，请别再欺负我们读书少』，我现在想问问大家，到底是谁在显示他读书多，欺负大家读书少？我有强调过我读书多吗？我告诉大家的是，我脑子里的东西大部分都不是看书学来的，书本知识是不可靠的，每本书里面都只有一两章好点的地方。我的知识大部分是自己动手学会的，所以我才能做到融会贯通。
通过这些他对 pysonar 技术细节的分析，我看得出来彭飞看过一些 PL 领域的书和论文，记住了一些皮面知识和吓人的术语。满口的术语，可是却没有深刻的理解它们后面的涵义。他读书确实也够少的，见识太少，不知道天外有天。恐怕动手能力也不高，没动手实现过 CFA 领域任何一个算法。拿别人的代码来随便摆弄两下，也没有深入试验和观察，就以为自己可以造出一个大新闻：看，王垠是个大骗子！
看了一下彭飞的知乎专栏，他似乎喜欢显示一些鸡毛蒜皮的东西，把一些刚看过，没经过实践检验的理论，当成宝一样给给其它人讲，传道授业解惑一样，试图用这种方式树立自己的“权威地位”，让大家以为他是大牛人。他的文章经常出现一些比如“牛逼到爆”，“巅峰之作”一类的词汇，跟国内小编吹嘘国外大公司差不多的语气。他当然希望大家继续崇拜 PL 界的权威们，这样他们就可以瞎蒙混骗，写一些看不懂，实现不了，无法验证真伪的理论，继续高高在上，高深莫测的样子。所以，到底是谁在欺负我们读书少呢？
知乎的民科们班门弄斧，拿起石头砸了自己的脚，已经不止第一次了。我劝这些人还是好自为之。