backup

作者:王垠

到底是谁在欺负我们读书少？

发表了之前的文章《我为什么不再做PL人》之后，我发现有人在知乎上发表文章诬蔑我。本来不想理知乎上的东西，但作者把各种刚从论文上学来的术语，似懂非懂，照本宣科列了一大堆，挺能唬人的，说起来很像那么回事儿，所以我只好破例回应一下，但是下不为例。

现在我把这篇文章，题名『王垠，请别再欺负我们读书少』的链接放在这里，供大家观看。评论的第4，第6页有我的回复，技术性比较强，不过有兴趣的人可以看看。为了方便，我也把评论整理和拷贝到这篇文章第二节。

历史和事实

文章作者彭飞自称导师是Jens 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。因为我根本不在乎Python，也没把PySonar2当回事。给Python这样的语言做一个很好的类型推导工具，有什么意义吗？未来的方向是直接写上type annotation，就像Java和C#那样，让类型检查简单，迅速又准确。所以PySonar2和CFA领域做的其实都是无用功，只不过我没花20年时间研究CFA，只用了加起来几个月时间，而且还比他们做得更好。

我在2014年末的样子给CFA的“祖师爷”Olin Shivers写了封email，寻找合作机会。我跟他讲述了PySonar2的做法，而且问他为什么他的call/return match用那么复杂的方法来做，然而他没有回我的email。这是一个不祥的预兆，因为我一直在犹豫是否应该告诉这些人，有简单很多倍的办法，可以达到同样的目的。他们完全可以“借鉴”我的做法，然后写进论文里面发表。所以如果他们的2016论文加入了我的想法，也不足为怪。但是真的不在乎这些了，学术界随便胡搞就胡搞呗，反正也不可能有什么大的用处。这些东西，其实做static analysis的人早就明白，CFA远远落后，只能在自己的圈子里发表点paper。

彭飞错误地认为我很把PySonar2当回事，然而它只是我曾经做过的一个小玩具。我一直在探索和展望更加实在，对人可以产生真正效益的领域。只是随便提了一下CFA，就得到如此强烈而具体的攻击，我对PL人士的自我保护意识真的很惊讶。

技术部分

以下是针对彭飞提出的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 1In 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大的原理和结构都是非常好的，这些小问题真是不值一提，很容易fix。

反复的提到“语义分析”（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界的权威们，这样他们就可以瞎蒙混骗，写一些看不懂，实现不了，无法验证真伪的理论，继续高高在上，高深莫测的样子。所以，到底是谁在欺负我们读书少呢？

知乎的民科们班门弄斧，拿起石头砸了自己的脚，已经不止第一次了。我劝这些人还是好自为之。