类型推导与不死代码
译自：Type inference and the undead code。除非特殊声明，下文『我』指原文作者 Oleg Kiselyov。 类型推导算法通常依赖于代码上下文，因而不具有组合性。Hindley-Milner 风格的类型推导的设计中，明确允许了『蒐集类型约束并求解』的过程中上下文影响/确定表达式（如变量）的类型。不过，类型推导算法的非组合性质有时也会给人们带来『惊喜』。例如，类型良好的『明显死代码』会影响整片代码的可赋类型性（typeability），甚至会影响其运行结果。本文的写作动机源于我与 Andreas Abel 自 2012 年 7 月始在 Haskell Cafe 邮件列表的进行的一系列讨论，他希望把讨论期间提出的各种示例记录下来。本文就是为了完成这一愿望－－收集，扩展和完善这些示例并建立它们内在的联系。 『死代码』通常指没有数据流和控制流流过的表达式。本文使用该术语专门表示无关的变量定义：即类型良好且无副作用，也没有数据流和控制流流过的变量定义，这些定义的标识符甚至不能出现在相关的表达式中。 首先从最简单，最广为人知的例子开始。在例子中，无关的定义导致了表达式无法被赋予类型。读者肯定在任何使用 Hindley-Milner 风格的类型推导的语言中都见过这样的例子。下面用 OCaml 的一个简单子集具体展示： let exp = let id = fun u -> u in let f = id id in let z = fun () -> f true in f 1 这段代码无法通过类型检查，检查器报告表达式 f 1 的类型错误。但是，如果我们删除 z 的定义（f 1 中显然没有出现 z），修改后的程序突然就变成类型良好的了。 练习：是否存在其他合法（从动态语义的角度）的代码转换能使 exp 的类型正确？ 在 Haskell 98 及以上版本中，类似的问题常常与臭名昭著的 MonomorphismRestriction 相关：...