类型推断

Type Inference.

type inference 是 ML 一个十分优雅的特性。在我接触过的所有 (极其有限的) 语言中从未见过这个 feature。

Java, C, ML 都是 statically typed languages。与之相对的是 dynamically typed language，例如 Racket, Ruby, Python。动态类型语言在运行时才会确定 bindings 的类型；因此在这些语言中类型错误是一种 run-time error 而非 compile-time error。

与 Java 和 C 又不同，ML 的类型是隐式 (implicitly typed) 的，即我们几乎不需要声明 binding 的类型。这个 feature 真的非常的厉害，它使得：

• binding 声明的流程大大简化；我们可以完全把类型的问题抛在一边。
• 优雅的支持参数多态 (parametric polymorphism)。

这样做的代价就是，ML 的 type-checker 远比其他显式类型语言的复杂。在程序员不具体声明 binding 类型的前提下，type-checker 需要根据代码与 bindings 之间的关系推断 (infer) 出所有可能的 type annotations。如果不存在任何一种解，type-checker 将会拒绝 (reject) 该程序。

注意，虽然 type inference 与多态联系紧密，但它们终究是两个独立的概念：举例来说，Java 支持泛型 (generics types)，但它是一种显式类型语言，不支持类型推断。

Undecidability

When we say type inference may be impossible, we mean this is the technical sense of undecidability, like the famous halting problem.

对于某些 type system，不存在一个有效的 type inference 能够同时满足以下三个条件：

• the inference process always terminates.
• the inference process always succeeds if inference is possible.
• the inference process always fails if inference is not possible.

关于这一部分的详细内容将会在 P2 中介绍；由于 type inference 系统是 static checker 的一部分，这牵涉到 static checker 的正确性 (correctness) 问题。

幸运的是，ML 的 type inference 算法设计得非常简洁与优美；虽然存在 non-trivial 的程序能够使得 inference 效率变得非常低，但在现实应用背景下这种情况几乎不可能发生。

Overview of ML Type Inference

ML 的 type inference 大致遵循以下规则：

• It determines the types of bindings in order, using the types of earlier binding to infer the types of later ones. This is why you cannot use later bindings in a file. (When you need to, use mutual recursion and type inference determines the types of all mutually recursive bindings together)
• For each val and fun binding, it analyzes the binding to determine necessary facts about its type. We gather facts for function calls, pattern-matches, etc.
• Afterward, use type variable (e.g., 'a) for any unconstrained types in function arguments or results.
• Enforce the value restriction such that only variables and values can have polymorphic types.

ML type inference 的这种 “going in order” 的优美设计使得其不会 reject 任何一个能够 type-check 的程序，同时也不会 accept 一个不能 type-check 的程序。因此，explicit type annotations really are optional.

1
2
3
4

fun length xs =
    case xs of
        [] => 0
      | x::xs' => 1 + (length xs')

我们来看这个例子：type inferencer 开始按照顺序进行类型推断。

• length has type T1->T2.
• xs has type T1. (参数)
• T1=T3 list. (根据 case...of 的 pattern matching 得出)
• T2=int. (函数返回值可以为 0)
• x has type T3 and xs' has type T3 list.

至此，我们已经获得了所有变量的类型。最后 type inferencer 对于所有的 unconstrained types 统一的分配 type variables：T3='a, T1=T3 list='a list. 对于函数 length 的类型推断完成：length: 'a list->int.

type variable 'a indicates itself as a polymorphic datatype (or generic type). 因此，函数 length 体现了 parametric polymorphism：它的参数类型是一个多态类型。

更多的例子，以及关于 value restriction 的相关介绍见课程提供的 section3sum.pdf。在之后，它还介绍了在 ML 中使用 signature 实现抽象的方式。但是这一部分内容并不是 functional programming 的核心 feature，在此按下不表。

Reference

Course info:

Programming Languages, Part A, University of Washington, Lecturer: Professor Dan Grossman.