译自：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 相关：
f = print
exp = f 1
z = f True
上述代码也无法通过检查，编译器将失败的原因归咎于 f 1 中的 1。同样的，z 的定义（实际编程中它可能出现在程序若干行后）显然与 exp 无关。但当我们删除该定义，程序就能通过检查并顺利运行。诚然 MonomorphismRestriction 是导致这种错误的惯犯，但也它也并非每次都是罪魁祸首。例如：
exp = do
f <- return id
r <- return (f 1)
z <- return (f True)
print r
在上面的代码中，z 的定义在 r 之后，但是它却『误导』了类型检查器，使检查器认为表达式 r 的定义中的字面量 1 有问题。这次的问题与 MonomorphismRestriction 或者是否有显式类型签名无关。
上述的所有例子，类型推导无法直接从 f 的定义中完全推导其类型，要完全推导则必须了解其使用时的上下文。像 z 的定义这样的死代码尽管对 exp 的求值结果无关，但因为它调用了 f ，导致类型检查器被误导了。值得思考的是为什么类型检查器在『活』代码中报错而非死代码（尽管死代码出现在活代码之后）。
另一个鲜为人知的事实是，死代码也可能会产生相反的效果：删除死代码导致无法对原本的程序赋予类型。尽管从计算的角度看，这样的代码什么也不做，但是从类型检查器的角度看，它还是做了一些有用的事情。例如，以下程序可以成功编译：
let id = fun u -> u
let f = id id
let exp x = f x
let z () = f True
如果我们删除 z 的定义，程序就无法编译了：编译器会认为 f 的定义有问题，并指出其类型『包含了无法被泛化的类型变量』。下面提供一个 Haskell 98 中的类似例子：
main = do
x <- return []
print (x == x)
let z = (x == "")
return ()
该例子也能通过类型检查并成功运行。如果我们删除了看起来无关，且晚于 x 定义的 z，类型检查器会抱怨『x == x 中的 == 产生了有歧义的类型变量 t0』。有时候，死掉的代码也可以通过约束检查器来帮助活着的代码。
最令人惊讶的是，就算死代码根本没有被执行，它也可能会影响程序执行的结果。下面的例子来自 Haskell 98:
instance Num Char
main = do
x <- return []
print x
let y = abs (head x)
let z = (x == "")
return ()
运行这段代码将打印 ""，如果我们删除无关的 z 定义，程序却会改为打印 []。顺带一提，这段程序中的 y 也是一个无关的定义，试想一下如果删掉它会发生什么？
下面是一个更简单的 Haskell 98 例子，该例子提炼自 Andreas Abel 的学生在某些图形相关代码的 RGB 转换部分遇到的问题。这个例子也说明本文谈论的不仅仅是一个学术问题：
main = do
x <- return (2^65)
print (x == 0)
let z = x > length []
return ()
上述程序打印 True，若删除 z 定义，程序将打印 False。
我们似乎不应该对类型推导算法的上下文有关性质感到惊讶。类型推导的本质是通过猜测每个子表达式的类型，最终为整个表达式赋予类型。为了使算法对于对相同表达式总是推导出相同类型，推导算法使用了一种叫做『惰性猜测』的手段，即：用新的类型变量表示可能的猜测，随着推导的进行看到更多的上下文，最终用具体的类型取代类型变量。
导致上述所有例子产生问题的幕后黑手其实是『类型变量被引入到的作用域不同』。对于某类型变量，最『自然』的作用域即其定义作用域，let 绑定的作用域。若某些类型变量在检查该作用域之后都无法确定具体类型，那么类型推导系统会尝试泛化该类型变量。如果无法/不适用泛化怎么办？一种设计选择是以类型错误为由拒绝这种定义－－Andreas Abel 指出这正是 Agda 的做法。MetaOCaml 也采取类似的做法，不过针对的是生成的代码中的变量－－若发现变量逃逸出预期绑定的作用域，则立即终止代码生成。
个人猜测，有的语言设计者认为将类型变量限制在其定义的作用域内过于严格了。这些设计者决定允许类型变量逃逸到更大的上下文中，希望这样能找到该类型变量的具体类型。在这种情况下，表达式定义的类型不仅由其定义侧决定，还由其使用侧决定。这种非组合性令某些人（尤其是 Andreas Abel）感到反感。尽管如此，Haskell 和 OCaml 也对类型变量施加了基于『编译单元』的严格限制。在类型检查整个编译单元，编译器发现某些变量未绑定且未被泛化时将采取措施。OCaml 编译器选择拒绝编译该编译单元，而 Haskell 则先尝试应用默认类型规则，如果不起作用，则声明该程序的类型有歧义。
大多数时候，类型推导的这种『非组合性』是无害的－－表达式的类型上下文如果发生冲突，也许会导致程序无法通过类型检查，但不会改变其运行结果。然而，当我们引入诸如『默认类型（type defaulting）』、『反射（reflection）』、『重叠实例（overlapping instance）』等特性时，『好』日子还在后头呢。
引用文献
Haskell Wiki 上 MonomorphismRestriction 的页面收集了更多该特性带来的『惊喜』。
拥有无限制作用域的全局类型变量其实类似于与被生成的代码中的变量名。引用论文中开发的 <NJ> 演算用特殊的『命名堆』来追踪这种变量名，以确保这些名字的作用域正确。