上周，我们在 cubiml 中实现了条件流约束(也就是存在多态)。今天，我们将从语言的不同方向出发，解决如何让程序员在程序中手动注释类型的问题。在这篇文章中，我将介绍为什么静态类型注释是有用的，以及如何为它们的设计提供参考，下周将进行实际的实现。这篇文章有点啰嗦，所以如果你只想看代码而不想看所有的背景讨论，请随意跳到下一篇文章。

代码生成和静态类型

在讨论为什么你实际上可能想要支持静态类型注释这个问题之前，我想先讨论一下类型注释的一个常见用途，即坏主意。

大多数流行的静态类型语言都利用静态类型系统来生成代码。简单地添加或改变类型注释就会改变代码行为方式，无论是插入隐式转换还是隐式选择调用哪些函数在哪里调用。然而，这有一些缺点。

最大的问题是，它使语言变得更加复杂，因为你不能再将静态类型系统和运行时语义解耦。在 TypeScript 这样的语言中，类型检查和执行是独立的。你不需要模拟类型检查器来确定一段给定的代码在运行时将做什么。然而，大多数编程语言都违反了这个属性。例如，考虑以下 Rust 行。它是做什么的？

let cases = cases.into_iter().collect();

这是一个技巧问题。在这段代码出处的特定背景下，它将向量转换为哈希表。然而，这段代码几乎可以做任何事情，这取决于 cases 在代码的其他地方如何使用。在这种情况下，实际的行为是由类型声明控制的，这些类型声明是 300 行，并且从代码本身去掉的间接好几层，但在更大的项目中，类型声明可能在不同的文件中，甚至在一个单独的箱子里。

除了远距离影响的诡异动作外，这种事情是不好的，因为这意味着静态类型系统的细节被嵌入到语言的运行时语义中。Cubiml 是一门非常简单的语言 - 不仅仅是因为它还没有时间去积累残缺，而是因为它的设计很用心，就是为了简单。你可以把类型规则放在一页上，把运行时语义放在另一页上，或多或少，而且无论任何给定目的你只需要其中一页。

相比之下，对于大多数编程语言，你需要知道所有东西的静态类型，以确定代码在运行时将做什么，这意味着你不能像这样将语言规范模块化。静态类型系统是运行时语义的一部分。在特别糟糕的情况下（但还是很常见），即使知道类型系统也是不够的 - 你需要知道编译器的精确实现细节，以了解它将推断哪些类型，从而了解代码将做什么。

遗憾的是，这种缺乏模块化设计的情况在流行的静态类型语言中几乎是普遍存在的。事实上，我所知道的唯一一个没有（大部分）这样做的流行语言是 TypeScript，在这种情况下，设计者被迫将静态和运行时语义分开，因为运行时语义已经以 JavaScript 的形式存在。

除了使语言变得不必要的复杂和难以推理之外，使用静态类型来决定行为与类型推理结合得特别差。当你使用静态类型来决定调用哪些函数，而这些函数又有不同的类型反馈到类型推理中，那么你通常会以一个矛盾的循环结束，类型推理不再有定义良好定义或可预测的结果。

许多语言通过定义默认类型来缓解这个问题，当编译器无法正常推断类型时，就会填入这些类型。虽然有时很方便(这主要是为了解决数字类型在语言中的其他设计缺陷，否则会使数字类型的使用变得过于繁琐)，但它会导致意想不到的行为，同时也抛弃了任何可预测类型推理的可能性。我在 Rust 代码中至少有一个问题是由于编译器意外地猜错了一个整数的类型而导致的。

此外，默认类型实际上已经阻止了 Rust 增加某些功能，因为默认类型意味着让类型系统更精确，不再是一个向后兼容的改变。简单地修复编译器来使推断类型更好是一个破坏性改变，因为这意味着它不再像以前那样猜测不同类型，导致以前编译的代码出现类型错误，或者在某些情况下，代码的静默表现与以前不同。

但是，关于不应该做什么已经够了。现在让我们来看看为什么你可能想要静态类型注释的一些好的理由。

类型注释的用途

显然，如果你想做一个静态类型语言，但又不想使用类型推理，那么你就需要类型注释。然而，类型推理使类型注释的传统用法变得过时了。例如，cubiml 经过精心设计，编译器可以在没有注释的情况下对整个程序进行类型检查。你可以得到传统静态类型检查的所有好处，而没有自己写注释的缺点。那么为什么要破坏这一点呢？主要有三个原因：增加编译器错误的数量，提高类型检查性能和错误信息质量，支持不可推断的类型系统特性。

增加编译器错误的数量

类型检查器通常被设计成健全的，即拒绝那些在运行时执行会导致错误条件的程序（语言通常包括转义舱口，以绕过类型系统，如 Rust 的 unsafe，TypeScript 的 any，或 Ocaml 的Obj.magic，但是这些都是“使用风险自负”的，所以我们在讨论类型检查的健全性时，可以假装它们不存在)。

然而，有时你可能想拒绝那些不会在运行时产生语言定义的错误条件的程序。也许它们违反了程序员的假设，而这个假设并不是默认类型检查的一部分，因此虽然不导致类型错误，但可能在运行时出错。

手动类型注释允许你提供比编译器推断的类型更不精确的类型，从而拒绝编译器本来会接受的额外程序。例如，考虑以下代码：

let f = fun x ->
    {thing1=x + 32; thing2="Hello, " ^ x};

函数 f 接受一个输入，并在函数中把它当作整数和字符串。没有任何可能的值是函数可以正确操作的，但只要函数从未在任何地方被实际调用，编译器仍然会接受它。这是健全的，因为如果函数从未被调用，在运行时就不会产生类型错误，但这可能不是程序员的本意。

然而，如果我们添加一个类型注解，int -> {thing1: int; thing2: str}，我们可以告知编译器 x 期望只能是整数，因此编译器会抱怨它被当作字符串使用，即使函数从未被调用。

let f = (
    fun x ->
        {thing1=x + 32; thing2="Hello, " ^ x}
    : int -> {thing1: int; thing2: str}
);

改善性能和错误信息

在推断类型时，编译器必须跟踪符合代码和类型规则的最精确的类型，这使得类型推断很慢。此外，当出现类型错误时，编译器不知道程序员的意图，因此必须考虑到在导致类型错误的推理链中的任何一点都可能出现错误。例如，考虑以下代码：

let addi = fun args -> args.a + args.b;

let addf = fun args -> args.a +. args.b;

let rec fib_sub = fun args ->
    if args.n <= 0 then
        args.a
    else
        let a = addf args in
        fib_sub {n=args.n - 1; a=a; b=args.a};

let fib = fun n -> fib_sub {n=n; a=1; b=1}

这是一个经典的斐波那契数计算函数，但是有一个问题。它似乎无法决定计算值是用浮点数还是用整数。

TypeError: Value is required to be a float here,
let addi = fun args -> args.a + args.b;

let addf = fun args -> args.a +. args.b;
                                 ^~~~~~

let rec fib_sub = fun args ->
But that value may be a integer originating here.
        fib_sub {n=args.n - 1; a=a; b=args.a};

let fib = fun n -> fib_sub {n=n; a=1; b=1}
                                   ^

但实际的错误在哪里呢？也许程序员的意思是要把数值计算成浮点数，而错误在于最后一行写的是 1 而不是 1.0。或者他们的意思是要用整型来计算，错误是写了 addf 而不是 addi。也可能 addf 本来就应该在整型上工作。

编译器没有办法读懂程序员的心思，所以任何错误信息必须要么足够详细，以说明所有的可能性，要么就会遗漏潜在的重要信息。（Cubiml 目前的错误信息采取的是后一种方式）。同样，有一个长长的推理链建立在错误上，使得类型推理更慢。

然而，程序员可以打破这个链条，通过一些明智放置的人工类型注释来解决这些问题。例如，也许他们的意思是函数要对浮点数进行操作：

let addf = fun args -> args.a +. args.b;

let fib_sub =
    let rec fib_sub = fun args ->
        if args.n <= 0 then
            args.a
        else
            let a = addf args in
            fib_sub {n=args.n - 1; a=a; b=args.a} in

    (* a manual type annotation for fib_sub *)
    ( fib_sub : {n: int; a: float; b: float} -> float );

let fib = fun n -> fib_sub {n=n; a=1; b=1}

这里的类型注释导致了一个更简单、更有用的错误信息：

TypeError: Value is required to be a float here,

    (* a manual type annotation for fib_sub *)
    ( fib_sub : {n: int; a: float; b: float} -> float );
                                      ^~~~~

let fib = fun n -> fib_sub {n=n; a=1; b=1}
But that value may be a integer originating here.
    ( fib_sub : {n: int; a: float; b: float} -> float );

let fib = fun n -> fib_sub {n=n; a=1; b=1}
                                        ^

同样，如果他们的意思是对整型进行操作，所产生的错误信息也比之前更加具体：

TypeError: Value is required to be a float here,
let addf = fun args -> args.a +. args.b;
                                 ^~~~~~

let fib_sub =
But that value may be a integer originating here.

    (* a manual type annotation for fib_sub *)
    ( fib_sub : {n: int; a: int; b: int} -> int );
                            ^~~

let fib = fun n -> fib_sub {n=n; a=1; b=1}

也许程序员错误地认为 addf 可以相加整数。在这种情况下，添加一个类型注释来检查这个假设，很快就会发现问题。

let addf = fun args -> args.a +. args.b;

let rec fib_sub = fun args ->
    if args.n <= 0 then
        args.a
    else
        (* let's make sure that addf is an int-adding function *)
        let addf = (addf : {a:int; b:int} -> int) in
        let a = addf args in
        fib_sub {n=args.n - 1; a=a; b=args.a};

let fib = fun n -> fib_sub {n=n; a=1; b=1}

TypeError: Value is required to be a float here,
let addf = fun args -> args.a +. args.b;
                                 ^~~~~~

let rec fib_sub = fun args ->
But that value may be a integer originating here.
    else
        (* let's make sure that addf is an int-adding function *)
        let addf = (addf : {a:int; b:int} -> int) in
                                     ^~~
        let a = addf args in
        fib_sub {n=args.n - 1; a=a; b=args.a};

支持不可推断型系统

目前为止，我们只谈到了可以进行类型推理的类型系统特性，因为这是一个关于类型推理的系列。然而，每一种流行的静态类型语言都有打破类型推理的特性，通常以许多不同的方式。我怀疑这其中很大一部分只是为了解决这些语言中缺乏子类型的问题（另见：Ocaml 的“放宽的值限制”)，但不可推断的类型系统特性偶尔也确实有用。毕竟，如果你想在你的代码中验证图灵完备的不变量，你就需要一个图灵完备的类型系统来实现。

这些语言通常需要程序员提供一些类型注释，然后使用类型推理来填充剩下的部分。然而，从类型推理的角度来说，这并不是那么有趣的事情。

如前所述，我特意在本系列中只关注那些能使最坏情况下的渐近复杂度最小化的算法，而忽略了微优化，尽管微优化对现实世界的性能往往很重要。主要原因是，渐近复杂度是一个客观的衡量标准，而真实世界的性能是主观的，高度依赖于环境。

同样的问题也适用于不完全类型推理。像 Haskell 这样的语言的程序员经常会说，“在实践中”很少需要类型注释，但没有办法对这种说法进行有用的判断。一个类型系统是否完全可推理是一个客观的衡量标准。一种语言“在实践中”是否需要“很少”或“很多”类型注释是主观的，高度依赖于“在实践中”编写的代码。

此外，在实践中需要更少的类型注释甚至不一定是好事! 全类型推理的真正优势不仅仅是为程序员节省了一些按键，让重构变得更容易，而是它简化了语言的概念模型。像 cubiml 这样的语言的宣传是，你不必担心类型理论。你可以像在 JavaScript 中一样编程，并且在你犯错误之前忽略类型检查器，只有一些小的例外。（具体来说，类型检查器大多对流和上下文不敏感，因此有时会拒绝有效的程序，而推理它们的正确性需要对流或上下文敏感）。

相比之下，在部分推理编程语言中，一般的编程经验是随机添加类型注释，直到编译器关闭为止。与其说类型推理简化了语言的心智模型，不如说是复杂化了。程序员仍然要在心理上跟踪每个值会有什么样的静态类型，还要推理出哪些注释可以省略，哪些不能，以及为什么。如果类型注释一般可以顺利省略，那只是让程序员最终不可避免地遇到不能省略的情况时，编译器的错误就更加难以捉摸了。这也意味着，看似无害的代码改动，往往会突然导致其他代码无缘无故的可以或无法编译。

荣誉奖：IDE 支持

静态类型注释还有一些其他用途，我在这里没有提到。例如，一些 IDE 利用类型注释来提升代码完成、代码搜索、提供弹出式文档提示等（有些 IDE 利用类型注释使代码完成变得更差，抱怨）。

不过，我不会涉及这些，因为这“只是”用户体验和 IDE 设计的问题。CS 方面仅在可用算法制约着什么样的分析在技术上是可行的范围内才有意义，但在这些制约下，实际设计是一个主观的、以人为本的研究领域。而且正如 PyCharm 所展示的那样，太过聪明的做法很容易让你自作聪明，IDE 中花哨的分析导致的用户体验比 Sublime Text 这样“笨”但设计良好的 IDE 更差（甚至 Sublime Text 为了可用也需要禁用 TypeScript 插件）。

结论

鉴于上述情况，本系列将重点介绍类型注释，它涵盖了编译器已经可以自行推断的类型，以达到提升性能和错误信息和限制代码产生更多的编译器错误的目的。下周，我们将看到如何在 cubiml 中添加类型注释来实现这些目标。