转载

回应CFA传人对我的攻击

发表了之前的文章《我为什么不再做PL人》之后，我发现有人（其实是一位CFA技术的传人）在知乎上发表文章黑我。本来不想理知乎上的东西，但作者把各种刚从论文上学来的术语，似懂非懂写了一大堆，挺能唬人的，所以我只好回应一下。现在我把这篇文章的链接放在这里。评论的第4页有我的回复，技术性比较强，不过有兴趣的人可以看看。为了方便，我也把评论拷贝到这篇文章末尾。

文章作者彭飞的导师是Jens Palsberg，其实就是曾在CFA领域做过研究的一位学者。我本来对Palsberg没有意见，因为他的研究不只限于CFA。Palsberg还跟我很尊敬的Neil Jones教授做过很多其它方面的研究，所以我无意与他为敌，也从来没有在批评CFA的时候点过Palsberg的名。但由于我指出了CFA领域的弊病，彭飞恐怕就是一心一意研究这个的，所以觉得“祖业”受到了攻击，想要反驳我，支持CFA的“先进性”，这样以后可以在学术界更好的混下去。这可以理解，然而彭飞的文章，其实破绽百出，这些都从我的评论里可以看得出来。

CFA领域的理论从来没有成功实现，展示过它的功效。CFA最强大的版本，CFA2和P4F的作者Dimitris Vardoulakis，当年在Mozilla实习的时候试图在JavaScript上实现CFA2算法。最后的产物叫做“DrJS”，还做了一个网站让人试用。可是在不久之后DrJS不了了之，消失了。后来跟Mozilla的research director聊天时，他告诉我DrJS其实根本不好用，理论过度复杂，实现起来非常困难，而且达不到号称可以达到的效果，说Mozilla以后不想再赞助类似的项目了。之前在Sourcegraph的时候，两位founder也试图采用DrJS来做JavaScript的分析，后来发现不好用，改用了 tern 才产生了有用一点的信息。

PySonar2比CFA2，P4F都要强大的原因很简单，因为它根本没有CFA所用的continuation passing style（CPS变换）所带来的所谓“call/return匹配问题”。所有的call和它们的return，被abstract interpreter自然而然的匹配好了，根本不可能错位。我很惊讶的是CFA领域研究了20年，就在解决这种根本不存在的问题。彭飞抓住PySonar2表面上的一些小问题指指点点，貌似好大个事情，而其实很多都是由于他自己理解不够深入。详情请见我的评论。

另外，我真的对Python，Ruby，JavaScript这些动态语言做type inference不感兴趣了。PySonar2虽然比CFA简单和强大很多，但是我从来没想维护PySonar2的“先进性”，我从来没想推广PySonar2。因为我根本不在乎Python，也没把PySonar2当回事。给Python这样的语言做一个很好的类型推导工具，有什么意义吗？未来的方向是直接写上type annotation，就像Java和C#那样，让类型检查简单，迅速又准确。所以PySonar2和CFA领域做的其实都是无用功，只不过我没花20年时间研究CFA，只用了加起来几个月时间，而且还比他们做得更好。

彭飞错误地认为我很把PySonar2当回事，然而它只是我曾经做过的一个小玩具。我一直在探索和展望更加实在，对人可以产生真正效益的领域。只是随便提了一下CFA，就得到如此强烈而具体的攻击，我对PL人士的自我保护意识真的很惊讶。如果你观察到彭飞似乎对PL刚入门，在知乎上发表挺多入门级的PL文章，而且看CFA的论文也才不久，也许会意识到，他其实是想在知乎上建立自己的“权威地位”。由于最近研究的CFA受到了攻击，想要重新树立起小白们对于CFA的崇敬之情，倒也可以理解。知乎，真不愧是民科的天堂 :)

以下是我评论的内容，可能会略有改动：

不要以为我不上知乎你就可以随便胡扯。你的导师Jens Palsberg就是那帮CFA扯淡的人之一，你当然那么说了。CFA2的发明人在Mozilla做的那个东西（DrJS)，后来发现根本不能用（Mozilla research director亲自跟我说的），所以现在网站都消失了。

Pushdown Control Flow Analysis完全干的就是PySonar2很简单就能完成的事情，而PySonar2根本不需要什么pushdown automaton，完全依靠自然的abstract interpreter call/return。你们2016年才发那样的paper，PySonar2早在2010年就解决了这个问题。

另外那几个链接没有指向，是因为当时在Sourcegraph，他们需要一个fully qualified name，所以没法再同时指向两个地方。然而实际上reference其实都是有的。至于Hindley-Milner那种generic type的抽象，对于Python这种非常polymorphic的语言是不可行的。简单的a->a可以，但是控制流复杂一点就不能再有效。

另外，我真的对这种动态语言inference不感兴趣了。PySonar2虽然还是比你们的CFA先进很多年，但是我从来没想维护PySonar2的“先进性”。给Python这样的语言做一个很先进的工具，有什么意义吗？未来的方向是直接写上type annotation，就像Java和C#那样。所以我们做的都是无用功，只不过我没花你们那20年，而且还做得更好 ;)

另外我在2014年末的样子给CFA的“鼻祖”Olin Shivers写了封email，寻找合作机会。讲述了我的PySonar2的做法，而且问他为什么他的call/return match用那么复杂的方法来做。如果他们的2016论文加入了我的想法，也不足为怪。但是真的不care这些了。你们学术界随便胡搞好了，反正也不可能有什么用处。这些东西做static analysis的人早就明白，CFA远远落后，只能在自己的圈子里发表点paper。

另外，推导出的 {int -> int} | {bool ->bool}表示的其实是一个intersection type，而不是union type。我不知道你到底明不明白什么是intersection type。这个type表示这个函数“同时”是int->int和bool->bool，而不是表示“有时”是int->int而另外的时候是bool->bool。这是对于Python最多能做到的事情。

你说的forall a. a -> a对于复杂点的Python代码是不可行的。PySonar做过HM那样的系统，能推出forall a. a -> a那样的类型，但是后来发现遇到复杂点的代码根本不可能准确的generalize。有本事你用CFA给我们show一下推导出forall类型？我随便写段代码你的推导就完蛋了。

我从来没说过PySonar2是sound的。其实你们的CFA2和P4F，对于Python也不可能是sound的，因为本来就是undecidable的问题。这些工具能做的，只是最大限度的发现类型错误而已。它们并不能完全排除类型错误。

不得不引用一下Linus的话（虽然我鄙视这句话）：Talk is cheap. Show me some code。你把CFA实现出来，给我们show一下它能生成什么样的结果？哈哈。CFA2的发明人已经在Mozilla试过了不是吗？过度复杂的理论，根本不能实现和work。

原文 http://www.yinwang.org/blog-cn/2016/04/07/cfa

正文到此结束