Hindley-Milner 类型系统的根本性错误

By guenchi at 2018-02-06 • 0人收藏 • 227人看过

作者:王垠


之前的一个时间,我曾经公开过这样一段幻灯片,它是2012年10月的时候,我在 Indiana 大学做的最后一次演讲。由于当时的委婉,我并没有直接说出这些结论的重要性。其实它揭示了 ML 和 Haskell 这类基于 Hindley-Milner 类型系统的语言的一个根本性的错误。


这个错误来源于对一阶逻辑的“全称量词”(universal quantifier,通常写作∀)与程序函数之间关系的误解。在 HM 系统里面,多态(polymorphic)的函数能够被推导为含有全称量词的类型,比如 \x->x 的类型被推导为 ∀a.a->a,但 HM 系统决定这个全称量词的位置的方式,却是没有原则的。这就导致了类型变量(type variable)的作用域(scope)的偏差。


我的研究显示,这个错误来源于 HM 系统最初的一项重要的设计,叫做 let-polymorphism。如果右边的函数是一个多态的函数,比如:


let f = \x->x in

  ...


let-polymorphism 总是会把全称量词的位置确定在 let 的“=”右边。然而这是一个非常错误的做法,它的错误程度近似于早期的 Lisp 所采用的 dynamic scoping。这样做的结果是,全称量词的位置会随着程序的“格式”,而不是程序的“结构”,而变化。至于什么是 dynamic scoping,你可以参考我的这篇博文


为了弥补这个错误,30多年来,许多的人发表了许多的论文,提出了很多的“改进措施”,比如 value restriction,MLF,等等。但是我的研究却显示,所有这些“改进措施”都是丑陋的 hack。因为他们没有看到问题的根源,所以他们的方案只对一些特殊情况起作用,而不能通用。为此,我可以轻而易举的写出正确的程序,而让它不能通过这些类型系统的检查,比如像我这篇英文博文所示。如果你看到了问题的根源,就会发现 HM 系统的这个错误是无法弥补的,因为它触及了 HM 系统的根基。为了根治这个问题,let-polymorphism 必须被去除掉。


我为此提出了自己的解决方案:在 lambda 的位置进行“generalization”,也就是说把 ∀ 放在 lambda 的位置,而不是 let。这样一来 let-polymorphism 就不存在了。但是这样一来,HM 系统就不再是 HM 系统,因为它的“模块化类型推导”的性质,就会名存实亡。由于类型里面含有程序的“控制结构”,这个类型系统表面上看起来是在进行“模块化类型检查”,而本质上是在做一个“跨过程静态检查”(interprocedual static analysis)。也就是说,模块化的类型推导,在 HM 这样的没有“类型标记”的体系下,其实是不可能实现的。


为了达到完全通用的模块化类型检查,却又允许多态函数的存在,我们终究会需要在函数的参数位置手工写上类型,这样我们就完全的丧失了 HM 系统设计的初衷。


登录后方可回帖

登 录
信息栏

Scheme中文社区

推荐实现 ChezScheme / r6rs / r7rs large
theschemer.org
Q群: 724577239

精华导览

社区项目

包管理器:Raven
HTTP服务器:Igropyr (希腊火)
官方插件:vscode-chez

社区目标:

完善足以使Scheme工程化和商业化的库,特别是开发极致速度的Web服务器和ANN模块。

一直以来Scheme缺少一个活跃的中文社区,同时中文资料的稀少,导致大多数因为黑客与画家和SICP而接触Scheme的朋友,在学完SICP后无事可做,不能将Scheme转换为实际的生产力。最后渐渐的放弃。
同时Chicken等实现,却因效率问题无法与其他语言竞争。本社区只有一个目的,传播Scheme的文明之火,在最快的编译器实现上,集众人之力发展出足够与其他语言竞争的社区和库。


友情链接:

Clojure 中文论坛
函数式·China


Loading...