Is sound gradual typing dead 解读

Is sound gradual typing dead? 主要研究sound gradual typing在编译中的收益问题，结论认为通过gradual type来指导编译优化是一件不划算的事情。

简介

动态类型语言在构建（或者生长）出复杂软件系统的时候会因为缺少可靠的类型信息而变得难以维护。一种解决方法是通过扩展语言，增量的增加类型信息。Gradual typing就是通过type annotation在typed和untyped代码边界增加run-time check，来建立type soundness。

这种Gradual typing的使用有两个隐含的要求。首先，类型系统适应常见的无类型的编程习惯。这允许程序员在添加类型时对现有代码进行最小的改动。其次，性能代价是可以容忍的，理想情况下新增加的类型对于性能优化应该是有益的。

而这篇文章通过实验手段评估了Gradual type system对性能的影响，结论是这种类型系统的代价是不可容忍的，因此提出了sound gradual typing is dead。

实验结论

实验基于Typed Racket实现，方法是对于一个完整程序，对其中n个模块标注type。实现一个lattice，Top是全部模块typed，Bottom是全部模块untyped，然后进行性能测试。

如图所示是一个通过执行时间对比的pyerformance lattice，被涂色的圆点表示typed module，未涂色的表示untyped module。当所有模块被标注类型之后（Top），性能提升约30%。说明当可以对任意operator、field access执行specialization和type check的情况下，对性能是有益的。

然而对于几乎所有的部分类型标注都出现了不同程度的性能下降。实验中观察到如下几点：

• 对main模块增加annotation对性能几乎没有影响，因为它只是一个驱动模块；
• 在任何一个主要模块–data、label或structs–上添加类型，而其他模块不添加类型，会导致速度至少降低35x。这组模块是紧密耦合的。增加一个未类型化的边界来分隔这组模块的元素，会导致相互引用时，增加相关的检查成本；
• 进一步观察data和label可以发现，后者通过一个适配器模块依赖于前者。当两个模块中的任何一个没有类型化时，这个适配器引入了一个边界检查。当这两个模块都是类型化的，但所有其他模块都是未类型化的，速度就会降低到13x左右。structs模块以同样的方式依赖于data，另外还依赖于label。因此，在structs和data都被类型化的配置中，仍然有很大的减慢。当所有三个模块都被类型化时，速度会降低到5x；
• 最后，接近最差减速情况的配置是data未被类型化，但其他几个模块被类型化。考虑到上面提到的耦合性，这是有道理的；在未类型化的数据和其他类型化的模块之间引起的巨大性能降低；

误差

原文中认为可能影响实验结论的几个点：

• Benchmark太小并且每种配置一个core并发执行的（这个地方听起来有点扯）；
• Benchmark所引用的其他库都是untyped；
• 对一个具体变量type annotation很少是唯一的，这种选择可能会影响性能；
• Typed Racket自身实现的问题，它会编译成Racket并且使用一个传统的JIT编译。它没有尝试消除冗余的类型检查；

个人评价

感觉实验结果并不靠谱，特别是Typed Racket本身的编译实现和优化能力相当值得怀疑。但是至少说明两点：

• 即便是依赖库untyped的情况下，对全程序进行类型标注也是有益的，这预示着对于大型程序来说，部分核心代码进行类型标注从而带来性能提升是可行的；
• type check的负载在相当多的情况下是无法用带来的优化消除的，类型特化这类的优化可能需要更加精确才行；