2. 类型推断¶
2.1. 类型环境¶
类型环境 是一种将表达式与数据类型关联起来的环境（而不是像我们迄今为止在解释器中使用的环境那样，将表达式与值关联起来）。
例如，假设你的语言是 Java，请为类型环境 tenv 填写以下问号：
[ [true, ???], [1, ???], [3.4, ???] ]
2.2. 用后系统表示的类型规则¶
类型规则是相对于类型环境，通过一种称为 Post 系统 的条件规范来指定的。该条件规范中的“已知条件”指定在虚线上方。可以从“已知条件”得出的结论指定在虚线下方。
例如，以下是类型环境 tenv 中一条可能的类型规则：
type-of E1 is bool
type-of E2 is T {Note: T stands for any type}
type-of E3 is T
------------------------------------
type-of (if E1 then E2 else E3) is T
这条规则是否准确描述了 JavaScript 的类型系统？Java 的类型系统呢？
2.3. 在简化版 ML 中的类型系统¶
由于我们将在 programming language ML 的上下文中讨论类型问题，特别是参数多态和类型推断，因此让我们首先严格地提供一个非常小的 ML 子集的语法。暂时可以将其视为带有整数、实数、布尔值和条件表达式的静态类型 lambda 演算。
<type> ::= <type-variable>
| int
| bool
| real
| <type> -> <type> {Example: int -> bool is the type of a predicate}
<expr> ::= <identifier>
| fn <identifier> => <expr>
| <expr> <expr> {Note: function applications don't have to be parenthesized}
| if <expr> then <expr> else <expr>
2.4. 使用 Post 系统规则描述 ML 中的类型推断¶
我们已经提供了一个描述 if-then-else 表达式类型的 Post 系统。现在我们需要用于函数定义和函数应用的 Post 系统规则。
在类型环境 tenv 中：
type-of <identifier> is T1 {Note: T1 and T2 stand for any types}
type-of <expr> is T2
-----------------------------------------------
type-of (fn <identifier> => <expr>) is T1 -> T2
In type environment tenv:
type-of <expr1> is T1 -> T2
type-of <expr2> is T1
------------------------------
type-of <expr1> <expr2> is ??? {What should ??? be?}
mini-ML 的 Post 系统规则的另一个例子是，对于给定的类型环境：
type-of x is bool
type-of y is int
---------------------------------------------------
type-of (fn x => fn y => if x then 1 else y) is ??? {What should ??? be?}
以下是 ML 类型推断引擎对某些函数定义的响应示例。在每个示例中，第一行是程序员输入的函数定义；第二行是 ML 输出的针对该定义所推断的类型。
现在，请将自己置于 ML 类型推断引擎的位置，尝试使用之前定义的 Post 系统规则来确定 ML 为何会以这种方式响应。
val g = fn x => fn y => if x then 1 else y;
fn : bool -> int -> int
val add1 = fn x => x + 1;
fn : int -> int
val add1r = fn x => x + 1.0;
fn : real -> real
val double = fn x => x + x;
fn : int -> int
val doubler = fn (x:real) => x + x;
fn : real -> real
2.5. ML 中的参数多态¶
要理解参数多态是什么，请考虑 Java 中以下两个恒等函数 id1 和 id2 之间的区别。
public static int id1( int a ) {
return a;
}
public static < E > E id2( E a ) {
return a;
}
System.out.println(id1(4));
System.out.println(id2("Hello"));
上述哪种方法展示了参数多态性？
现在让我们将注意力转向 ML 中如何处理参数多态性。
ML 使用带有参数多态性的静态安全类型推断解释器。在继续之前，请确保您理解 ML 类型系统的每个所述特性的含义。
ML 的类型推断算法总会为变量或参数重构出限制最少的类型。这就是它拥有类型变量的原因，例如 'a 和 'b。ML 类型变量（即代表类型而非值的变量）总是以撇号开头。
例如，一个类型被推断为 'a list 的变量是一个所有元素都具有相同类型的列表，但该类型可以是任何类型。因此，类型变量 'a 可以代表 int 类型、bool 类型，甚至 int list 类型；在这些情况下，'a list 分别是 int list（仅包含整数）、bool list（仅包含布尔值），甚至是 int list list（仅包含 int list）。下面展示了这三种列表类型的实例。
让我们先理解 ML 列表：
[true, false, true] {ML will infer this is a bool list}
[true, false, true, false] {ML will infer this is a bool list}
[1,2,3,4,5] {ML will infer this is an int list}
["foo", "bar", "baz"] {ML will infer this is a string list}
[17, "foo"] {ML will infer this is ILLEGAL}
[ [1,2,3], [4,6], [0,233] ] {ML will infer this is an int list list}
[ [1,2,3], [4,6], [0,233], [ [1], [2,3] ] ] {ML will infer this is ILLEGAL}
确保你理解为什么上面的最后一个列表是非法的。
ML 中的 hd 和 tl 函数与我们在 fp 模块中使用的对应函数完全相同。然而，要将元素添加到列表前端，必须使用 :: 运算符（或 cons 运算符）。例如，1::[2,3] 会生成列表 [1,2,3]。
现在来看参数多态的要点。考虑 ML 如何推理以下涉及列表的函数。
val rec sumlist = fn lst => if lst = nil {Note: nil is the same as the empty list []}
then 0
else (hd lst) + (sumlist (tl lst));
ML's response: sumlist = fn : int list -> int
val rec lengthlist = fn lst => if lst = nil
then 0
else 1 + (lengthlist (tl lst));
ML's response: lengthlist = fn : ''a list -> int
同样，'a （您可以忽略此处第二个前导单引号）是一个类型变量，表明 lengthlist 将接受任何类型的列表，而 sumlist 仅适用于整数列表。您能想出这是为什么吗？
2.6. ML 中的类型推断¶
所有 ML 函数都是单参数函数。当我们需要在 ML 中实现多参数函数的等价形式时，有两种策略。第一种是使用我们之前描述过的 柯里化 。第二种是使用一个作为 ML 元组 的单参数。以下是 ML 中元组的示例：
(17, "foo") int * string
(12.5, 13.5, 9) real * real * int
(true, false, true) bool * bool * bool
因此，以下带有一个元组参数的函数表现得如同具有三个参数的函数。
val add3 = fn (x,y,z) => x + y + z;
而 ML 的类型推断器将告诉我们关于 add3 类型的以下信息：
add3 = fn : int * int * int -> int
相比之下：
val add3curried = fn x => fn y => fn z => x + y + z;
是同一函数的柯里化版本，其类型签名由 ML 推断为：
add3curried = fn : int -> int -> int -> int
再考虑一个类型推断示例：
val rec map = fn (f,lst) => if lst = nil
then []
else (f (hd lst))::(map (f, (tl lst)));
ML 对此函数推断出什么？关键字 rec 是什么意思？
2.7. 类型推断问题 1¶
下面列出了六个带编号的 ML 表达式。它们每一个都是已输入到 ML 中的函数定义。
六个 ML 函数定义
1 val x = fn (f, g, h) => if g < h then f else if g <= f then h else 5.5;
2 val x = fn f => fn g => fn h => if g < h then f else if g <= f then h else 5.5;
3 val x = fn f => fn g => fn h => if f g then f else if g > 4.5 then h else f;
4 val x = fn (f, g, h) => if f g then f else if g > 4.5 then h else f;
5 val x = fn (f, g, h) => if g f then f h else (h + 3);
6 val x = fn f => fn g => fn h => if g f then f h else (h + 3);
下面列出了当上述六个表达式输入时，ML 提供的六个类型推断响应。不幸的是，它们已被打乱。在接下来的六个练习问题中，你将帮助把每个类型推断响应与上面正确的 ML 表达式进行匹配。
ML 的类型推断响应（已打乱）
1 fn : (real -> bool) -> real -> (real -> bool) -> real -> bool
2 fn : (int -> int) * ((int -> int) -> bool) * int -> int
3 fn : (real -> bool) * real * (real -> bool) -> real -> bool
4 fn : real * real * real -> real
5 fn : (int -> int) -> ((int -> int) -> bool) -> int -> int
6 fn : real -> real -> real -> real
上述六个函数定义和六个类型推断响应在以下六个练习题中均被引用。
