15 静态地检查程序中的不变量：类型
当程序变得更大或者更为复杂时，程序员希望能有工具帮助他们描述、验证程序中的不变量。顾名思义，不变量指的就是关于程序组成元素的那些不会发生改变的陈述。例如，当我们在静态类型语言中写下x : number时，表示 x 中存放的总是数，程序中依赖 x 的部分都可以认定它是数的这个事实不会改变。我们将会看到，类型只是我们想要陈述的各类不变量中的一种，静态类型检测——一个分支众多的技术家族——也只是用于控制不变量的众多方法中的一个。
15.1 静态类型规则
本章我们将专注于静态类型检查：即在程序执行前检查（声明的）类型。之前使用的静态类型语言已经让我们积攒了一些这种形式程序的经验。我们将探索类型的设计空间及这些设计中的权衡取舍。尽管类型是控制不变量的一种非常强大且有效的方法，最后我们还是会考察一些其它可用的技术。
考虑下面这段静态语言写就的程序：
(define (f [n : number]) : number
(+ n 3))
(f "x")
程序开始执行前我们就会得到一个静态类型错误。使用普通 Racket 写就的同样的程序（去除类型注解）只会在运行时出错：
(define (f n)
(+ n 3))
(f "x")
练习题
如何判断错误是在程序执行前还是运行时抛出的？
考虑下面这段 Racket 程序：
(define f n
(+ n 3))
它也是在程序执行前就遇到错误——语法解析错误——终止。尽管我们认为语法解析和类型检查有所不同——通常是因为类型检测是针对已经被解析好的程序做的——但是将语法解析看作一种最简单形式的类型检查也很有用：它（静态地）判定程序是否遵守某个上下文无关语法。随后，类型检查判定它是否遵守某个上下文相关（或者一个更丰富的）语法。简而言之，类型检查从某种程度上看是语法解析的泛化，它们都是通过语法控制程序遵循指定的规则。
15.2 关于类型的经典看法
我们先介绍传统的包含类型的核心语言；然后我们将探索其扩展和变种。
15.2.1 简单的类型检查器
要定义类型检查器，我们先需要就两件事达成一致：我们静态类型核心语言的语法，对应的类型的语法。
先回到我们之前实现过的函数作为值的那一版语言，其中并不包含赋值等其它稍复杂的东西（后面将讲到添加其中的一些）。我们需要为该语言添加类型注解。按惯例，我们不对常量或基本操作（如加法）强加类型注释；相反，我们把类型注释加在函数或方法的边界上。在本章讨论的过程中，我们将探讨为什么这么做。
鉴于此决定，我们静态类型的核心语言变成了：
(define-type TyExprC
[numC (n : number)]
[idC (s : symbol)]
[appC (fun : TyExprC) (arg : TyExprC)]
[plusC (l : TyExprC) (r : TyExprC)]
[multC (l : TyExprC) (r : TyExprC)]
[lamC (arg : symbol) (argT : Type) (retT : Type) (body : TyExprC)])
每个函数都添加了其参数及返回值类型的注解。
现在我们需要对类型语言作出选择。我们遵从传统定义，即类型是一组值的集合的抽象。我们的语言中有两类值：
(define-type Value
[numV (n : number)]
[closV (arg : symbol) (body : TyExprC) (env : Env)])
因此我们有两种类型：数和函数。
即使数类型也并不那么简单直接：数类型应该记录何种信息？大部分语言中，实际上有很多数类型，甚至没有哪个类型表示“数”。然而，我们忽略了数的层级结构（译注，第三章），对于我们来说有一种数的类型足矣。这样决定之后，我们是否需要记录哪种数的信息？ 原则上可以，但这样我们很快就会遇到可判定性问题。
至于函数，我们有更多信息：参数的类型，返回值的类型。我们不妨记录下这些信息，除非事后证实这些信息没有用处。结合这些，我们得出这样的类型的抽象语言：
(define-type Type
[numT]
[funT (arg : Type) (ret : Type)])
既然已经确定了语言中项和类型的结构，接下来我们来确定语言中哪些算是类型错误（并且，如果程序中不包含这里列出的类型错误，它就会通过类型检查）。显然有三种形式的类型错误：
+的参数不是数，即不是numT。*的参数不是数。- 函数调用时函数位置的表达式不是函数，即不是
funT。
思考题
还有其它形式的类型错误吗？
事实上我们遗漏了一个：
- 函数调用时实参的类型和函数形参的类型不一致。
我们的语言中的所有其他程序似乎都应该通过类型检查。
关于类型检查器的签名，初步设想，它可以接受表达式作为参数，返回布尔值指明该表达式是否通过检查。由于我们知道表达式中包含标识符，所以很显然我们还需要一个类型环境，它将名字映射到类型，类似于我们之前用到的值环境。
练习题
定义与类型环境相关的数据类型以及函数。
于是，我们开始写下的程序结构大致是这样：
<tc-take-1> ::= ;;类型检查，第一次尝试
(define (tc [expr : TyExprC] [tenv : TyEnv]) : boolean
(type-case TyExprC expr
<tc-take-1-numC-case>
<tc-take-1-idC-case>
<tc-take-1-appC-case>))
正如上面程序中列出的要处理几种情形所表明的，这种方法行不通。我们很快将知道这是为什么。
首先处理简单的情形：数。单独的一个数能通过类型检查吗？显然可以；它所处的上下文可能想要的不是数类型，但是这种错误应该在其它地方被检查出。因此：
<tc-take-1-numC-case> ::=
[numC (n) true]
下面处理标识符。如何判断标识符是否通过类型检查呢？同样，就其自身来说，如果是绑定标识符，总是通过检查的；它可能不是上下文要求的那种类型，但是这种错误应该在其它地方检查。因此，我们得出：
<tc-take-1-idC-case> ::=
[idC (n) (if (lookup n tenv)
true
(error 'tc "not a bound identifier"))] ;不是绑定标识符
上面的代码你可能感觉不太对：如果标识符未绑定的话，lookup会抛出异常，因此没必要再去重复处理该情况（事实上，代码永远不会执行到error调用那个分支）。但是让我们先继续。
下面来处理函数调用。我们应该首先检查函数位置，确定它是个函数，然后确保实际参数的类型和该函数定义时声明的形式参数类型相同。例如，函数可能需要参数是数，但调用给的是个函数，或者反之，在这两种情况下，我们都需要防止错误的函数调用。
代码该怎么写？
<tc-take-1-appC-case> ::=
[appC (f a) (let ([ft (tc f tenv)])
...)]
对于tc的递归调用只能让我们知道函数位置是否通过类型检查。如果它通过了，怎么知道它具体是什么类型的呢？如果是个简单的函数定义的话，我们可以直接从语法上取得其参数和返回值的类型。但是如果是个复杂的表达式，我们就需要一个函数能计算出表达式类型。当然，只有这个表达式是个类型正确的表达式时，该函数才能返回类型结果；否则的话它将不能得出正确的结果。换句话说，“类型检查”是“类型计算”的一种特殊情形！因此，我们应该增强tc的归纳不变量：即，不仅仅返回表达式是否能通过类型检查，而是返回表达式的类型。事实上，只要有返回值，就说明该表达式通过了类型检查；否则它会抛出错误。
下面我们来定义这个更完善的类型“检查器”。
<tc> ::=
(define (tc [expr : TyExprC] [tenv : TyEnv]) : Type
(type-case TyExprC expr
<tc-numC-case>
<tc-idC-case>
<tc-plusC-case>
<tc-multC-case>
<tc-appC-case>
<tc-lamC-case>))
现在填充具体实现。数很简单：它的类型就是数类型。
<tc-numC-case> ::=
[numC (n) (numT)]
与之相似，标识符的类型从环境中查询得到（如果其未被绑定则会抛出错误）。
<tc-idC-case> ::=
[idC (n) (lookup n tenv)]
到此，我们可以观察到该类型检查器与解释器之间的一些异同：对于标识符，两者做的事情其实一样（只不过这里返回的是标识符的类型而不是一个实际的值），对于数的情况，这里返回了抽象的“数”而不是具体的数。
下面考虑加法。必须确保其两个子表达式都具有数类型；如果满足该条件，则加法表达式本身返回的是数类型。
<tc-plusC-case> ::=
[plusC (l r) (let ([lt (tc l tenv)]
[rt (tc r tenv)])
(if (and (equal? lt (numT))
(equal? rt (numT)))
(numT)
(error 'tc "+ not both numbers")))] ;+不都是数
通常在处理完加法的情形之后，对于乘法我们就一笔带过了，但是这里显式处理一下它还是很有教益的：
<tc-multC-case> ::=
[multC (l r) (let ([lt (tc l tenv)]
[rt (tc r tenv)])
(if (and (equal? lt (numT))
(equal? rt (numT)))
(numT)
(error 'tc "* not both numbers")))] ;*不都是数
思考题
看出其中的区别了吗？
是的，基本上完全没区别！（仅有的区别是在type-case时使用的分别multC和plusC，以及错误提示信息稍有不同）。这是因为，从（此静态类型语言）类型检查的角度来说，加法和乘法没有区别，更甚，任意接受两个数作为参数返回一个数的函数都没有区别。
注意到代码解释和类型检查之间另一个不同点。它们的参数都得是数。解释器返回加或者乘它们得到的确切数值，但是类型检查器并不在乎具体的数值：因此该表达式的计算结果（(numT)）是个常数，两种情形返回都是该常数。
最后还剩下两个难一点的情形：函数调用和函数。我们已经讨论过怎么处理函数调用：计算函数以及参数表达式的值；确保函数表达式为函数类型；检查参数类型和函数形参类型相容。如果这些条件满足，函数调用得到的结果类型就是函数体的类型（因为运行时最终的返回值就是计算函数体得到的值）。
<tc-appC-case> ::=
[appC (f a) (let ([ft (tc f tenv)]
[at (tc a tenv)])
(cond
[(not (funT? ft))
(error 'tc "not a function")] ;不是函数
[(not (equal? (funT-arg ft) at))
(error 'tc "app arg mismatch")] ;app参数不匹配
[else (funT-ret ft)]))]
最后还剩下函数定义。函数有一个形参，函数体中一般会用到；除非它被绑定到环境中，不然函数体应该不太可能通过类型检查。因此我们需要扩展类型环境，添加形参与其类型的绑定，然后在扩展后的环境中检查函数体。最终计算得到的函数体类型必须和函数定义中指定的函数返回值类型相同。如果满足了这些，该函数的类型就是指定参数类型到函数体类型的函数。
练习题
上面说的“不太可能通过类型检查”是什么意思？
<tc-lamC-case> ::=
[lamC (a argT retT b)
(if (equal? (tc b (extend-ty-env (bind a argT) tenv)) retT)
(funT argT retT)
(error 'tc "lam type mismatch"))] ;λ类型不匹配
注意到解释器与类型检查器另一个有趣的不同点。解释器中，函数调用负责计算参数表达式的值，扩展环境，然后对函数体求值。而这里，函数调用的情形中的确也检查了参数表达式，但是没有涉及到环境的处理，直接返回了函数体的类型，而没有遍历它。对函数体的遍历检查过程实际是在检查函数定义的过程中进行的，因此环境也是在这个地方才实际被扩展的。
15.2.2 条件语句的类型检查
考虑为上面的语言添加条件语句，即使最简单的 if 表达式都会引入若干设计抉择。这里我们先讨论其中的两个，后面会回过头讨论其中的一个。
- 条件表达式的类型应该是什么？某些语言中它必须计算得到布尔值，这种情况下需要为我们的语言添加布尔值类型（这可能是个好主意）。其它语言中，它可以是任意值，某些值被认为是“真值”，其它的则被视为“假值”。
then-和else-两个分支之间的关系应该是什么呢？一些语言中它们的类型必须相同，因此整个 if 表达式有一个确定无歧义的类型。其它语言中，两个分支可以有不同的类型，这极大地改变了静态类型语言的设计和它的类型检查器，而且也改变了编程语言本身的性质。
练习题
为该静态类型语言添加布尔值。至少需要添加些啥？在典型的语言中还需要加什么？
练习题
为条件语句添加类型规则，其中条件表达式应该计算得到布尔值，且
then-和else-分支必须有相同的类型，同时该类型也是整个条件语句的类型。
15.2.3 代码中的递归
现在我们已经得到了基本的编程语言，下面为其添加递归。之前我们实现过递归，可以很容易的通过去语法糖实现。这里的情况要更复杂一些。
15.2.3.1 递归的类型，初次尝试
首先尝试表示一个简单的递归函数。最简单的当然就是无限循环。我们可以仅使用函数实现无限循环吗？可以：
((lambda (x) (x x))
(lambda (x) (x x)))
因为我们的语言中已经支持将函数作为值。
练习题
为什么这会构成无限循环？它是如何巧妙地依赖于函数调用的本质的？
现在我们的静态类型语言要求我们为所有函数添加类型注解。我们来为该函数添加类型注解。简单起见，假设从现在开始我们写的程序使用的语法是静态类型的表层语法，去语法糖将帮我们将其转换为核心语言。
首先注意到，我们有两个完全一样的表达式，它们互相调用。历史原因，整个表达式被称为Ω（希腊字母大写欧米茄），那两个一样的子表达式被称为ω（希腊字母小写欧米茄）。两个一样的表达式并非得是同种类型的，因为这还依赖于具体使用环境中对于不变量的定义。这个例子中，观察到 x 被绑定到ω，于是ω将出现在在(x x)式子的第一个和第二个部分。即，确定其中一个表达式的类型，另一个式子的类型也被确定。
那么我们就来尝试计算ω的类型；称该类型为γ。显然它是一个函数类型，而且是单参数的函数，所以它的类型必然是φ -> ψ这种形式的。该函数的参数是什么类型？就是ω的类型。也即，传入φ的值的类型就是γ。因此，ω的类型是γ，也即φ -> ψ，展开即(φ -> ψ) -> ψ，进一步展开得((φ -> ψ) -> ψ) -> ψ，还可以继续下去。也就是说，该类型不能用有限的字符串写出来！
思考题
你注意到了我们刚做的的微妙但重要的跳跃吗？
15.2.3.2 程序终止
我们观察到，试图直接地计算Ω的类型，需要先计算γ的类型，这似乎导致了严重的问题。然后我们就得出结论：此类型不能用有限长度的字符串表示，但是这只是直觉的结果，并非证明。更奇怪的事实是：在我们迄今定义的类型系统中，根本无法给出Ω的类型！
这是一个很强的表述，但事实上我们可以给出更强的描述。我们目前所用的静态类型语言有一个属性，称为强归一化（strong normalization）：任何有类型的表达式都会在有限步骤后终止计算。换句话，这个特殊的（奇特的）无限循环程序并不是唯一不可获得类型的程序；任何无限循环（或潜在存在无限循环）程序都无法求得类型。一个简单的直觉说明可以帮助我们理解，任何类型——必须能被有限长度的字符串表示——只能包含有限个->，每次调用会去除一个->，因此我们只能进行有限次数的函数调用。
如果我们的程序只允许非转移程序（straight-line program），这点也无足为奇。但是，我们有条件语句，还有可以当做值任意传递的函数，通过这些我们可以编码得到任何我们想要的数据结构。然而我们仍能得到这个保证！这使得这个结果令人吃惊。
练习题
试着使用函数分别在动态类型和静态类型语言中编码实现链表。你看到了什么？这说明此类型系统对于编码产生了何种影响？
这个结果展示了某种更深层次的东西。它表明，和你可能相信的——类型系统只是用来避免一些程序 BUG 在运行时才被发现——相反，类型系统可能改变语言的语义。之前我们一两行就能写出无限循环，现在我们怎么都写不出来。这也表明，类型系统不仅可以建立关于某个特定程序的不变量，还能建立关于语言本身的不变量。如果我们非常需要确保某个程序将会终止，只要用该语言来写然后交由类型检查器检查通过即可。
一门语言，用其书写的所有程序都将终止，有什么用处？对于通用编程来说，当然没用。但是在很多特殊领域，这是非常有用的保证。例如，你要实现一个复杂的调度算法；你希望知道调度程序保证会终止，以便那些被调度的任务被执行。还有许多其他领域，我们将从这样的保证中受益：路由器中的数据包过滤器；实时事件处理器；设备初始化程序；配置文件；单线程 JavaScript 中的回调；甚至编译器或链接器。每种情况下，我们都有一个不成文的期望，即这些程序最终会终止。而现在我们有一个语言能保证这点——且这点是不可测试的。
这不是假想的例子。在Standard ML语言中，链接模块基本上就是使用这种静态类型语言来编写模块链接规范。这意味着开发人员可以编写相当复杂的抽象概念——毕竟可以将函数作为值使用——且同时链接过程被保证会终止，产生最终的程序。
15.2.3.3 静态类型的递归
这就意味着，之前我们可以只通过去语法糖来实现rec，现在则必须在我们的静态类型语言中显式的实现。简单起见，我们仅考虑rec的一种特殊形式——它涵盖了常见用法，即递归标识符被绑定到函数。因此，表层语法中，我们可能写出如下的累加函数：
(rec (Σ num (n num)
(if0 n
0
(n + (Σ (n + -1))))) ;译注，原文如此，+应前置
(Σ 10))
其中，Σ是函数名，n为其参数，num为函数参数以及返回值的类型。表达式(Σ 10)表示使用该函数计算从 10 累加到 0 的和。
如何计算这个表达式的类型？显然，求类型过程中，n在函数体中的类型需要绑定（但是在函数调用处就不需要了）；这一点计算函数类型的时候我们就知道了。那么Σ呢？显然，在检查(Σ 10)的类型时，它应该在类型环境中被绑定，类型必须为num -> num。不过，在检查函数体时，它同样需要被绑定到此类型。（还要注意，函数体返回值的类型需要和事先声明的返回类型相同。）
现在我们可以看到如何打破类型有限性的束缚。程序代码中，我们只能编写包含有限数量->的类型。但是，这种递归类型的规则在函数体中引用自身时复制了->，从而供应了无穷的函数调用。这是包含无穷箭矢的箭筒。
实现这种规则的代码如下。假设f被绑定到函数的名字，aT是函数参数的类型，rT为返回类型，b是函数体，u是函数的使用：
<tc-lamC-case> ::=
[recC (f a aT rT b u)
(let ([extended-env
(extend-ty-env (bind f (funT aT rT)) tenv)])
(cond
[(not (equal? rT (tc b
(extend-ty-env
(bind a aT)
extended-env))))
(error 'tc "body return type not correct")] ;函数体类型错误
[else (tc u extended-env)]))]
15.2.4 数据中的递归
我们已经见识了静态类型的递归程序，但是它还不能使我们创建递归的数据。我们已经有一种递归数据——函数类型——但是这是内建的。现在还没看到如何创建自定义的递归数据类型。
15.2.4.1 递归数据类型定义
当我们说允许程序员创建递归数据时，我们实际在同时谈论三种东西：
- 创建新的类型
- 让新类型的实例拥有一个或多个字段
- 让这些字段中的某些指向同类型的实例
实际上，一旦我们允许了第三点，我们就必须再允许一点：
- 允许该类型中非递归的基本情况的存在
这些设计准则的组合产生了通常被称为代数数据类型（algebraic datatype）的东西，比如我们的静态语言中支持的类型。举个例子，考虑下面这个数二叉树的定义：【注释】
(define-type BTnum
[BTmt]
[BTnd (n : number) (l : BTnum) (r : BTnum)])
后面我们会讨论如何参数化类型。
请注意，如果这个新的数据类型没有名字，BTnum，我们将不能在BTnd中引用回该类型。同样地，如果只允许定义一种BTnum构造，那么就无法定义 BTmt，这会导致递归无法终止。当然，最后我们需要多个字段（如BTnd中的一样）来构造有用、有趣的数据。换句话说，所有这三种机制被打包在一起，因为它们结合在一起才最有用。（但是，有些语言确实允许定义独立结构体。后文我们将回来讨论这个设计决策对类型系统的影响）。
我们关于递归表示的初步讨论暂告一个段落，但这里有个严重的问题。我们并没有真正解释这个新的数据类型BTum的来源。因为我们不得不假装它已经在我们的类型检查器中实现了。然而，为每个新的递归类型改变我们的类型检查器有点不切实际——这就好比需要为每个新出现的递归函数去修改解释器！相反，我们需要找到一种方法，使得这种定义成为静态类型语言的固有能力。后面我们会回来讨论这个问题。
这种风格的数据定义有时也被称为乘积的和，“乘”指代字段组合成不变量的方式：例如，BTnd的合法值是传递给BTnd构造器的每个字段合法值的叉乘。“和”是所有这些不变量的总数：任何给定的BTnum值是其中之一。（将“乘”想作“且”，“加”想作“或”。）
15.2.4.2 自定义类型
想一想，数据结构的定义会产生哪些影响？首先，它引入了新的类型；其次它基于此类型定义若干构造器、谓词和选择器。例如，在上面的例子中，首先引入 BTnum，然后使用它创建以下类型：
BTmt : -> BTnum
BTnd : number * BTnum * BTnum -> BTnum
BTmt? : BTnum -> boolean
BTnd? : BTnum -> boolean
BTnd-n : BTnum -> number
BTnd-l : BTnum -> BTnum
BTnd-r : BTnum -> BTnum
观察几个显著的事实：
- 这里的构造器创建
BTnum的实例，而不是更具体的东西。稍后我们将讨论这个设计抉择。 - 这里的谓词函数都接受
BTnum类型参数，而不是“Any”（任意值）。这是因为类型系统已经可以告诉我们某个值的类型是什么，因此我们只需要区分该类型的不同形式。 - 选择器只能作用于类型中相关形式的实例——例如，
BTnd-n只对BTnd的实例有效，对BTmt的实例则不行——但是由于缺乏合适的静态类型，我们无法在静态类型系统中表示这点。
递归类型中还有很多值得讨论的东西，我们不久将回到这个话题。
15.2.4.3 模式匹配和去语法糖
类型定义的讨论告一段落，剩下要提供的功能就是模式匹配。例如，我们可以这样写：
(type-case BTnum t
[BTnum () e1]
[BTnd (nv lt rt) e2])
我们知道，这可以用前述的函数来实现。用 let 就可以模拟此模式匹配所实现的绑定：
(cond
[(BTmt? t) e1]
[(BTnd? t) (let ([nv (BTnd-n t)]
[lt (BTnd-l t)]
[rt (BTnd-r t)]
e2)])
总之，它可以通过宏实现，所以模式匹配不需要被添加到核心语言中，直接用去语法糖即可实现。这也意味着一门语言可以有很多不同的模式匹配机制。
不过，这不完全正确。生成上面代码中的cond表达式时，宏需要通过某种手段知道BTnd的三个位置选择器分别是BTnd-n、BTnd-l和BTnd-r。这些信息在类型定义时显式给出，但是在模式匹配时是隐含的（划重点）。因此，这些信息必须要从类型定义处传过来。因此宏展开器需要使用类似类型环境的东西完成其任务。
此外，还要注意，例如e1和e2这样的表达式无法类型检查——事实上，甚至不能被可靠地识别为表达式——直到完成了type-case的宏展开之后。因此，展开依赖于类型环境，而类型检查依赖于展开的结果。换句话说这两者是共生关系，不仅仅是并行运行，而是同步运行。因此，静态类型语言中进行去语法糖操作时，如果语法糖需要对相关类型作出推测，要比动态类型语言中更复杂一些。
15.2.5 类型、时间和空间
明显，类型已经赋予了类型安全语言一些性能优势。因为一些本来需要运行时执行的检查（例如，检查加法的两个参数的确是数）现在是静态执行的。在静态类型语言中，类似:number的注解已经回答了关于某个值是否是特定类型这种问题；无需在运行时再去检查。因此，类型级别的谓词以及程序中对它们的使用将会（并且需要）完全消失。
对于开发者来说这需要付出一些代价，他们必须说服静态类型系统他们的程序不会导致类型错误；由于可判定性的限制，有些可以正确运行的程序也可能与类型系统冲突。不过，类型系统为满足了它要求的程序提供了可观的运行时性能优势。
接下来我们来讨论空间。到目前为止，语言的运行时系统需要对每个值附加存储其类型信息。这也是其实现类型级别谓词如 number? 的基础，这些谓词既可被开发人员使用也可被语言内部使用。如果不需要这些谓词，那么这些为了实现它们而存储的信息所占据的空间也将不再需要。因此（静态语言）不需要类型标签。
然而，垃圾回收器仍然需要它们，但其他表示法（如BIBOP(译注BIg Bag Of Pages)）能极大减少它们对空间的需求。
类型变体相关的谓词仍要保留：如上面例子中的BTmt?和BTnd?。它们的调用需要在运行时求值。例如，如前所述，选择器BTnd-n就需要执行这种检查。当然，进一步的优化是可能的。考虑模式匹配去语法糖后生成的代码：其中的三个选择器就无需执行这些检查，因为只有BTnd?返回真值时才会执行对应代码片。因此，运行时系统可以给去语法糖层面提供特殊的不安全（unsafe）指令，也就是不执行类型检查的版本，从而生成如下所示的代码：
(cond
[(BTmt? t) e1]
[(BTnd? t) (let ([nv (BTnd-n/no-check t)]
[lt (BTnd-l/no-check t)]
[rt (BTnd-r/no-check t)])
e2)])
但最终的结果是，运行时系统仍然需要存储足够的信息来准确回答这些问题。不过，相比于之前需要使用足够的位来区分每种类型及类型变体，现在，由于类型被静态地隔离了，对于没有变体的类型（例如，只有一种类型的字符串），不再需要存储任何变体相关的信息；这意味着运行时系统可以使用所有可用位来存储实际的动态值。
与之相对，如果类型存在变体，运行时系统需要牺牲一些空间用于区分不同变体，不过一个类型中变体的数量显然比所有类型和其变体的数量要小得多。在上面的例子中，BTnum只有两个变体，因此运行时系统只需要使用一个比特来记录某个值是BTnum的哪个变体。
特别要注意的是，类型体系的隔离可以防止混淆。如果有两种不同的数据类型，每种都有两种变体，在动态类型的世界中，所有这四种变体都需要有不同的表示法；与之相对，在静态类型的世界中，这些表示法可以跨类型重叠，因为静态类型系统会保证一种类型中的变体和另一种类型中的不被混淆。因此，类型系统对于程序的空间（节约表示所需空间）和时间（消除运行时检查）上都有实打实的性能提升。
15.2.6 类型和赋值
我们已经覆盖了核心语言中除赋值之外的大部分基本特性。从某些方面看，类型和赋值之间的相互作用很简单，这是因为在经典环境中，它们根本不相互作用。例如，考虑下面动态类型程序：
(let ([x 10])
(begin
(set! x 5)
(set! x "某物")))
x的“类型”是什么？它并没有确定的类型，它在一段时间内是数，后来（注意里面蕴含时间意味）是字符串。我们根本无法给它定类型。一般来说，类型检查是种非时间性的活动：它只在程序运行之前执行一次，因此必须独立于程序执行的特定顺序。因此，跟踪贮存中的精确值超出了类型检查程序的能力范围。
上面的例子当然可以简单的静态的被理解，不过我们不能被简单的例子误导。考虑下面的程序：
(let ([x 10])
(if (even? (read-number "输入数字"))
(set! x 5)
(set! x "某物")))
现在，静态检查不可能得到关于x的类型的结论，因为只有在运行时我们才能获得用户输入的值。
为了避免这种情况，传统的类型检查器采用了一个简单策略：赋值过程中类型必须保持不变。也就是说，赋值操作，不论是变量赋值还是结构体赋值，都不能改变被赋值的量的类型。因此，上面的代码在我们当前的语言中将不能通过类型检查。给程序员提供多少灵活性就取决与语言了。例如，如果我们引入更加灵活的类型表示“数或字符串”，上面的例子将能通过类型检查，但是x的类型就永远不那么精确，所有使用x的地方都需要处理这种降低了的精度，后面我们会回到这个问题。
简而言之，在传统的类型系统中赋值相对容易处理，因为它采用了简单的规则，值可以在类型系统指定的限度下进行改变，但是类型不能被改变。在像set!这种操作的情况下（或者我们的核心语言中的setC），这意味着赋值的类型必须和变量的类型匹配。在结构体赋值的情况下，例如box，这意味着赋值的类型必须和box容器内容的类型匹配。
15.2.7 中心定理：类型的可靠性
之前我们说过，一些静态类型语言可以为其书写的程序所能达成某些特性作出很坚实的证明：例如，该语言书写的程序肯定会终止。当然，一般来说，我们无法获得这样的保证（事实上，正是为了能写出无限循环我们才添加的通用递归）。然而，一个有意义的类型系统——事实上，任何值得类型系统这一高贵头衔的东西【注释】——应该为所有静态类型程序提供某种有意义的保证。这是给程序员的回报：通过给程序加上类型，她可以确保某些不好的事情不会发生。没有类型的话，我们也能找到bug；这是有用的，但它不足以提供构建高级别工具（例如要保证安全性、隐私性或健壮性）的必要基础。
我们一再使用“类型系统”这个术语。类型系统通常是三个组件的组合：类型的语言、类型规则，以及将这些规则应用于程序的算法。我们的讨论中将类型规则放入函数中，因此模糊了第二者和第三者之间的区别，但它们仍然可以在逻辑上加以区分。
我们可能希望类型系统给我们提供什么样的保证呢？请记住，类型检查器在程序运行前静态地对程序进行检查。这意味着它本质上是对程序行为的预测：例如，当它指出某个复杂表达式的类型为num，它实际是在预测程序运行时，该表达式将产生一个数值。我们怎么知道这个预测是正确的呢，也就是说检查器从不撒谎？每种类型系统都应该附带一个证明这一点的定理。
对于类型系统存疑有一个很好的理由，不是怀疑主义的那种。类型检查器和程序求值器工作方式上有很多不同：
- 类型检查器能见到的只有程序文本，求值器运行在真实的存储器上。
- 类型环境将标识符绑定到类型，求值器的环境则绑定标识符到值或者存储位置。
- 类型检查器将值的集合（甚至是无限集合）压缩成类型，而求值器处理的是值本身。
- 类型检查器一定会终止，求值器不一定会。
- 类型检查器仅需检查表达式一遍，求值器运行时某个表达式的运行次数可能从零次到无穷次。
因此，我们不应假设这两者将始终对应！
对于给定的类型系统，我们希望达到的核心目标是——该类型系统是可靠的（sound）。它的意思是：给定表达式（或者程序）e，类型检查得出其类型为t，当我们运行e时，假设得到了值v，那么v的类型是t。
证明这个定理的标准方法是分两步进行，进展（progress）和保持（preservation）。进展的意思是，如果一个表达式能够通过类型检查，那么它应该能进行进一步求值得到新的东西（除非它本身就是值）；保持的意思是，这个求值步骤前后类型不变。如果我们交错进行这些步骤（先进展再保持，不断重复），可以得出一个结论，最终的结果和最初被求值的表达式类型相同，因此类型系统确实是可靠的。
例如，考虑表达式：(+ 5 (* 2 3))。它的类型为num。在一个可靠的类型系统中，进展证明，由于该表达式能通过类型检查，且其当前不是值，它可以进行一步求值——这里它显然可以。进行一步求值之后，它被规约成了(+ 5 6)。不出所料，正如保持给出的证明，它的类型也为num。进展表明它还能进行一步求值，得到11。保持再次表明它的类型和上一步的表达式类型相同，都为num。现在，进展发现我们已经得到最终结果，无后续要进行的求值步骤，该值的类型和最初的表达式类型相同。
但这不是完整的故事。有两点需要说明：
- 程序可能不会得出最终的结果，它可能永远循环。这种情况下，该定理严格来说并不适用。但是我们仍能看到，计算得到的中间表达式类型将一直保持不变，因此即使程序没有最终产生一个值，它仍在进行着有意义的计算。
- 任何特性足够丰富的语言中都存在一些不能静态决定的属性（有些属性也许本来可以，但是语言的设计者决定将其推迟到运行时决定）。当这类属性出错时——比如，数组的索引越界——关于这种程序没有很好的类型可以约束它们。因此，每个类型完备性定理中都隐含了一组已发布的、允许的异常或者可能发生的错误条件。使用该类型系统的开发者隐式的接受了这些条件。
作为第二点的一个例子，典型的静态类型语言中，都会指明对于向量的寻址、链表的索引等操作可能抛出异常。
后面这个说明好像站不住脚。事实上，我们很容易忘记这其实是一条关于运行时不能发生的事情的陈述：这一组异常之外的异常将能被证明不会产生。当然，对最开始就设计为静态类型的语言，除了不那么严格的类比外，可能搞不清这组异常具体是什么，因为一开始本就无须定义它们。但是当我们将类型系统添加到已有的语言时——特别是动态类型语言，如Racket或Python——那么这里已经有一组明确定义的异常，类型检查器将会指明其中一些异常（像“函数调用位置不是函数”或者“未找到方法”）不会发生。这就是程序员接纳类型系统语法上限制所得到的回报。
15.3 对核心的扩展
现在我们已经有了基础的静态类型语言，下面探索一下如何将其扩展成为更有用的编程语言。
15.3.1 显式的参数多态
下面哪些是相同的？
List<String>List<String>(listof string)
事实上，上面任何两个都不太一样。但是第一个和第三个非常相似，因为第一个是Java代码而第三个是我们的静态语言代码，而第二个，是C++代码，和其它两个不同。清楚了吗？不清楚？很好，继续往下读！
15.3.1.1 参数化类型
我们所使用的编程语言已经展示了参数多态的价值，例如，map函数的类型可以这样给出：
(('a -> 'b) (listof 'a) -> (listof 'b))
意思是，对于任意类型'a和'b，map读入一个从'a到'b的函数，一个'a的链表，生成对应的'b的链表。这里，'a和'b不是具体的类型；它们是类型变量（我们的术语中，这应该被称为“类型标识符”，因为它们在实例化过程中不会变化；但是我们还是使用传统术语）。
可以换种方式理解它：实际上有一族无穷多的这样的map函数。例如，其中一个map的类型是这样的：
((number -> string) (listof number) -> (listof string))
另一个的类型是这样的（没有限制说其中的类型必须是基本类型）：
((number -> (number -> number)) (listof number) -> (listof (number -> number)))
还有这样的（也没有限制说'a和'b必须不同）：
((string -> string) (listof string) -> (listof string))
以此类推。由于它们的类型不同，名字也需要不同：map_num_str、map_num_num->num、map_str_str等。但是这会让它们变成不同的函数，于是我们总得使用某个特定map，而不是直接使用比较一般的那个。
显然，不可能将所有这些函数放到我们的标准库中：毕竟它们有无穷多个！更好的方式是能按需获取我们需要的函数。我们的命名规则给出了一点提示：map接受两个参数，它们都是类型。给定了两个类型作为参数，我们可以得到针对特定类型的map函数。这种类型的参数化被称为参数多态。
注意不要和对象“多态”搞混，后面会讨论它。
15.3.1.2 显式声明类型参数
换句话说，我们相当于说map实际上是有四个参数的函数，其中两个是类型，另外两个是实际的值（函数和链表）。在需要显式声明类型的语言中，我们需要写成类似这样：
(define (map [a : ???] [b : ???] [f : (a -> b)] [l : (listof a)]) : (listof b)
...)
但是这会产生一些问题。首先，???处应该填什么？它是a和b的类型。但是如果a和b本身将被类型替换，那么类型的类型是什么？其次，我们真的希望每次调用map的时候传入四个参数吗？再者，我们真的希望在接收任何实际值之前先接收类型参数吗？对于这些问题的答案能延伸出关于多态类型系统巨大的讨论空间，其中的大部分我们这里将不会涉及。
推荐阅读Pierce的《Types and Programming Languages(类型和编程语言)》，获取易懂、现代的介绍。
注意到一旦我们引入参数化，很多预期之外的代码都将被参数化。例如，考虑平平无奇的cons函数的类型。它的类型需要基于链表中值的类型进行参数化（尽管它实际上并不依赖于这些值——稍后会解释这一点），于是每次使用cons时都需要正确地进行类型实例化。说到这，即使用empty创建空链表也必须类型实例化！当然，Java和C++程序员应该对这个痛点很熟悉了。
15.3.1.3 一阶多态
我们将只讨论这个空间中一个特别有用且易于理解的点上，也即 Standard ML 的类型系统、同时是本书使用的静态类型语言和早期版本的 Haskell 的类型系统，有范型加成的 Java 和 C# 以及引入了模版的C++ 也差不多获得了这种类型系统的大部分能力。这类语言定义了被称为谓词、一阶或者叫前缀多态的东西。关于上小节的问题它的答案是不填、没有、是。下面我们来探讨一下。
我们首先将类型的世界分成两组。第一组包含我们目前用到的静态类型语言，另外加上类型变量；它们被称为 monotype（单型）。第二组包含参数化的类型，被称为 polytype（多型）；按惯例它们是这样写的：∀前缀，一组类型变量，再跟一个类型表达式，表达式中可以使用这些类型变量。因此，map的类型将写作：
∀ a, b : (('a -> 'b) (listof 'a) -> (listof 'b))
由于“∀”是逻辑符号“对于所有的”的意思，于是上面的东西可以读作：“对于所有类型'a和'b，map的类型为……”。
在一阶多态（rank-1 polymorphism）中，类型变量只能被monotype替换。（此外，它们只能被具体类型替换，否则剩下的类型变量将无法被替换掉。）因此，在类型变量参数和常规参数之间我们有了明确的界线。我们不需要为类型变量提供“类型注解”，因为我们知道它们可以是什么。这样得到的语言相对简洁，但仍提供了相当的表达能力。
非直谓性语言（Impredicative language）取消了
monotype和polytype的区别，因此类型变量可以使用另一个多态类型实例化。
注意到由于类型变量只能被monotype替换，他们全相互对立。于是，类型参数可以全被提到参数表的前面。这使我们可以使用形如∀ tv, ... : t的类型，其中tv是类型变量，t是monotype（其中可以引用这些类型变量）。此语法的意义就在这里，这也是之前称其为前缀多态的原因。而且后面也将看到这对其实现也很有用。
15.3.1.4 通过去语法糖实现一阶多态解释器
该特性最简单的实现就是将其视为一种去语法糖的形式：C++ 实际上就是这么做的。（具体来说，因为 C++ 有一个叫做模版的宏系统，所以使用模版，它非常巧合地达成了一阶多态。）举个例子，如果我们有一个语法形式define-poly，它接收名字、类型变量和表达式。当传入类型的时候，它将表达式中对应类型变量替换为此类型，因此：
(define-poly (id t) (lambda ([x : t]) : t x))
通过将id定义为多态的方式定义了一个恒等（identity）函数：给t传入递任意具体类型，就得到一个单参数的类型为(t -> t)的函数（其中t被替换）。我们可以使用各种类型实例化id：
(define id_num (id number))
(define id_str (id string))
从而获得针对这些类型的恒等函数：
(test (id_num 5) 5)
(test (id_str "x") "x")
与之相对，像
(id_num "x")
(id_str 5)
这样的表达式将不能通过类型检查（而不是运行时出错）。
如果你好奇的话，下面给出了实现。简单起见，我们假设只有一个类型参数；很容易使用...实现多个参数的情形。我们不仅将define-poly定义为宏，它还会定义宏：
(define-syntax define-poly
(syntax-rules ()
[(_ (name tyvar) body)
(define-syntax (name stx)
(syntax-case stx ()
[(_ type)
(with-syntax ([tyvar #'type])
#'body)]))]))
因此，对于：
(define-poly (id t) (lambda ([x : t]) : t x))
该语言将创建名为id的宏：对应(define-syntax (name ...) ...)的部分（对于这个例子，name是id）。id的一个实例，如(id number)，将类型变量t、宏里面的typvar替换成给定的类型。因为要规避卫生，我们用with-syntax来确保所有对于类型变量（typvar）的使用被替换为给定的类型。因此，实际效果是，
(define id_num (id number))
被转换成了
(define id_num (lambda ([x : number]) : number x))
然而这种方式有两个重大局限性：
来试试定义递归的多态函数，比如说
filter。之前我们说过，每个多态值（例如cons和empty）都需要类型实例化，但是为了简洁起见我们将依赖静态类型语言实现这点，而仅专注于filter的类型参数。对应代码是：(define-poly (filter t) (lambda ([f : (t -> boolean)] [l : (listof t)]) : (listof t) (cond [(empty? l) empty] [(cons? l) (if (f (first l)) (cons (first l) ((filter t) f (rest l))) ((filter t) f (rest l)))])))注意到递归的使用
filter时，必须使用恰当的类型对其实例化。上面的定义完全正确，只有一个问题，当我们尝试使用它时——如：
(define filter_num (filter number))DrRacket 将不会终止，更准确的说，是宏展开不会终止，因为它将不断的尝试创建
filter代码的副本。不过如果用下面这种方式定义该函数，展开会终止——(define-poly (filter2 t) (letrec ([fltr (lambda ([f : (t -> boolean)] [l : (listof t)]) : (listof t) (cond [(empty? l) empty] [(cons? l) (if (f (first l)) (cons (first l) (fltr f (rest l))) (fltr f (rest l)))]))]) fltr))但是这给开发人员徒增了不必要的痛苦。实际上，一些模版展开程序会缓存之前展开的值，避免对于相同的参数反复生成代码。（Racket 做不到这点，因为一般来说，宏表达式可以依赖可变变量和值，甚至可以执行输入输出，因此 Racket 无法保证同样的输入表达式总是产生相同输出。）
考虑恒等函数的两个实例。我们无法比较
id_num和id_str，因为它们类型不同，但即使它们类型相同，使用eq?比较它们也不同：(test (eq? (id number) (id number)) #f)这是因为对
id每次实例化都会创建一份新的代码副本。即使使用了上面提到的优化，同一种类型对应代码只有一份副本，但是不同类型的对应代码体还是会被重新生成【注释】——但这也是没必要的！例如，id的实现的部分其实没任何东西依赖于参数的类型。实际上，id这一族无穷多个的函数可以共享同一个实现。简单的去语法糖策略实现不了这点。事实上，
C++模版因代码膨胀的问题而臭名昭著，这是原因之一。
换种说法，基于去语法糖的策略本质上是使用替换的实现方式，它有着和我们之前函数调用时使用替换的方式实现相同的问题。不过，其它情况下，替换策略能达成我们关于程序行为的期望；对于多态也是一样，正如我们将看到的一样。
注意去语法糖策略的一个好处就是它不需要类型检查器“理解”多态。我们的核心语言仍可以是单态的（monomorphic），所有的（一阶）多态完全由宏展开处理。这提供了一种廉价的将多态添加到语言中的策略，但正如C++所示，它也引入了很大的开销。
最后，虽然这里我们只关注了函数，但前面的讨论同样适用于数据结构。
15.3.1.5 其它实现方式
有些其他实现策略不会遇到此类问题。这里我们不会深入讲解它们，但是其中一些策略的本质就是上面提到过的“缓存”方法。因为可以确定的是，对于给定的同一组类型参数，应该得到相同的实现代码，不需要对相同的类型参数实例化多次。这避免了无限循环。如果我们检查了使用特定类型实例化的代码一次，后续相同类型参数的实例化结果就无需再进行类型检查（因为它不会发生改变）。此外，我们无需保留实例化后的源码：一旦我们检查了展开后的程序，就可以将其丢弃，运行时也只需要保留一份实例化的副本。这样可以避免上述纯去语法糖策略中讨论过的所有问题，同时保留它的好处。
其实我们有点过分了。静态类型的好处之一就是能选择更精确的运行时表示。例如，静态类型可以告诉我们用的是数是32位的还是64位的甚至1位的（也就是布尔值）。然后编译器可以利用位的布局方式（例如，32个布尔值可以*打包进一个32位字）为每种表示生成专用代码。因此，在对每种使用的类型进行检查之后，多态实例化程序可以跟踪函数或数据结构使用时用到的特定类型，并将这些信息提供给编译器用于代码生成。这会导致生成相关函数的若干副本，彼此都互不eq?——但这么做有充分的理由，因为它们要执行的操作的确不同，所以这是正确的。
15.3.1.6 关系型参数
我们还需解决关于多态的最后一个细节。
早先我们说过像cons这样的函数不依赖于其参数的具体值。这一点对map、filter等也成立。map和filter接收一个函数作为参数，当它们要对单个元素进行操作时，实际上使用该函数进行操作，即该函数负责做出如何处理元素的决定；map和filter本身只是遵从该函数参数。
“检验”这种情况是否属实的一种方法是，替换不同类型的值链表及对应的函数作为参数。也就是说假设两组值之间有映射关系；我们根据此关系替换链表元素和参数函数。问题是，map和filter的输出结果是否可以通过该关系预测？如果对于某些输入，map的输出和关系预测的结果不同，这说明map肯定侦测了实际值并根据相关信息做出了处理。但事实上，这不会发生在map上，或者说实际上也不会发生在大多标准多态函数上。
遵从这类型关系准则的函数被称为关系型参数（Relational Parametricity）【注释】。这是类型赋予我们的另一个非常强大的能力，因为它们告诉我们这种多态函数可以执行的操作很受限制：它们可以删除、复制或重新排列元素，但是不能考察这些元素，也不能对它们进行具体操纵。
请参阅Wadler的《Theorems for Free!》和Reynolds的《Types, Abstraction and Parametric Polymorphism》。
起初这听起来非常令人印象深刻（确实如此！），但细查，你可能会意识到这与经验并不一致。例如，在Java中，多态方法依然可以使用instanceof在运行时检查、获得特定类型的值，并相应的改变行为。这种方法就不是关系型参数了！【注释】事实上，关系型参数也能被看作是语言弱点的一种表述：它只允许一组有限的操作。（你仍可以检查类型——但不能根据你获取的信息进行相关行动，这样检查就没有意义了。因此运行时系统如果想要模拟关系型参数，必须要移除类似instanceof及它的替代行为：例如，对值进行加一操作并捕获异常以判断它是数。）然而，这是个非常优雅和令人吃惊的结果，显示了使用丰富类型系统能获得的强大程序推理能力。
网上，你会经常发现这个属性被描述为函数不能检查其参数——这是不正确的。
15.3.2 类型推断
手工书写每处多态类型的实例参数是一个令人沮丧的过程，很多版本的Java和C++用户可以证明这点。想象一下，每次使用first和rest时都需要传入类型参数是个什么场景！我们之所以能够避免这种命运，是因为我们的语言实现了类型推断。这使我们可以编写定义：
(define (mapper f l)
(cond
[(empty? l) empty]
[(cons? l) (cons (f (first l)) (mapper f (rest l)))]))
然后编程环境自动声明
> mapper
- (('a -> 'b) (listof 'a) -> (listof 'b))
它不仅是正确的类型，而且是非常一般的类型！从程序结构中派生出这种一般类型的过程感觉几乎就是魔法。我们来揭示其幕后。
首先，我们来了解类型推断做了什么。有些人错误的认为，有类型推断的语言无类型声明，其被类型推断取而代之了。这混淆了多个层面的东西。首先，即使在有类型推断的语言中，程序员仍被允许声明类型（并且为了文档更为清晰，通常会鼓励这样做——就像你之前被鼓励的一样）【注释】。此外，在没有这些声明的情况下，推断的实际含义并不显明。
有时（类型）推断是不可判定的，这时程序员别无选择只能声明某些类型。最后，显式的书写类型注解能够大大减少难以辨认的错误信息。
相反，最好将底层语言看作需要完整地显式声明类型的——就如我们刚才研究的多态语言。然后我们说，在:后类型注解部分可以留空，编程环境中的某个特性会为我们填充这些。（如果走得更远，我们可以丢弃:及额外的修饰，它们都会被自动插入。因此，类型推断只是为用户提供的一种便利，减轻编写类型注解的负担，而底层的语言仍然是显式声明类型的。
我们怎么考虑类型推断做的是什么呢？假设我们有个表达式（或者程序）e，由显式声明类型语言书写：也就是说在任何需要类型注解的地方都有写出。现在假设我们擦除e中所有的类型注解，然后使用函数infer将它们推断回来。
思考题
infer应该有何种属性？
我们可以要求很多东西。其中之一为，它要产生和e原来恰好一样的注解。这在很多方面都是有问题的，尤其是当e本就不能通过类型检查的情况下，怎么能推断回它们（应该）是什么？你可能觉得这是个学究式的玩笑：毕竟，如果e本就不能通过类型检查，如果能在删除其注解之后还能还原回来呢？反正两者都不能通过类型检查，谁在乎啊？
思考题
这个推理正确吗？
假设e是：
(lambda ([x : number]) : string x)
它显然不能通过类型检查。但是如果我们擦除类型注解——得到
(lambda (x) x)
——这个函数显然可以合法地添加类型！因此，更合理的需求可以是，如果原始的e能通过类型检查，那么对应的使用了推导出的注解的版本也必须能。这种单向的含义的用途体现在两方面：
- 它没有说
e未通过类型检查应该怎样，也即它不会排除前述的类型推断算法，其会将例子中类型错误的恒等函数变成类型正确的。 - 更重要的是，它向我们保证，使用类型推断将不会使我们失去任何东西：之前能通过类型检测的程序不会被推断后而不能。这意味着我们可以在想要的地方显式添加类型注解，但不会被迫这样做。
当然，这只在程序推断可判定的情况下才成立。
我们还可能希望两者类型是相同的，但这不是能做到的：函数
(lambda ([x : number]) : number x)
类型为(number -> number)，而擦除类型注解后推导出的类型要一般得多。因此，将这些类型关联并给出类型相等的定义并不简单，尽管如此后面将简要讨论此问题。
有了这些准备，我们下面进入对类型推断机制的研究。最需要注意的地方，前述的简单递归下降的类型检查算法将不再起作用。它之前能起作用，是因为所有函数的边界处都有类型注解，所以我们下降进入函数体，同时用类型环境携带这些注解中包含的信息。没了这些注解，就不知如何递归下降了。
事实上，目前还不清楚哪个方向更合理。像上面mapper的定义，各代码段之间互相影响。例如，从empty?、cons?、first和rest对l的调用都可以看出它是链表。但是是什么的链表呢？从这些操作看不出来。然而，对于其每个（或者应该说，任意）first元素调用了f这点可以看出，链表成员的类型必须可以被传给f。同理，由empty和cons我们可以知道（mapper的）返回表达式必须为链表。它的成员类型是什么呢？必须为f的返回类型。最后，请注意最微妙的地方：当参数链表为空时，我们返回empty而不是l（这时我们是知道其被绑定到empty）。使用前者，返回值的类型可能是任意类型的链表（仅受f返回类型的约束）；使用后者，返回的类型就被迫和参数链表的类型相同。
所有这些信息都包含在函数里。但是我们如何系统地提取出这些信息呢，而且使用的算法必须会终止，并满足前面陈述属性？我们分两步来做。首先，根据程序表达式生成其必须要满足的类型约束。然后，通过合并散布在函数体各处的约束、识别其中的不一致，最终解决约束。每一步都相对简单，但是组合起来创造了魔力。
15.3.2.1 约束生成
我们最终的目标是给每个类型注解位置填入类型。将会证明，这也等同于找到每个表达式的类型。简单想想就知道，这本来也是必要的：比如，在不知道函数体类型的情况下，如何能确定函数本身的类型？这也是足够的，因为如果每个表达式的类型都被计算得出，其中必然包括了那些需要被注解的表达式。
首先，我们需要生成（待解决的）约束。这一步会遍历程序源码，为每个表达式生成恰当的约束，最后返回这组约束。为了简单，使用递归下降的方式实现；它最终生成约束的集合，所以原则上遍历和生成的顺序是无关紧要的——因此我们选择了相对简单的递归下降方式——当然，为了简单起见，我们使用链表表示这个集合。
约束是什么呢？就是关于表达式类型的陈述。此外，虽然变量绑定并不是表达式，但我们仍需计算其类型（因为函数需要参数和返回值类型）。一般来说，对于表达式的类型我们知道些什么呢？
- 它和某些标识符的类型有关。
- 它和某些其它表达式的类型有关。
- 它是数。
- 它是函数，其定义域（domain）和值域（range）类型可能受到进一步的约束。
因此，我们定义如下两个数据结构：
(define-type Constraints
[eqCon (lhs : Term) (rhs : Term)])
(define-type Term
[tExp (e : ExprC)]
[tVar (s : symbol)]
[tNum]
[tArrow (dom : Term) (rng : Term)])
接下来定义约束生成函数：
<constr-gen> ::= ;约束生成
(define (cg [e : ExprC]) : (listof Constraints)
(type-case ExprC e
<constr-gen-numC-case>
<constr-gen-idC-case>
<constr-gen-plusC/multC-case>
<constr-gen-appC-case>
<constr-gen-lamC-case>))
当表达式为数时，唯一能说的是，我们希望该表达式的类型为数类型：
<constr-gen-numC-case> ::=
[numC (_) (list (eqCon (tExp e) (tNum)))]
听上去很微不足道，但我们不知道的是，其他包含它的表达式是什么。因此，某个更大的表达式可能会与此断言——这个表达式的类型必须是数型——相矛盾，从而导致类型错误。
对于标识符，我们只是简单地说，表达式的类型就是我们所期望该标识符应有的类型：
<constr-gen-idC-case> ::=
[idC (s) (list (eqCon (tExp e) (tVar s)))]
如果上下文限制了其类型，该表达式的类型将自动受到限制，并且必须与上下文的期望一致。
加法是我们第一个遇到的上下文约束。对于加法表达式，首先需要确保我们生成（并返回）其两个子表达式的约束，而子表达式可以是复杂的。这两个约束中，我们期望什么？需要每个子表达式是数类型的。（如果其中一个子表达式不是数类型的，应该导致类型错误。）最后，我们断言整个表达式的类型为数。
<constr-gen-plusC/multC-case> ::=
[plusC (l r) (append3 (cg l)
(cg r)
(list (eqCon (tExp l) (tNum))
(eqCon (tExp r) (tNum))
(eqCon (tExp e) (tNum))))]
append3是append的三参数版本。
multC的情况与之相同，区别只在名字上。
下面我们来看另外两个有趣的情况，函数声明和调用。两种情况下我们都需要生成和返回子表达式的约束。
在函数定义中，函数的类型是函数（“箭头/arrow”）类型，其参数类型是形参的类型，其返回类型是函数体的类型。
<constr-gen-lamC-case> ::=
[lamC (a b) (append (cg b)
(list (eqCon (tExp e) (tArrow (tVar a) (tExp b)))))]
最终，考虑函数调用。我们不能直接陈述函数调用的类型约束。不过，我们可以说，函数接受的参数类型必须和实际参数的类型相同，并且函数返回的类型就是调用表达式的类型。
<constr-gen-appC-case> ::=
[appC (f a) (append3 (cg f)
(cg a)
(list (eqCon (tExp f) (tArrow (tExp a) (tExp e)))))]
完成了！我们已经完成约束的生成；现在只需解出它们。
15.3.2.2 使用合一求解约束
求解约束的过程也被称为合一（unification）。合一器的输入是等式的集合，其中每个等式是变量到项（term）的映射，项的数据类型在上面定义了。注意到一点，我们实际上有两种变量。tvar和tExp都是“变量”，前者很明显，注意后者同样也是，因为我们需要求解此类表达式的类型。（另一种方式是为每个表达式引入新的类型变量，但我们仍需一种方法确定这些变量与表达式之间的对应关系，而现在这已经能通过对表达式进行eq?操作自动完成了。另外这会产生大得多的约束集，不好进行人工检查。）
就我们的目的而言，合一是为了是生成替换（substitution），或者说将变量映射为不包含任何变量的项。这听起来应该很耳熟：我们有一组联立方程，其中每个变量都是线性使用的；这种方程组可以使用高斯消元法求解。该情形中，我们清楚最终可能遇到缺少约束（under-constrained）或过度约束（over-constrained）的情况。这种事情同样也将发生这里。
合一算法会遍历约束集合。由于每个约束有两项，每个项有四种可能的类型，因此有十六种情况需要考虑。幸运的是，我们实际可以用比较少的代码覆盖这十六种情况。
算法从所有约束的集合和空替换开始。每个约束都会被处理一次，并从集合中删除，因此原则上终止判据应该非常简单，但是实际处理起来还有点小麻烦。随着约束被处理，替换集合会逐渐增长。当所有的约束都被处理完后，合一过程返回最后的替换集合。
对于给定的约束，合一器检查等式左边，如果它是变量，那么这时它就可以被消除了，合一器将该变量（等式）的右侧添加到替换中，为了真正完成消除，还需要将替换集中所有该变量的出现替换成该右侧。实践中，实现需要考虑效率；例如，使用可变值表示这些变量可以避免搜索—替换过程。然而我们可能需要进行回溯（我们在后面确实会需要），可变值表示也有缺点。
思考题
注意到上面微妙的错误了吗？
这个微妙的错误是，我们说合一器通过替换变量的所有实例来消除它。不过，我们假设等式右侧不包含该变量的实例。不然的话，我们将得到循环定义，这将使替换变得不可能。出于这个原因，合一器会进行出现检查（occurs check）：检查某个变量是否出现在等式两侧，如果是，则拒绝合一。
思考题
构造一个其约束会触发出现检查的项。
还记得ω吗？
下面考虑合一的实现。惯例使用希腊字母Θ表示替换。
(define-type-alias Subst (listof Substitution))
(define-type Substitution
[sub [var : Term] [is : Term]])
(define (unify [cs : (listof Constraints)]) : Subst
(unify/Θ cs empty))
首先把简单的东西写出来：
<unify/Θ> ::=
(define (unify/Θ [cs : (listof Constraints)] [Θ : Subst]) : Subst
(cond
[(empty? cs) Θ]
[(cons? cs)
(let ([l (eqCon-lhs (first cs))]
[r (eqCon-rhs (first cs))])
(type-case Term l
<unify/Θ-tVar-case>
<unify/Θ-tExp-case>
<unify/Θ-tNum-case>
<unify/Θ-tArrow-case>))]))
现在可以实现合一的核心了。我们需要一个辅助函数extend-replace，其签名为(Term Term Subst -> Subst)。它将执行出现检查，如果检查得出没有环路，则扩展替换集合，并将替换集合中所有出现的第一个项（第一个参数）替代为第二个项（第二个参数）。同样，我们假设lookup: (Term subst -> (optionof Term))存在。
练习题
定义
extend-replace和lookup。
如果约束等式的左侧是个变量，我们先在替换集合中寻找它。如果存在，我们将当前约束换成新的约束；否则我们扩展替换集合。
<unify/Θ-tVar-case> ::=
[tVar (s) (type-case (optionof Term) (lookup l Θ)
[some (bound)
(unify/Θ (cons (eqCon bound r)
(rest cs))
Θ)]
[none ()
(unify/Θ (rest cs)
(extend+replace l r Θ))])]
同样的逻辑也适用于表达式的情况：
<unify/Θ-tExp-case> ::=
[tExp (e) (type-case (optionof Term) (lookup l Θ)
[some (bound)
(unify/Θ (cons (eqCon bound r)
(rest cs))
Θ)]
[none ()
(unify/Θ (rest cs)
(extend+replace l r Θ))])]
如果是基本类型，例如数，我们就需要检查等式右边。有四种可能：
- 如果是数，那么该等式声明类型
num等于num，这恒为真。因此我们可以忽略该约束——它没有告诉我们什么有用信息——继续检查剩下的。 当然，首先得解释为什么会出现这种约束。显然，我们的约束生成器不会生成这种约束。然而，前面替换集合的扩展会导致这种情况。事实是实践中我们会遇到好几个这种情况。 - 如果是函数类型，显然存在类型错误，因为数和函数类型不相交。同样，我们不会直接生成这样的约束，一定是由先前的替代产生。
- 它可能是两种变量类型之一。不过，我们的约束生成器经过了仔细的安排，不会将它们放在右侧。此外，替代过程也不会在右侧引入它们。因此，这两种情况不会发生。
于是得出这样的代码：
<unify/Θ-tNum-case> ::=
[tNum () (type-case Term r
[tNum () (unify/Θ (rest cs) Θ)]
[else (error 'unify "number and something else")])]
最后还剩下函数类型。这里的论点几乎和数类型完全一样。
<unify/Θ-tArrow-case> ::=
[tArrow (d r) (type-case Term r
[tArrow (d2 r2)
(unify/Θ (cons (eqCon d d2)
(cons (eqCon r r2)
cs))
Θ)]
[else (error 'unify "arrow and something else")])]
请注意，我们并没有严格地缩小约束集合，因此仅通过约束集合的大小不足以判断这个过程会终止。需要同时综合考虑约束集合的大小以及替换的大小（包括其中变量的个数）。
上面的算法非常通用，不仅对数和函数，对于各种类型项也都适用。我们使用数代表各种基础类型；同样，使用函数代表各种构造类型，例如listof和vectorof。
这就完成了。合一产生了替换。现在我们可以遍历这些替换，找到程序中所有表达式的类型，然后插入对应的类型注解。有定理（这里不证明）指出，上面过程的成功意味着程序通过了类型检查，因此我们无需对该程序显式地再跑一遍类型检查。
不过请注意，类型错误的性质在这里发生了巨大变化。之前，我们的递归下降算法利用类型环境遍历表达式。类型环境中的绑定是程序员定义的类型，因此可以被当作（期望的）权威的类型规范（specification）。因此，所有的错误都应归咎于表达式，类型错误的报告很简单（而且很好懂）。然而这里，类型错误无法通知。合一错误是两个智能算法——约束生成和合一——共同导致的，因此程序员不一定能理解。特别是，由于约束的本质是等式，报告的错误位置和“真实”的错误位置可能相差甚远。因此，生成更好的错误信息仍然是个活跃的研究领域。
实践中，算法会维护涉及到的程序源码的元信息，并可能也会保存合一的历史，以便溯源错误回源程序。
最后，请记住，约束可能不会精确指明所有变量的类型。如果方程组过度约束，可能会有冲突，导致类型错误。如果缺少约束，这意味着我们没有足够的信息对所有表达式做出明确的类型声明。例如，对于表达式(lambda (x) x)，没有足够的约束指明x的类型，从而无法以指明整个表达式的类型。这并非错误；它只是意味着x可以是任意类型。换句话说，该表达式的类型是“x的类型->x的类型”，无其它约束。这些欠约束标识符的类型以类型变量的方式展示，于是上面表达式的类型可以表示为('a -> 'a)。
合一算法实际上有个很好的属性：它能自动计算表达式最通用的类型，也被称为主类型（principal type）。这就是说，表达式可以有的任何实际类型都可以通过（用实际类型）替换推导出的类型中的类型变量的得到。这是个异乎寻常的结果：没人能生成比前述算法得出的更为一般的类型！
15.3.2.3 Let-多态
很不幸，尽管这些类型变量表面上看和我们之前遇到的多态有诸多相似之处，但它们并不同。考虑下面的程序：
(let ([id (lambda (x) x)])
(if (id true)
(id 5)
(id 6)))
如果加上显式的类型注解，它能通过类型检查：
(if ((id boolean) true)
((id number) 5)
((id number) 6))
然而，如果使用类型推断，它将不能通过类型检查！因为id中的类型'a——取决于约束处理的顺序——要么和boolean合一，要么和number合一。对应的，那时id的类型要么是(boolean -> boolean)要么是(number -> number)。当使用另一个类型调用id时，就会发生类型错误！
这是因为我们通过合一推断出来的类型实际并不是多态的。这点很重要：将其称为类型变量不会使你获得多态!类型变量可以在下次使用时合一，彼时，最终得到的还只是单态函数。而真正的多态只有在能真正进行类型变量实例化时才会获得。
所以在具有真正多态的语言中，约束生成和合一是不够的。相反，像ML和Haskell这种语言，甚至我们使用的静态类型语言也是，都实现了俗称let-多态的东西。这种策略中，当包含类型变量的项在词法环境中被绑定时，该类型被自动提升为量化类型。每次使用时，该项被自动实例化。
很多实现策略可以做到这点。最简单（而不令人满意）的方式只需复制绑定标识符代码的代码；这样，上面每次id的使用都会得到自己的(lambda (x) x)副本，所以每个都有它自己的类型变量。第一个的类型可能是('a -> 'a)，第二个是('b -> 'b)，第三个是('c -> 'c)，等等。这些类型变量互不冲突，因此我们得到多态的效果。显然，这不仅增加了程序的大小，而且在存在递归的情况下也不起作用。然而，这给我们提供了通往更好解决方案的思路：不是复制代码，而是复制类型。因此在每次使用时，我们创建推导出类型的重命名版本：第一次使用时，id的类型('a -> 'a)变成了('b -> 'b)，以此类推，这种方式实现了拷贝代码相同的效果且没有它的包袱。不过，因为这些策略实质都是效仿代码拷贝，因此它们只能在词法环境下工作。
15.3.3 联合类型
假设我们要建立动物园动物的链表，动物有这些种类：犰狳、红尾蚺等。目前，我们必须创建新的数据类型：
(define-type Animal
[armadillo (alive? : boolean)] ;犰狳
[boa (length : number)]) ;蚺
“在德州，马路中间除了黄线和死掉的犰狳什么都没有。” —— Jim Hightower
然后创建它的链表：(listof Animal)。因此，Animal类型表示的是armadillo和boa的“联合（或称联合体，union）”，不过要创建这种联合的唯一方式是每次都创建新类型：比如要创建动物和植物的联合，就需要：
(define-type LivingThings
[animal (a : Animal)]
[plant (p : Plant)])
这样实际的动物现在裹在了更深一“层”。这些类型被称为带标签的联合（tagged union）或可辨识的联合（discriminated union），因为我们需要显式引入类似animal和plant的标签（或称辨识符(discriminator)）来区分它们。相应地，结构体只能通过数据类型声明来定义；要创建只包含一种变体的数据结构，如
(define-type Constraints
[eqCon (lhs : Term) (rhs : Term)])
来表示该数据结构，我们需要使用类型Constraints而不是eqCons，因为eqCons不是类型，只是能在运行时区分的类型变体。
无论哪种方式，联合类型的要点是表示析取或“或”。值的类型是联合中某个类型。值通常只能是联合中某个特定的类型，不过这取决于联合类型的精确定义、规范它们的规则等等。
15.3.3.1 作为类型的结构体
对此自然的反应可能是，为什么不移除这种限制？为什么不允许每个结构体独立存在，将类型定义为一些结构体的集合？毕竟，不管是C还是Racket，程序员都可以定义独立的结构体，无需使用标签构造函数将它们包裹在其它类型里！例如，Racket里可以写：
(struct armadillo (alive?))
(struct boa (length))
加个注释：
;; 动物是下面两者之一：
;; - (armadillo <boolean>)
;; - (boa <number>)
但是由于Racket不强制静态类型，这种比较不太清楚。然而，我们可以和 Typed Racket （内置与DrRacket中的静态类型Racket）相比较。下面是对应的静态类型代码：
#lang typed/racket
(struct: armadillo ([alive? : Boolean]))
(struct: boa ([length : Real])) ;; feet
无需引用armadillo就可以定义使用boa类型值的函数：
;; http://en.wikipedia.org/wiki/Boa_constrictor#Size_and_weight
(define: (big-one? [b : boa]) : Boolean
(> (boa-length b) 8))
事实上，如果调用此函数时传入其它类型，如armadillo——(big-one? (armadillo true))——将发生静态错误。因为armadillo和boa之间的关系等同与数和字符串之间的关系。
当然，我们仍可以定义这些类型的联合：
(define-type Animal (U armadillo boa))
在这之上定义函数：
(define: (safe-to-transport? [a : Animal]) : Boolean
(cond
[(boa? a) (not (big-one? a))]
[(armadillo? a) (armadillo-alive? a)]))
之前我们有一种包含两个变体的类型，现在则有三种类型，其中两种类型恰巧能方便的通过联合定义第三种。
15.3.3.2 无标签联合
看起来我们好像还需要辨识标签，但并非如此。在支持联合类型的语言中，通常这样获取类型构造器optionof：将期望的返回类型和用于表示失败或者none的类型结合起来。例如，下面是(optionof number)的等价实现：
(define-type MaybeNumber (U Number Boolean))
同时，Boolean本身也可以是True和False的联合，在Typed Racket中也确实如此。因此，选择（option）类型更为准确的模拟实现应该是：
(define-type MaybeNumber (U Number False))
更为一般的，可以定义：
(struct: none ())
(define-type (Maybeof T) (U T none))
由于由于none是新的、独特的类型，不会和其它类型混淆，因此该定义适用于所有类型。它提供给我们与选择类型相同的好处，且我们的值没有被埋入深一层的some结构体，而是立即可用。例如member，其Typed Racket中的类型是：
(All (a) (a (Listof a) -> (U False (Listof a))))
如果元素未找到，member返回false；否则，它将返回从该元素开始的链表（即，链表的第一个元素是期望的元素）。
> (member 2 (list 1 2 3))
'(2 3)
将其转换为使用Maybeof实现，可以写成：
(define: (t) (in-list? [e : t] [l : (Listof t)]) : (Maybeof (Listof t))
(let ([v [member e l]])
(if v
v
(none))))
如果元素未找到，它将返回值(none)；如果找到了，仍然是返回链表：
> (in-list? 2 (list 1 2 3))
'(2 3)
这样就无需从some容器中取出链表。
15.3.3.3 辨识无标签联合
将值放入联合是一码事；我们还需要考虑如何以类型良好的方式将值从其中取出来。在我们的类ML类型系统中，我们使用程式化的符号——我们的语言中type-case，ML中的模式匹配——来标识和取出各部分。具体来说，对于代码：
(define (safe-to-transport? [a : Animal]) : boolean
(type-case Animal a
[armadillo (a?) a?]
[boa (l) (not (big-one? l))]))
在整个表达式中a的类型保持一致。标识符a?和l分别被绑定到布尔类型和数类型的值上，big-one?接收的就是这些类型，而不是armadillo和boa。换句话说，big-one?函数的输入类型不可以是boa，因为根本没有这样的类型。
反之，使用联合类型的话，我们确实有boa类型。因此，我们遵守对值进行谓词操作将缩小其类型的原则。例如，在cond的子句
[(boa? a) (not (big-one? a))]
中，尽管a的初始类型为Animal，在通过boa?测试后，类型检查器会将其类型缩小到boa的分支，这样big-one?调用得以通过类型检查。反过来，其在条件表达式剩余部分的类型不是 boa——这里，只剩下armadillo一种可能。这给类型检查器提出了更高的要求，它需要能测试并识别特定模式（称为条件分割(if-splitting)）；缺了这种能力就无法使用联合类型编程；当然我们可以只识别类ML系统中能识别的模式，也就是模式匹配、type-case。
15.3.3.4 改造为静态类型
毫不奇怪，Typed Racket使用联合类型。当将现有语言改造为静态类型时，它们尤其有用，因为现有语言（如脚本语言中）的程序没有用类ML类型系统的原则来定义。这种类型改造的通用的原则之一是尽可能多地静态捕获动态异常。当然，检查器最终会让一些程序无法通过检查【注释】，但如果它拒绝太多可以无错运行的程序，开发者不太可能采用它。由于这些程序是在没有考虑类型检查的情况下编写的，因此类型检查器需要以更为激进的方式接受该语言中被认为合理的习惯用法。
除非它实现了称为软类型（soft typing）的有趣想法：不拒绝任何程序，而是提供信息告知程序中无法通过类型检查之处。
考虑下面的JavaScript函数：
var slice = function (arr, start, stop) {
var result = [];
for (var i = 0; i <= stop - start; i++) {
result[i] = arr[start + i];
}
return result;
}
它读入一个数组和两个索引，返回这两个索引之间的子数组。例如，slice([5, 7, 11, 13], 0, 2)求得[5, 7, 11]。
在JavaScript中，开发人员在函数调用时可以自由的省略任意或者所有尾部参数。每个被省略的参数都被赋予特定值undefined，如何处理这种情形完全由函数决定。例如，slice的典型实现允许用户省略最后一个参数；下面的定义
var slice = function (arr, start, stop) {
if (typeof stop == "undefined")
stop = arr.length - 1;
var result = [];
for (var i = 0; i <= stop - start; i++) {
result[i] = arr[start + i];
}
return result;
}
在未给定第三个参数时自动返回到数组结尾的子数组：因此slice([5, 7, 11, 13], 2)返回[11, 13]。
在Typed JavaScript【注释】中，程序员可以通过为给定参数指定类型U Undefined来显式地指明函数可以接受更少的参数，此函数的类型如下：
∀ t : (Array[t] * Int * (Int U Undefined) -> Array[t])
由Arjun Guha等人在布朗（大学）创建。参见我们的网站。
原则上，这意味着表达式stop - start存在发生类型错误的可能，因为stop可能不是数。然而，当用户省略该参数时，对stop的赋值正好将其设为数类型。换句话说，在所有控制路径上，减法发生前stop都将是数类型，因此该函数能通过类型检查。当然，这要求类型检查器能够对控制流（条件）和状态（赋值）进行推断来确保函数类型正确；而Typed JavaScript可以做到，也因此能允许这样的函数。
15.3.3.4 设计选择
拥有联合类型的语言中，通常有
- 独立的结构体类型（通常用类表示），而不是带有变体的数据类型。
- 用于表示特定类型的特殊（ad hoc）结构体集合。
- 哨兵值（sentinel value）表示失败。
将这种风格的程序转换成满足类ML类型风格的非常费事。因此，许多改造过来的类型系统引入联合类型来减轻类型化过程的负担。
上述三个属性中，第一个相对中立，但是其它两个需要更多讨论。我们以反序依次解决它们。
首先处理哨兵值。很多情况下，哨兵应该被替换为异常，但是在很多语言中，抛出异常的代价巨大。因此开发者倾向于区分真正的异常情况——不应该发生——和正常运行中的预期情况。检查元素是否属于链表发现不存在的情况显然属于后者（如果我们已经知道元素是否存在，这个谓词判断就无需进行）。在后一种情况下，使用哨兵是合理的。
然而，我们需要认识到，在C程序中，未能检测异常的哨兵值是错误——甚至安全缺陷——的常见原因。这点很容易解决。在C中，哨兵值和普通返回值类型相同（或者至少等同于类型相同），而且运行时也没有检查。因此哨兵可以被当作合法的值使用，且不会出现类型错误。这就导致哨兵值
0可以被当作分配数据的地址来使用，从而导致系统崩溃。与之不同，我们的哨兵是真正意义上的新类型，无法用于任何计算。观察到前语言中没有任何函数的输入类型为none，可以推理出这点。先忽略这里贬义的“特殊”一词，对一组结构体进行不同的分组是否是个好主意？实际上，就算在遵循类ML规范的程序中，当程序员希望刻画一个大宇宙的子宇宙时，也会出现这种分组的情形。例如，ML程序员会使用下面的类型
(define-type SExp [numSexp (n : number)] [strSexp (s : string)] [listSexp (l : (listof SExp))])表示s-expression。如果有函数希望操作这些项的某个子集，比如数和数的链表，就必须创建新的类型，然后将值在两种类型之间转换，尽管这两个类型的内部表示完全相同。另一个例子，考虑CPS表达式的集合，这显然是所有可能表达式的一个子集，但如果不得不为其创建新的类型，我们将无法对其使用任何已有的表达式处理程序，比如解释器。
换种说法，联合类型似乎是我们之前见到的ML风格类型系统的合理变种。但是，即使在联合类型中仍有设计选择，它们都有其后果。例如，允许类型系统创建新联合类型吗？允许用户定义（和命名）联合吗？也就是说，允许表达式
(if (phase-of-the-moon)
10
true)
通过类型检查吗（将创建类型(U Number Boolean)），还是由于其引入了之前未命名并显式标识的类型而将其判定为类型错误？Typed Racket提供的是前者：它将创建真正的临时联合。对于给现有代码引入类型来说，这么做可能更好，因为它更加灵活。但对于写新代码来说，这是否是个好的设计还并不清楚，因为并非程序员期望内的联合会出现，而且无法避免。这给程序语言的设计空间提供了一个未被探索的角落。
15.3.4 名义类型系统与结构类型系统
我们最初的类型检查器中，如果两个类型具有相同的结构，则认为它们是相同的。事实上我们根本没有提供类型的命名机制，因此不清楚有何替代方案。
现在考虑Typed Racket。程序员可以写
(define-type NB1 (U Number Boolean))
(define-type NB2 (U Number Boolean))
然后写
(define: v : NB1 5)
假设还定义了函数
(define: (f [x : NB2]) : NB2 x)
然后用v调用f，即(f v)：该调用应该通过类型检查吗？
有两种完全合理的解释。一种是说v被声明为类型NB1，与NB2名称不同，因此应该被当作不同类型，所以该调用应导致错误。这种系统被称为名义的（nominal），因为类型的名字对于确定类型是否相等极为重要。
与之对应，另一种解释是说因为NB1和NB2结构相同，因此开发者无法写出在这两种类型的值上表现的不同的程序来，所以它们应该被视为相同。【注释】这种类型系统被称为结构的（structural），将允许上面的程序通过检查。（Typed Racket遵循结构类型的规范，理由同样是减少导入现有动态类型代码的负担，这些Racket代码通常是以结构解释为模型编写的。事实上，Typed Racket中(f v)不仅能通过类型检查，而且打印出的返回类型为NB1，无视f返回值的类型注解！）
如果特别小心，你会注意到被认为相同和实际相同之间是有区别的。这里不会涉及该问题，但请考虑编译器作者选择值的表示时其影响是啥，尤其在允许运行时获取值的静态类型的语言中。
名义和结构类型之间的区别在面向对象语言中是最常见的争议，后面将简要回顾这个问题。然而，这里的重点是要说明这些问题本质上并不关乎“对象”。任何允许命名类型的语言——出于程序员精神健康的需要，也就是所有的语言了——都要应付此问题：命名只是方便起见，还是说所选的名字是被认为是有意义的？选择前者导致结构类型，选择后者导致名义类型。
15.3.5 交叉类型
我们刚探索了联合类型，很自然的就会想到有没有交叉（intersection）类型呢。确实有。
如果联合类型指（该类型的）值属于这个联合中某个类型，交叉类型显然意味着该值属于交叉中的所有类型：合取，或“且”。这可能看起来很奇怪：值怎么可能属于多种类型呢？
用具体例子回答，考虑重载函数。例如，某些语言中+即可操作数，也能操作字符串；传入两个数它返回数，传入两个字符串它返回字符串。这种语言中，+的类型应该是什么呢？不是(number number -> number)，因为那样它将不能用于字符串；同样的原因，也不是(string string -> string)。甚至它也不是
(U (number number -> number)
(string string -> string))
因为+不仅仅是这些函数之一：实际上它（同时）是这两者。我们可以认为其类型是
((number U string) (number U string) -> (number U string))
这说明它的每个参数和返回值都只能是这两种类型之一，而不同时为两者。但是，这样做会导致精度损失。
思考题
这种类型以何种方式损失精度？
观察到，对于这个类型，所有函数调用的返回值类型均为(number U string)。因此，对于每个返回值都必须区分数和字符串，不然我们将得到类型错误。所以，尽管我们知道给定两个数参数将返回数结果，但这种信息在类型系统中丢失了。
更巧妙的是，这个类型允许独立的选择每个参数的类型。因此，根据该类型，(+ 3 "x")也是合法的（且其返回值类型为(number U string)）。但我们描述的加法操作当然没有对这组参数定义过！
因此描述这种加法的更为合适的类型是
(^ (number number -> number)
(string string -> string))
这里的∧让人联想到逻辑上的合取操作符。这允许函数用两个数或者两个字符串进行调用，其它的则不允许。使用两个数调用返回数类型；使用两个字符串调用返回字符串类型；除此之外没有其它合法调用了。这刚好对应于我们期望的重载行为（有时也称为特设多态(ad hoc polymorphism)）。请注意这只能处理有限数量重载的情况。
15.3.6 递归类型
学过联合类型之后，值得讨论一下我们原来遇到过的递归数据类型表达式。如果接受变体作为类型构造器，我们可以将递归类型写作它们的联合吗？例如就BTnum来说，能否将它描述成等价于
((BTmt) U (BTnd number BTnum BTnum))
的类型吗，其中BTmt是零参数的构造器，而BTnd是三参数的？不过，这三个参数的类型是什么？按上面所写的类型，BTnum要么是类型语言内建的（这不能令人满意），要么是未绑定的。也许我们要的是
BTnum = ((BTmt) U (BTnd number BTnum BTnum))
问题是这个方程没有明显解法（还记得ω吗？）。
这种情况我们讨论值的递归时就熟悉过。那时，我们发明了递归函数构造器（并展示了其实现）来规避这个问题。这里我们同样需要递归类型构造器。按惯例它被称为μ（希腊字母“缪”）。有了它，我们可以将上面的类型写做
μ BTnum : ((BTmt) U (BTnd number BTnum BTnum))
μ是绑定构造；它将BTnum绑定到后面写的整个类型上，包括对BTnum自身的递归绑定。实践中，整个递归类型就是我们希望得到的称为BTnum的类型：
BTnum = μ BTnum : ((BTmt) U (BTnd number BTnum BTnum))
尽管这看起来像是循环定义，但请注意，右侧的BTnum不依赖于等式左侧的那个：即，我们可以将其重写为
BTnum = μ T : ((BTmt) U (BTnd number T T))
换句话说，BTnum的这个定义可以被认为是语法糖，可以在程序的各个地方替换使用，无需担心无限回归的问题。
语义层面上，对μ绑定的类型的意义有两种截然不同的思考方式：它们可以被解释为同构递归（isorecursive）或等价递归（equirecursive）。然而其中区别很微妙，超出了本章范围。【注释】只需理解递归类型可以被视为等同于它的展开。例如，我们定义数的链表类型为
NumL = μ T : ((MtL) U (ConsL number T))
于是有
μ T : ((MtL) U (ConsL number T))
= (MtL) U (ConsL number (μ T : ((MtL) U (ConsL number T))))
= (MtL) U (ConsL number (MtL))
U (ConsL number (ConsL number (μ T : ((MtL) U (ConsL number T)))))
以此类推（同构和等价递归之间的区别正是在相等性的概念上：是定义上的相等性还是同构意义上的）。每一步中，我们将参数T替换成整个类型。和值的递归一样，它的意思是需要时我们可以“获得另一个”ConsL构造。换种说法，链表的类型可以写成零或任意多元素的联合；这等价于包含零个、一个或任意个元素的类型；以此类推。任何数的链表都（恰好）符合这些类型。
Pierce的书中对此解释的非常好。
注意到，即使基于对于μ的这种非正式理解，我们已经可以给ω进而Ω提供类型。
练习题
描述
ω和Ω的类型。
15.3.7 子类型
假设我们有一个典型的二叉树定义；简单起见，我们假设值为数。为了说明问题，我们用Typed Racket写：
#lang typed/racket
(define-struct: mt ())
(define-struct: nd ([v : Number] [l : BT] [r : BT]))
(define-type BT (U mt nd))
考虑二叉树具体的值：
> (mt)
- : mt
#<mt>
> (nd 5 (mt) (mt))
- : nd
#<nd>
请注意，每个结构体构造器构造出自己对应类型的值，而不是BT类型的值。但是考虑(nd 5 (mt) (mt))：nd的定义表明其子树必须为BT类型，但我们可以传给它mt类型的值。
显然，使用mt和nd来定义BT并不是巧合。但是，它确实表明在进行类型检查时，不能只检查构造函数的相等性，至少我们目前所做的不够。相反，我们必须检查一种类型“适用于”另一种。这种行为被称为子类型化（subtyping）。
子类型化的本质是定义一种关系，通常用<:表示，将一对类型关联起来。在期待类型T的位置，如果放入类型S的值也成立，那么我们就称S <: T：换句话说，子类型化将可替代性的概念（即，任何期望类型T的值的地方，都可以被替换成类型为S的值）形式化。当这种关系成立时，S被称作子类型（subtype），T被称作超类型（supertype）。使用子集去解释这点是很有用的（通常也是准确的）：如果S的值是T的子集，那么期望接受T值的表达式收到S值时不会出问题。
子类型化对类型系统有着深远影响。我们必须审视每一种类型，并理解它和子类型化之间的相互作用。对于基本类型，这通常比较明显：数、字符串等不相交的类型，彼此无关。（存在一些语言，使用某基本类型表示其它的基本类型——例如，某些脚本语言中，数只不过是特殊写法的字符串，还有些语言中，布尔值就是数——这些语言中，基本类型之间也可能存在子类型关系，但是这并不常见。）但是，我们必须考虑子类型化和每个复合类型构造器之间的关系。
事实上，甚至我们关于类型的表述也需要改变。假设我们有个类型为T的表达式。通常我们会说它产生类型为T的值。现在，我们需要小心的说，它产出最多为T的值，因为它可能只产出T的某个子类型的值。因此，每个对类型的引用都隐含地涉及可能的子类型引用。为避免烦恼我会控制不这么做，但要小心，忽略这种隐含的解释可能导致推理错误。
15.3.7.1 联合
我们来讨论联合和子类型化会发生什么相互作用。显然，每个子联合是整个联合的子类型。在我们所用的例子中，显然每个mt值都是BT值；这同样适用于nd。因而，
mt <: BT
nd <: BT
于是，(mt)也是BT类型的，因此表达式(nd 5 (mt) (mt))类型正确，就是nd——因此也是BT类型。一般来说，
S <: (S U T)
T <: (S U T)
（我们写了两个看上去差不多的的规则，这是为了明确说明子类型处在联合中的哪“一边”并不重要）。它的意思是，S的值可以被认为是S U T的值，因为任何S U T类型的表达式都确实可以包含S类型的值。
15.3.7.2 交叉
既然到了这里，我们也简要的讨论一下交叉。正如你可能想象的那样，交叉的行为是对偶的：
(S ∧ T) <: S
(S ∧ T) <: T
为了说明这点，使用子集的解释：如果值即是S也是T，显然，它可以是两者中的任意一个。
思考题
为什么下面两条假设不成立？
(S U T) <: ST <: (S ∧ T)
第一条不成立是因为类型T的值是(S U T)中完全合法的值。例如，数是类型(string U number)的一员。然而，数不可以在需要类型为string的时候被使用。
至于第二条，类型T的值一般来说不是类型S的值。任何希望类型(S ∧ T)消费者希望其能够既作为T也作为S，而后一点无法保证。例如对前面重载的+来说，如果T为(number number -> number)，那么该类型的函数无法对字符串进行处理。
15.3.7.3 函数
我们还讨论过一种复合类型：函数。【注释】我们需要决定子类型关系中，任何一个类型为函数时的规则。通常我们认为函数和其它类型不相交，因此我们只需考虑函数类型作函数类型子类型的情况：也既，何时式子
(S1 -> T1) <: (S2 -> T2)
成立？方便起见，我们称类型(S1 -> T1)为f1，(S2 -> T2)为f2。问题就变成了，如果表达式的期望类型为f2，何种情况下给其传递f1类型的函数是安全的？使用子集合解释来考虑这个问题比较容易。
我们还讨论过参数化数据类型。在本书中，对它们子类型化的探索作为练习留给读者。
考虑f2类型的使用。它返回值的类型为T2。因此，函数调用所在的上下文会对T2类型的值满意。显然，如果T1和T2相同，那么这里f2的使用也能通过类型检查；类似的，如果T1是T2值的一个子集，也是可以的。唯一的问题是，如果T1的值比T2多，该上下文将可能遭遇非期望的值，从而导致未定义行为。换句话说，我们需要T1 <: T2。注意这里包含的“方向”与整个函数类型中的方向相同；这被称为协变（covariance，两者在相同的方向上变化）。这也许正是你所期望的。
出于同样的原因，你可能认为参数位置也出现协变：即S1 <: S2。这也符合预期，但它是错的。让我们看看为什么。
调用f2类型的函数，需要提供类型为S2的值作参数。假设我们将函数替换为类型f1的。如果S1 <: S2，这意味着新函数仅能接受S1类型的值——这是一个严格子集。这意味着对于某些值——在S2中但不在S1中的值——函数调用会提供它们为参数，而换入的函数在它们之上并无定义，这导致未定义的行为。为避免此，需要假定相反的方向：即替代函数应该至少能接收原函数能够接收的那些值。因此我们需要S2 <: S1，我们说该位置是逆变（contravariant）的：它和子类型化方向相反。
综合这两个发现，我们得到函数（对于方法也一样）子类型化的规则：
(S2 <: S1) and (T1 <: T2) => (S1 -> T1) <: (S2 -> T2)
15.3.7.4 实现子类型
当然，这些规则假定我们已经修改了类型检查器遵循子类型化的要求。子类型化的本质规则是，如果有表达式e，其类型为S，且S <: T，那么e也具有类型T。虽然这听起来很直观，但它也有问题，原因有二：
- 到目前为止，我们所有的类型规则都是语法驱动的，这使我们可以编写递归下降的类型检查器。但现在有可一条适用于所有表达式的规则，我们不知道何时应用这条规则了。
- 可能存在很多级别的子类型。这使得何时“停止”子类型化不再是个显而易见的问题。特别是，原来类型检查会求出表达式的类型，现在表达式可以有很多可能的类型；如果我们返回了“错误”的类型，可能会导致类型错误（因为它不是上下文期望的类型），尽管这时候可能存在其它的类型能够满足上下文需求。
这两个问题指出的是，我们这里给出的关于子类型化的描述根本上来说是声明性的：我们描述了它是怎样的，但是没有将这种说明转换成算法。对于每个实际的静态类型语言，将其转换成子类型算法——实现类型检查器的实际算法（理想情况下，该类型检查器仅让所有声明机制下被认为是有效的程序通过类型检测，也即，既可靠又完备）——或多或少是个有趣的问题。
15.3.8 对象类型
正如我们前面提到的，对象的类型通常分为两个阵营：名义的和结构的。名义类型大多数程序员通过Java都熟悉了，所以这里不多讨论。对象的结构类型是说，对象的类型本身就是一个结构化的对象，由字段的名字及它们的类型组成。例如，有两个方法——add1和sub1——的对象，其类型将是：
{add1 : (number -> number), sub1 : (number -> number)}
（为方便引用，我们称这个类型为addsub。）类型检查的做法也很容易预计：对于字段的访问，我们只需确保字段存在，并将解引用表达式类型求为该字段的声明类型；对于方法调用，我们不仅需要确保对应成员存在，还要确保其类型是函数。到目前为止，一切都很简单。
对象类型会因为很多原因而变复杂：
很多书都专注于此问题。尽管有点过时，但是Abadi和Carelli的《A Theory of Objects（对象理论）》仍然很重要。Bruce的《Foundationos of Object-Oriented Languages: Types and Semantics（面向对象语言基础：类型和语义）》更为现代，阐述也更温和。Pierce的书则漂亮的覆盖了所有必要的理论。
- 自引用。
self的类型是什么？它必须和整个对象的类型相同，因为任何可以从“外部”施加到对象上的操作也可以通过self在“内部”施加。这意味着对象是递归类型。 - 访问控制：私有（private）、公共（public）和其它限制。这导致对象“外部”和“内部”类型之间的区别。
- 继承：不仅需要为父对象指定类型，还需要考虑继承路径上哪些东西可见，这和“外部”可见的东西又有区别。
- 多重继承和子类型之间的相互作用。
- 像Java这样的语言中，类和接口之间的关系存在运行时成本。
- 赋值。
- 类型转换。
- 横生枝节。
等等。其中的一些问题会因为名义类型而简化，因为给定类型名我们就可以确定其行为的所有信息（类型声明实际变成了一个字典，从中可以查询关于对象的描述），这也是赞成名义类型的一个论据。
请注意，Java的方法不是构建名义类型系统的唯一方法。之前讨论过，Java的类系统不必要地限制了程序员的表达能力；相应地，Java的名义类型不必要地将类型（接口描述）和实现混为一谈。因此，名义类型系统可以比Java做的好得多。例如，Scala在这个方面就做出了重要的改变。
对这些问题进行充分论述需要更多的篇幅。这里我们只讨论一个有趣的问题。还记得我们说过，子类型化迫使我们考虑每种类型构造器吗？有了对象的结构类型，我们就必须多考虑一种：对象类型构造器。因此我们必须了解它与子类型化之间的相互作用。
在开始之前，先来确保我们理解对象类型到底意味着什么。考虑上面的addsub类型，其中列出了两个方法。什么对象的类型可以是它？显然，恰好拥有这两个方法、且方法的类型符合的对象符合条件。同样明显的是，如果某个对象只包含这两个方法中的一个而不含另一个，不管它还包含有其它什么，都不符合条件。但其中短语“不管它还包含其它什么”是最先要考虑的。如果对象表示的是算术包，除了这两个方法之外，它还包含+和*呢（所有方法的类型也都正确）？这种情况下的对象当然能提供上面两个方法，因此该算术包确实具有类型addsub。不过将其作为类型addsub使用时，其它方法不可用。
下面我们写下这个包的完整类型，称之为as+*：
{add1 : (number -> number),
sub1 : (number -> number),
+ : (number number -> number),
* : (number number -> number)}
前面论证的是，类型as+*的对象也允许被声明为类型addsub，这意味着它可以放入任何期望addsub类型值的上下文。换句话说，我们刚才的意思其实是as+* <: addsub：
{add1 : (number -> number), {add1 : (number -> number),
sub1 : (number -> number), <: sub1 : (number -> number)}
+ : (number number -> number),
* : (number number -> number)}
这可能乍一看令人困惑：我们说过子类型化遵从集合包含关系，因此我们期望小的集合在左侧而大的集合在右侧。可这里，好像“大的类型”（至少在字符数量的意义上是）在左侧而“小的类型”在右侧。
要理解为什么这是正确的，需要建立这样的直觉：“越大”的类型包含的值越少。左侧的每个对象都含有四个方法，而且其中包含了右侧的那两个方法。但是，有很多对象有右侧的两个方法，但是不包含左侧那另外两个方法。如果我将类型看作对可接受值形状的约束的话，“更大”的类型给定了更多的约束，因此会导致更少的值。于是，尽管类型的大小关系可能看上去不对，但是它们所包含的值的集合的大小关系是正确的。
更一般地，这表明从对象中删除字段就能获得超类型。这被称为宽度子类型化（width subtyping），因为子类型“更宽”，而我们通过调整对象“宽度”来移动到更上层的类型。即使在Java的名义类型世界中也能看到这点：当沿着继承链上溯时，类中的方法和字段越来越少，直到Object——所有类的超类型——包含得最少。因此对于Java中的任意类类型C，C <: Object。
有时，缩小（narrowing）和拓宽（widening）的使用方式会让人疑惑，它看上去好像用反了一样。拓宽是指从子类型转到超类型，因为它是从一个“较窄”（较小）的集合到一个“较宽”（较大）的集合。这些术语是独立演化而来的，很不幸，并不一致。
正如你可能预计的那样，还有一种重要的子类型化形式，是关于给定成员内部的。就是说，任何特定的成员都可以归入相应位置的超类型。出于显而易见的原因，这种形式的子类型化被称为深度子类型化（depth subtyping）。
练习题
构造两个深度子类型化的例子。其中一个，给定字段为对象类型，使用宽度子类型化去取该字段的子类型。另一个例子中，给定字段为函数类型。
Java中限制了深度子类型化，它倾向于类型在对象层次结构中保持不变，因为这对传统的赋值操作来说是安全的。
宽度和深度子类型化的结合包含了对象子类型化中大部分最有趣的情形。然而，仅实现这两种子类型化的类型系统不可避免地会招致程序员恼火。其它方便的（而且数学上必须的）规则还包括：改变名称排列顺序的能力、反身性（每个类型是其自己的子类型，因为将子类型关系解释为⊆更方便）和传递性。像Typed JavaScript这样的语言使用了所有这些特性为程序员提供最大的灵活性。