Local Type Inference

ML语言的背后 众所周知, ML系语言十分强大, 这不仅仅得益于它们丰富的语义(高阶函数, local binding, lambda), 还得益于这套语义背后强大的类型系统. ML语言的类型系统通常支持十分强大类型推导功能, 强大到什么程度呢? 理论上开发者可以忽略所有类型签名, type checker仍然可以推导出所有的类型签名. 类型推导的两个"端点" 但是, 如此强大的类型推导技术居然也不小心带来了一些负面影响: 重要的类型签名被忽略. 很多情况下, 类型签名并不是开发者的负担而是起到了 “verified document” 的作用, 对可读性有着关键的影响. 类型系统的复杂度增加(主要是类型推导部分). 直观来看这点是在语言实现上的负面影响, 但是过于复杂的类型推导除了会提升类型检查的复杂度也会带来编程的"负担". 比如说开发者如果不能明确知道哪些类型能推导哪些类型不能推导, 那么考虑"要不要加上类型签名"的这个问题就会给程序员带来心智负担. 对于这些负面的影响, 最极端的做法就是我们要求把所有的类型都加上, 直接抛弃类型推导功能. 你不是说我推导不好吗, 那你自己写上吧. 但是这又带来了新的问题: 为所有类型写上类型签名实在是太啰嗦了, 维护一个冗长但是又没有意义的类型签名, 反而会带来编程时的心智负担. 很多类型签名实际上是"噪音". 如果完全抛弃类型推导, 那么在一个程序中, 有可能类型签名比描述程序执行信息的核心部分还要多, 这样的类型噪音甚至反而会影响程序的可读性. 尝试找到类型推导平衡点 那么有没有一种办法设计一个类型系统, 可以在描述ML丰富的语义的同时引入"适量"的类型推导: 当显式写出类型签名的对开发者有益的时候不推导这个类型, 只选择推导"显式写出时无意义"的类型签名. 局部类型推导(Local-Type inference)技术就诞生了 作者总结了3种ML编程中常见的类型推导, 并通过局部类型推导技术完成这三种类型推导: 函数调用时类型参数的推导是必要的 匿名函数的类型推导是需要的 local binding的类型推导是需要的 局部类型推导(Local-Type inference) 局部类型推导尝试在保持ML编程的前提下尽可能的减弱类型推导的能力以简化类型推导算法, 局部的含义是类型推导只用到了局部的语法树的类型信息. ...

September 5, 2023 · butterunderflow