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

发表了之前的文章《我为什么不再做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->intbool->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的输入。所以就左右不是人。

其实如果彭飞仔细看那两个变量ab的类型,就会发现这是intersection type,而不是union type。

可能有人对这里的intersection type有所误解。int -> int ∧ bool ->bool,在这里其实不是表示这个函数只能接受int或者bool的输入,而只是表示这个函数在某些调用的地方输入了int或者bool,然后分别输出了intbool。所以在“官方意义”下,这并不是这个函数的类型。那么这个函数的类型是什么呢?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是一个什么样的函数,它是同时能接受intbool,还是其实能接受所有类型,也就是forall a. a->a呢?类型推导不能确定这个范围,所以只能假设f不可以是一个polymorphic的函数,所以发现f被同时输入了1True,就报错了。

这是一个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.xB.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界的权威们,这样他们就可以瞎蒙混骗,写一些看不懂,实现不了,无法验证真伪的理论,继续高高在上,高深莫测的样子。所以,到底是谁在欺负我们读书少呢?

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