四、Bugs：放弃、断言和合约

Bugs: Abandonment, Assertions, and Contracts

Cover Image

在 Midori 中，很多类型的 bug 都可能会触发放弃：

  • 不正确的类型转换
  • 尝试对null指针解引用
  • 尝试越界访问数组
  • 零除错误
  • 算数计算发生意外的上溢/下溢
  • 内存不足栈溢出
  • 显式放弃
  • 合约失败
  • 断言失败

我们最根本想法是，这里每一种错误都是不可恢复的。让我们逐一进行讨论。

普通的老 Bug

上面那些情况中，有一些是公认的程序 Bug。

很显然，不合法的类型转换、尝试对null解引用、数组越界访问、零除错误都是程序的逻辑错误，这些都是非法操作。我们在下文会看到，这些操作也有可能被认为是合法操作（比如当一个数除以零时，也许你想要把结果表示为 NaN）；不过我们先默认假设这些就是 Bug。

很多程序员都会接受这个结论。使用“放弃”来应对这些 Bug，使得这些 Bug 能够在开发阶段就被快速发现、快速修正。放弃确实有助于提高写代码的生产力。一开始我还有点惊讶，但确实很有道理。

而另一方面，上面其他的情况是否属于 Bug，则是个主观问题。我们必须决定当出现这些状况时程序的默认行为、可能还需要提供程序化的控制方法。我们当时还为此争论不休。

算数计算上溢/下溢

算数计算发生了意外的上溢/下溢究竟算不算一种 Bug，这就是一个有争议的问题。在不安全的系统里，这样的错误经常会导致安全漏洞。我建议你看看国家漏洞数据库，就能知道有多少漏洞是由这种问题导致的。

Windows TrueType 字体的语法分析器就曾经在过去的几年里不断地受到这类问题的影响（我们把它 port 到了 Midori，还有性能提升）。语法分析器似乎是这种安全漏洞的重灾区。SafeInt 因此而生，它本质上就是不让你使用语言本身提供的算术计算操作，转而使用这个库提供的受检查的计算操作。

当然，在这些漏洞中，大多数都跟访问不安全的内存有关。所以你可能会反驳说，溢出在一门安全的语言中没什么害处，应该被允许。然而，基于我们在安全方面的经验，通常当一个程序遇到了意外的上溢/下溢时，继续执行也不会得到正确的结果——简单来说，开发者经常会忽略可能发生的溢出，因此程序执行的结果也就无法预料。这很符合 bug 的定义，而“放弃”就是用来发现这些问题的。压死骆驼的最后一根稻草则是一个哲学问题：当我们面对任何有关正确性的问题时，我们更倾向于站在显式意图这一边。

因此，所有无标注的上溢、下溢都会被视为 Bug 并触发放弃。这与 C# 的 /checked 编译选项很类似，只有一点不同：我们的编译器会激进地优化掉冗余的检查。（对于 C# 来说，由于很少有人用到这个开关，代码生成器不会那么激进地删掉插入的检查。）多亏了语言和编译器的协同开发，生成的代码比大多数使用 SafeInt 的 C++ 编译器产生的结果要好。跟 C# 一样，unchecked 作用域结构可以用来显式指明允许上溢或下溢。

大多数 C# 和 C++ 程序员第一次听到这个决定时都持反对态度。但尽管如此，我们发现，由算术溢出所触发的放弃，十次有九次都是程序 Bug。剩下的一次是在我们进行了72个小时的压力测试之后发生的——我们不断地使用浏览器、媒体播放器等软件来折磨我们的系统——然后，一些没什么危害的计数器溢出了。我觉得相比于通过压力测试来使得程序更加成熟稳定（比如死锁和竞态条件），直接提前发现问题然后修了它要有意思得多了。

内存不足和栈溢出

内存不足（Out-of-Memory，OOM）的情况有点复杂。我们的方法在这当然也是有争议的。

在内存需要手动管理的情况下，错误码风格是最常见的检查方式：

X* x = (X*)malloc(...);
if (!x) {
    // 处理内存申请失败
}

这种方式有一个很微妙的好处：内存分配很痛苦、需要思考，因此使用这种技术的程序通常更加节俭、谨慎地使用内存。但这种方式有一个巨大的不足：它极易出错、同时会产生大量的没有经过测试的代码路径（code path）。如果一条代码路径没有被测试过，那么它很容易出问题。

当内存快要不够的时候，开发人员所采取的措施通常都不够妥当。以我在 Windows 和 .Net Framework 上的经验来看，这就是犯下严重错误的地方，衍生出了极其复杂的编程模型，比如 .Net 中所谓的受限执行区域（Constrained Execution Regions）。一个程序一瘸一拐，连一小块内存都拿不到，很快就会成为可靠性的敌人。Chris Brumme 的一篇非常赞的文章讲述了与其有关的故事。

我们的系统中有一些部分比较难搞，比如在内核的底层，放弃的范围肯定要比单一进程更大。不过我们在尽可能地控制这种代码的规模。系统中的其他部分呢？没错，你肯定猜到了——放弃。优雅而又简洁。

令人惊讶的是，这种方法似乎并没有带来太多的麻烦，我把大部分原因归功于隔离模型。实际上，根据资源管理的策略的设置，我们也可以有意地让使一个进程“内存不足”进而触发放弃，以此来证明整个系统的健壮性和可恢复性。

当某一次内存申请失败时，你也可以选择不触发放弃。这其实不太常见，但我们也有机制来支持这种选择。可能最合适的例子是：假如你的程序这一次想要申请 1MB 的内存。这跟平时小于 1KB 的对象内存申请不太一样，开发人员可能会提前考虑到内存不够的情况并作出充分的准备。比如：

var bb = try new byte[1024*1024] else catch;
if (bb.Failed) {
    // 处理内存申请失败
}

栈溢出是这个思路的简单延伸。实际上，由于我们的“异步链接栈”（asynchronous linked stacks）模型，栈内存不足在物理上就等同于堆内存不足，因此处理方法与 OOM 一致也并不令人惊讶。如今很多系统都用这样的方式来处理栈溢出。

断言

断言是指在代码中手动检查某些条件必须为真，否则就会触发放弃。与很多系统一样，我们的系统中断言也分为两种：仅在 Debug 模式下的断言和 Release 模式下的断言。然而不同的是，我们使用 Release 断言的时候更多。实际上，断言在我们的代码里随处可见，大多数的方法都有不止一个断言。

这种实践符合这样的哲学：当运行时遇到 bug 时，把它暴露出来要比继续执行更好。当然，我们的编译器后端知道如何激进地对这些断言进行优化。我们的代码中断言的密度很高，与很多高可靠系统所建议的很类似，比如在 NASA 的论文 The Power of Ten -Rules for Developing Safety Critical Code 中：

规则：代码中断言的密度至少为每个函数2个。断言用来检查在真正执行时不应该发生的反常现象。断言必须没有副作用，应当定义为布尔值检测。
原因：根据工业界编码工作的统计数据，通常每编写10行到100行代码，单元测试就能发现一个缺陷。发现缺陷的机率随着断言密度的增加而增长。断言也通常作为强防御编码策略（strong defensive coding strategy）所建议的一部分。

如果想要插入断言，只需要简单地调用 Debug.Assert 或是 Release.Assert：

void Foo() {
    Debug.Assert(something); // Debug-only assert.
    Release.Assert(something); // Always-checked assert.
}

我们同样实现了与 C++ 中 __FILE__ 和 __LINE__ 宏类似的功能，外加 __EXPR__，代表了断言中谓语表达式的文本。这样的话由于失败断言而导致的放弃将会包含一些有用的信息。

在早些时候，我们设计了与现在不同的断言“等级”。一共三级，Contract.Strong.Assert、Contract.Assert、Contract.Weak.Assert。最强的等级表示“始终检查”，中间的等级表示“编译器说了算”、最弱的等级表示“仅在 Debug 模式下检查”。我做了一个很有争议的决定——抛弃这种模型。实际上，我非常肯定，我们组里 49.99% 的人都讨厌我对术语的选择（Debug.Assert 和Release.Assert），但我始终都觉得这两个词很恰当，它们完美地表明了这两种断言究竟在做什么。旧的分类方法的问题在于，没有人确切地知道什么时候应该检查断言；在我看来，由于好的断言准则对于程序的可靠性极其重要，而断言的使用方法居然会令人困惑，这是我无法接受的。

在我们把合约（contracts）添加到语言中之后（下文很快就会介绍），我们也尝试过把 assert 设计为一个关键字。不过，最终我们还是继续使用了 API 的方式。主要的原因是，与合约不同，断言不是 API 签名（signature）的一部分；同时由于断言很容易以库的形式实现，我们也不确定把它加入到语言当中有什么好处；还有一点，“Debug 模式下的检查”和“Release 模式下的检查”之类的策略，看着就不像一门编程语言应该有的东西。我得承认，就算这么多年过去了，我还是不太确定哪种方式更好一些。

合约

合约是在 Midori 中发现 Bug 的最核心的机制，没有之一。我们是从 Singularity 开始做起的，它使用的是 Sing#，一门 Spec# 的变种语言。不过我们很快就换成使用正规的 C# 了，只能把我们想要的东西重新发明一遍。最终我们实现的模型跟最初的模型已经相去甚远。

多亏了我们的语言对不变性和副作用的理解，所有的合约和断言都被证明了是没有副作用的。这大概是这门语言最大的创新点，我肯定会再写一篇博客讲讲它的。

跟其他方面一样，我们也受到了很多其它系统的影响。Spec# 是最明显的一个。Eiffel 也对我们有很大的影响，尤其是有很多公开发表的研究。另外还有一些其他的研究工作也对我们有所帮助，例如基于 Ada 的 SPARK、一些实时与嵌入式系统的提议等等。更深入地讲，像霍尔公理语义这样的编程逻辑为所有的一切提供了基础。然而对我来说，最重要的哲学启发来自于 CLU、以及之后的 Argus 中提供的错误处理方法。

前置条件和后置条件（Preconditions and Postconditions）

合约最基本的形式就是方法的前置条件，它声明了要调用这个方法所必须满足的条件。通常来说先决条件会用来验证参数。它有时也会用来验证目标对象的状态，不过这非常少见，因为对于程序员来说考虑清楚模态（modality）是一件很困难的事。前置条件基本上就是调用者对被调用者做出的承诺。

在我们最终的模型中，前置条件使用 requires 关键字声明：

void Register(string name)
    requires !string.IsEmpty(name) {
    // 继续执行，字符串一定不为空
}

一种稍微不太常见的合约就是方法的后置条件。它声明了在这个方法调用之后应有的状态。这是被调用者对调用者做出的承诺。

在我们最终的模型中，后置条件使用 ensures 关键字声明：

void Clear()
    ensures Count == 0 {
    // 继续执行，调用者明确知道在方法返回时Count一定0
}

在后置条件中，同样可以通过特殊的名字 return 来引用返回值。旧值——比如在后置条件中需要引用输入的时候——可以通过 old(...) 来得到。例如：

int AddOne(int value)
    ensures return == old(value)+1 {
    ...
}

当然，前置条件和后置条件可以一起混用。例如，在 Midori 内核中的环形缓冲区的实现里：

public bool PublishPosition()
    requires RemainingSize == 0
    ensures UnpublishedSize == 0 {
    ...
}

这个方法的函数体在执行时可以确信 RemainingSize 一定为 0，调用者在调用之后也可以确信 UnpublishedSize 也一定为 0。

在运行时，任何一个合约没有被满足时，都将会触发放弃。

在这个领域，我们的方法跟其他人的工作有点不同。最近，合约在一些高级证明技术中的程序逻辑中作为一种表达式越来越流行，这些工具工厂使用全局分析来证明声明的的合约是否为真。我们也采用了类似的方法，但合约默认是在运行时检查的。如果编译器在编译期能够证明真假，那么它也可以不生成运行时检查的代码，或是抛出一个编译错误。

现代的编译器都有基于约束的分析，在这方面做得很好，例如我上篇博客中提到的范围分析。它们通过传递事实信息（facts）来对代码进行优化，例如消除冗余的检查：既包括显式声明的合约，也包括普通的程序逻辑。它们也能在合理的时间内完成这些分析，这样程序员才不会觉得太慢转而使用别的编译器。定理证明技术所支持的代码规模满足不了我们的需要。最好的定理证明分析框架花了整整一天来分析我们的核心系统模块！

进一步来说，方法所声明的合约是它签名的一部分。这就意味着这些合约会自动显示在文档里、IDE 的代码提示里，等等。合约就跟方法的参数类型、返回类型一样重要。合约其实就是类型系统的扩展，使用语言所能表达的任何逻辑来对类型交换（exchange types）加以控制。因此，所有常见的对子类型的要求都适用于合约。同样，这也有助于模块化局部分析，使用标准优化的编译器技术能够在几秒钟之内完成。

.NET 和 Java 中大约 90% 的异常都能够使用前置条件替代，包括所有的ArgumentNullException、ArgumentOutOfRangeException 以及相关的类型。更重要的是，我们不再需要手动检查之后再 throw 了。如今很多 C# 代码中四处可见这样的检查，仅在 .NET 的 CoreFX 仓库中就有上千个。例如，下面是 System.IO.TextReader 中的 Read 方法：

/// <summary>
/// ...
/// </summary>
/// <exception cref="ArgumentNullException">Thrown if buffer is null.</exception>
/// <exception cref="ArgumentOutOfRangeException">Thrown if index is less than zero.</exception>
/// <exception cref="ArgumentOutOfRangeException">Thrown if count is less than zero.</exception>
/// <exception cref="ArgumentException">Thrown if index and count are outside of buffer's bounds.</exception>
public virtual int Read(char[] buffer, int index, int count) {
    if (buffer == null) {
        throw new ArgumentNullException("buffer");
    }
    if (index < 0) {
        throw new ArgumentOutOfRangeException("index");
    }
    if (count < 0) {
        throw new ArgumentOutOfRangeException("count");
    }
    if (buffer.Length - index < count) {
        throw new ArgumentException();
    }
    ...
}

这样的写法不太好，原因有很多。显而易见的是它太冗长了，除此之外似乎没什么不好——然而，我们需要在文档中提及所有可能抛出异常，这似乎在提醒开发人员，这些异常需要被捕获。但这些异常真的不应该被捕获，相反，它们应该在开发阶段就发现这些 bug 然后修掉。

另一方面，如果我们使用 Midori 风格的合约，则这些代码可以简化为：

/// <summary>
/// ...
/// </summary>
public virtual int Read(char[] buffer, int index, int count)
    requires buffer != null
    requires index >= 0
    requires count >= 0
    requires buffer.Length - index >= count {
    ...
}

这段代码有很多地方值得一说。首先，它更简洁，更重要的是，它以一种文档化的方式描述了这个 API 的合约，调用者也更容易理解。相比于使用用于来描述这些错误条件，调用者还可以直接查看表达式，相关工具也更容易理解和利用这些条件。最后，当合约检查失败时，它会触发放弃。

同样值得一说的是，我们提供了非常多的合约帮助方法，以便能够更方便地实现一些常见的前置条件。上述的显式范围检查同样非常啰嗦，容易出错。我们可以改写为：

public virtual int Read(char[] buffer, int index, int count)
    requires buffer != null
    requires Range.IsValid(index, count, buffer.Length) {
    ...
}

说句有点偏题的，如果结合两个高级功能——数组切片和非空类型——我们能够进一步简化代码，同时提供了相同的承诺：

public virtual int Read(char[] buffer) {
    ...
}

还是让我们从头开始讲吧…

谦卑的开始

虽然我们最终的语法很像 Eiffel 和 Spec#，但就像我前面提到的，我们一开始并没有想改变语言本身。因此我们从 API 开始：

public bool PublishPosition() {
    Contract.Requires(RemainingSize == 0);
    Contract.Ensures(UnpublishedSize == 0);
    ...
}

这种方法有很多问题，就像 .NET Code Contracts 所遇到的一样。

首先，这种方式实现的合约属于 API 实现 的一部分，然而我们希望它成为 API 签名 的一部分。这似乎只是理论上的问题，但其实不是。我们希望生成的程序包含一些内置的元数据，从而像 IDE、调试器之类的工具能够在函数调用时把合约显示出来。我们也希望文档工具能够根据合约自动生成文档。把合约埋在实现当中无法实现这些功能，除非你知道如何反汇编这些函数然后再把这些信息提取出来（然而这是一种hack）。这也让合约与编译器后端的整合更加困难，生成高性能的代码需要这些信息。

其次，你可能会注意到对 Contract.Ensures 的调用。Ensures 需要在函数的每一个返回点调用，我们如何只使用 API 来实现呢？答案是：确实不能。一种方法是在编译器生成 MSIL 后，对 MSIL 进行重写，但这很麻烦。看到这你也许回想，为什么我们不能简单地承认这是一个语言的表达能力和予以的问题，然后加上专门的语法呢？

另一方面，一个长期举棋不定的问题是合约是否允许根据编译模式的不同而不同。很多经典的系统中，Debug 模式会检查合约，但完全优化的版本不会。在很长一段时间里，我们有三种不同级别的合约，就像我们之前提到的断言一样：

  • Weak，声明为 Contract.Weak.*，表示仅在 Debug 模式开启
  • Normal，声明为 Contract.*，表示由具体实现来决定什么时候检查合约
  • Strong，声明为 Contract.Strong.*，表示始终检查。

我得承认，一开始我觉得这种方案非常优雅。然而不幸的是，始终都有人对“Normal”合约存在疑惑，它们会在 Debug 还是 Release 模式下开启？开始两者都会开启？（也因此大家也都用错了 Weak 和 Strong。）不管怎样，我们开始把这种合约模式整合进语言，以及编译器后端工具链。而此时，问题开始不断出现。我们不得不做出一些妥协。

首先就是，如果你简单的把 Contract.Weak.Requires 翻译为 weak requires、把 Contract.Strong.Requires 翻译为 strong requires，你会的到一种相当笨拙而又不够普适的语法，过多可选的策略也让我不舒服。这就直接引出了 weak/strong 策略的参数化和可替换性。

其次，这种方法引入了一种新的条件编译模式，对我而言有点不爽。换句话说，如果你想要只在 Debug 模式下检查，已经有语法来实现了：

#if DEBUG
    requires X
#endif

最后——对我而言这是压死骆驼的最后一根稻草——合约应该是 API 签名的一部分。条件编译一个合约是几个意思？相关工具应该怎么看待 API 签名？需要为 Debug 和 Release 模式产生不同的文档吗？更进一步，如果我们真的采取了这种方式，你就失去了严格的保证——即如果前置条件不满足，你的代码就不会运行。

最后，我们修改了整个条件编译的方案。

我们最终只采用了一种合约：它是 API 签名的一部分，并且始终检查。如果一个编译器在编译阶段就能够证明合约成立（我们花了很大的精力在这个方面），那么可以省略这些检查。我们始终都能够保证前置条件不满足的话就不执行代码。任何需要条件检查的情况，都可以使用上面提到的断言系统。

在部署了这个新的模型之后，我跟高兴曾经误用了“weak”和“strong”的人都不再困惑了。强迫开发人员做出决定，有助于提高代码的质量。

未来的方向

当我们的项目结束的时候，很多领域都已经不同程度地有所成熟。

不变量（Invariants）

我们对不变量做了大量的尝试。每次我跟精通合约设计的人讨论问题的时候，他们对我们没有从一开始就使用不变量感到惊讶。老师说，我们的设计的确一开始就包括了这些内容，但我们没能有足够的时间来实现和部署这一功能。部分原因是工程人力的不足，但同时也是由于存在一些难以解决的问题。同时，团队几乎对前置条件、后置条件和断言非常满意。我甚至怀疑，随着时间的推移，我们已经完整实现了不变量，但如今仍有一些问题困扰着我。我得再多看一看它在实践中的应用。

我们的设计所提供的方法是，invaraint 是类型内部的一个成员。例如：

public class List<T> {
    private T[] array;
    private int count;
    private invariant index >= 0 && index < array.Length;
...
}

需要注意的是 invariant 标记为了 private。一个不变量的访问控制符表明了这个不变量需要检查的成员。例如，一个 public invaraint 只需要对 public 函数的入口和出口做出限制。这使得一些 private 函数能够临时的破坏不变量，只要其在 public 的入口和出口处仍然成立即可，这也是一种常见的模式。当然，就像上面的例子一样，一个类也可以声明一个 private invariant，这就要求所有的函数在进入和退出时都要满足不变量的条件。

我非常喜欢这种设计，我也认为它能够实现。一个主要的忧虑是我们在所有的地方都引入了一个隐式的检查。就算在今天，这也让我有点不安。例如在 List<T> 的例子中，这个类中的每一个函数的开始和结束的地方都需要插入 index >= 0 && index < array.Length 的检查。我们的编译器最终能够很好的识别并合并冗余的合约检查，并且在很多情况下合约都能够 显著 提高代码的质量。然而，在上面给出的极端例子中，我确信性能上会有所影响。这迫使我们考虑换一种不变量的检查策略，而这可能会使得整个合约模型变得复杂。

我真的希望我们能够有更多的时间，来更深入地探索不变量。我们的团队似乎并没有对这个功能非常期待——至少我们没有听到过抱怨没有不变量的声音（也许是因为整个团队特别看重性能问题）——但我确定的是，不变量肯定会为合约系统增色不少。

高级类型系统

我喜欢这种说法：合约是类型系统的补充。类型系统让你能够使用类型来对变量的属性进行定义，例如类型可以限制一个变量的值的范围。合约同样可以检查变量的值的范围。那么区别在哪呢？在编译时，严格的、可组合的归纳规则确保了类型的正确性。在检查局部的函数时，这些规则通常不会太耗时，同时还会有开发人员提供的标注作为帮助（不过也可能没有）。而合约则是：尽可能的在编译期证明合约的正确性，如果证明不了的话，就在运行时检查。因此，合约不提供严格的规范，允许使用语言本身提供的任意逻辑进行声明。

类型总是首选，因为它们能够在编译期就提供保证，而且保证能够做到快速地检查。这种为开发人员提供的强有力的保证，有助于提高开发人员整体的生产力。

然而，类型系统不可避免地有一些限制；类型系统需要留出一定的回旋的余地，否则它们就会变得非常难用。极端的情况下，类型系统甚至会退化至位/字节级别的规定。即便如此，有两点“回旋的余地”始终让我很不爽，使得我们必须使用合约来解决：

  1. 是否可为空
  2. 数值范围

大约 90% 的合约会落入这两点当中。结果就是，我们认真探索了更加复杂的类型系统，以便能够使用类型系统（而不是合约）来判别是否为空、以及变量值的范围。

具体来说，下面这段代码使用了合约：

public virtual int Read(char[] buffer, int index, int count)
    requires buffer != null
    requires index >= 0
    requires count >= 0
    requires buffer.Length - index < count {
    ...
}

而下面这段代码则不需要，只利用编译期的静态检查就能够得到同样的保证：

public virtual int Read(char[] buffer) {
    ...
}

将这些属性放入类型系统能够大幅度减轻错误检查的负担。举个例子，对于某个状态来说，它有 1 个生产者、10 个消费者。与其在 10 个消费者那里对状态进行检查，我们可以做到把检查放到生产者那里——比如加上一句强制的类型断言，或者更好的做法是一开始就把值存进正确的类型中。

非空类型

第一点其实有点难办：静态地保证一个变量不会为 null 值。这就是 Tony Hoare （译注：就是上文提到的 C. Hoare）所说的著名的“billion dollar mistake”。对任何语言来说，想办法解决这个问题都是一个非常合理的目标。现在很多新语言的设计师都决定直面这个问题，我非常高兴。

一门语言的很多方面都会阻碍我们实现这一特性，泛型、零值初始化、构造函数，等等。把非空类型添加进一门现有的语言真的很难！

类型系统

简单来说，非空类型可以简单归纳为类型系统的一些规则：

  1. 所有不加装饰的类型 T 默认都是非空的
  2. 所有添加了 ? 的类型，例如 T?，都是可空的
  3. 对于非空类型来说，null 是不合法的值
  4. T 能够隐式转换为 T?。换句话说，T 是 T? 的一个子类型（尽管不完全对）
  5. 存在从 T? 到 T 的显式转换，运行时需要检查是否为空，如果为空则触发放弃

这其中的大部分似乎都“显而易见”，我们没有太多的选择。根据类型名称的不同，类型系统能够知道 null 的所有路径。具体来说，一个 null 永远不能偷偷地变成一个非空类型 T；这就意味着我们需要零值初始化，也许这才是所有问题当中最难的一个。

语法

我们提供了几种将 T? 转换为 T 的语法，用来实现第 5 条规则。当然，我们不建议做这种转换，而是更希望你能够尽可能地使用非空的类型。但有时候确实是需要做转换的。多阶段初始化很常见，尤其是容器类的数据结构，因此还是需要支持这种转换。

考虑一下，假如我们有一个 map：

Map<int, Customer> customers = ...;

这一句构造语句告诉我们：

  1. Map 自身不为 null
  2. Map 当中的 int 键不会为 null
  3. Map 当中的 Customer 值也不会为 null

假设我们在索引函数中，使用 null 来表示某个键不存在的情况：

public TValue? this[TKey key] {
    get { ... }
}

那么现在我们需要在调用处检查一下索引是否成功。我们讨论了很多种语法。

最简单的方法是加上一个检查来做保护：

Customer? customer = customers[id];
if (customer != null) {
    // 此处的 `customer` 变为非空类型 `Customer`
}

我承认，我总是对神奇的隐式转换持怀疑态度。当出现问题的时候，很难发现到底是哪里不对。例如，当你试图将 c（译注：应为 customer）跟一个值为 null 的变量进行比较的时候，就会出现问题。不过，这种语法很好记，而且通常情况下都没问题。

当值确实为 null 时，这种语法就会执行另一条分支。但有时你只是像简单地做一次断言，如果值为空则触发放弃。显式类型断言操作符能够实现这样的操作：

Customer? maybeCustomer = customers[id];
Customer customer = notnull(maybeCustomer);

notnull 操作符将任意的 T? 类型的表达式转换为 T 类型。

泛型

泛型有点复杂，因为有多级的可空性需要考虑。考虑下面的代码：

class C {
    public T M<T>();
    public T? N<T>();
}

var a = C.M<object>();
var b = C.M<object?>();
var c = C.N<object>();
var d = C.N<object?>();

一个很基本的问题是：a、b、c 和 d 的类型是什么？

一开始我们走了点弯路，主要是因为我们当时在模仿 C# 中的 nullable，但其实 C# 的 nullable 有点特别。好消息是，我们最终找到了自己的方法，虽然花了点时间。举个例子来说明我想表达的意思，关于这个问题的答案，现在有两大阵营：

  • .NET 阵营：a 是 object；b、c 和 d 是 object?
  • 函数式语言阵营：a 是 object；b 和 c 是 object?；d 是 object??

换句话说，.NET 阵营认为你应该把所有的 ? 压缩成一个。而理解了数学组合之美的函数式阵营，则选择不使用任何神奇的操作，让这个世界该怎么样就怎么样。我们最终意识到，.NET 的方法出奇的复杂，同时还需要运行时支持。

函数式语言的方法确实会让人一时摸不着头脑。例如，前面举的 map 的例子：

Map<int, Customer?> customers = ...;
Customer?? customer = customers[id];
if (customer != null) {
    // 请注意, `customer` 在此处为 `Customer?`，仍然可能为 `null`！
}

在这个模型中，每次只能剥掉一次 ?。但说实话，如果停下来想想，就会发现这其实很有道理。它更加透明，准确地表达了究竟发生了什么事。我们最好不要逆势而为。

此外，在实现上还有问题需要考虑。最简单的实现方法是把 T? 扩展为某些“wrapper”类型，比如Maybe<T>，然后插入合适的 wrap 和 unwrap 操作。确实，这似乎是一个合理的实现方法。但有这个模型存在两点问题。

第一点问题是，对于引用类型 T 来说，T? 不能浪费不必要的空间——一个指针的运行时表示已经能够包括 null 了。作为一门系统语言，我们希望能把 T? 和 T 实现得一样高效。这可以简单地通过特化泛型的实例化来解决。但这意味着非空类型不再只是简单的前端问题，变为需要编译器后端支持。（需要注意的是，这种解决方案难以扩展至 T??）

第二点是， 由于有可变型（Mutability）的标注，Midori 支持安全协变（safe covariant）数组。如果 T和T? 有着不同的物理表示，那么从 T[] 到 T?[] 就不是一种转换操作了。这其实只是个小瑕疵，特别是当你堵住了协变数组的安全漏洞之后，协变数组就不再那么有用了。

不管怎样，我们最后放弃了 .NET Nullable<T> 这条路，转而使用了组合性更强的多个 ? 的设计。

零值初始化

零值初始化是一个真正的难题。它需要：

  • 一个类的所有非空域（field）都需要在构造时初始化
  • 一个非空类型的数组中的所有成员需要在构造时全部初始化

但这还不是最糟糕的。在 .NET 中，所有的值类型（value types）都是隐式零值初始化的。因此最基本的规则就是:

一个 struct 的所有域必须是可空的

绝望的气息。这几乎把整个系统都污染了。我的假设是，只有当可空类型不常用时（比如 20% 的使用率），不可空性才会真正有用。这条规则立刻就毁了一切。

所以我们开始了去除自动零值初始化的工作，工作量非常大。（C# 6 则选择了允许 struct 提供自己的零值初始化构造函数，但由于对整个生态系统的影响太大而不得不放弃。）非空类型本来是能够成功的，但我们有点偏离了跑道、分了心，进而引出了别的问题。如果我能再重来一次，我只需要将 C# 中的值类型和引用类型统一起来就够了。在我下一篇文章——垃圾回收的斗争之路中，这方面的原因将会有更清楚的解释。

非空类型的命运

我们有坚实的设计、实现了几个原型，但从来没有在整个操作系统层面部署这个功能。原因与我们所期望的 C# 兼容性有关。公平地说，我在这件事上犹豫了很久，最终就做出了这样的决定。在 Midori 的早期，我们希望人们一见到它就觉得很熟悉；后来，我们甚至在考虑，是不是所有的功能都能够作为 C# 的附加扩展来实现。正是这种想法阻碍了非空类型的实现。如今我相信，仅仅添加一些标注是无法成功的——Spec# 已经这么尝试过了！而且空和非空的默认选择应该倒过来——非空值必须得是默认实现，它才能够达到我们想要的效果。

我最大的遗憾之一就是没能尽早着手非空类型的工作。我们在开始大规模应用合约之后才开始非空类型的探索——因为我们发现代码中充斥着成千上万个 requires x != null。虽然它很复杂、代价很高，但如果同时把去除值类型也实现的话，它们俩绝对是个超赞的组合。真的是要活到老学到老啊！

如果我们把我们的语言从 C# 独立出来单独发布，我相信我们能做的更好。

范围类型

我们设计过向 C# 中添加范围类型，但它的复杂度总是刚好高过我能接受的程度。

基本的想法是，每一个数值类型都可以接受一个下界类型参数和一个上界类型参数。例如，你能够表达出一个整型只能存放 0 到 1000000 之间的整数。例如声明为 int<0..1000000>。当然，这其实代表你应该使用一个 uint，编译器应该能够给出警告。实际上，所有的整型都可以根据这个概念进行表示：

typedef byte number<0..256>;
typedef sbyte number<-128..128>;
typedef short number<-32768..32768>;
typedef ushort number<0..65536>;
typedef int number<-2147483648..2147483648>;
typedef uint number<0..4294967295>;
// ...

真正帅爆了（但同时极度复杂）的是，我们可以进而使用依赖类型来允许符号范围参数。例如，我有一个数组，并且希望传入的索引能够保证在某个范围之内。通常来说我会写：

T Get(T[] array, int index)
        requires index >= 0 && index < array.Length {
    return array[index];
}

或者我可以使用 uint 来替代前半部分的检查：

T Get(T[] array, uint index)
        index < array.Length {
    return array[index];
}

如果有了范围类型，我就可以把索引的上界跟数组的长度直接绑定起来：

T Get(T[] array, number<0, array.Length> index) {
    return array[index];
}

当然，如果你破坏了编译器的别名检查，边界检查可能就会在运行时进行了。但我们希望至少它能跟合约检查的代价相当。必须要承认，这种方法就是对类型系统中的信息进行更直接的操作。

不管怎样，我还是觉得这个主意太酷了。不过它仍然是“有它更好，没有也不强求”的那一类功能。“不强求”的原因在于，在我们的类型系统中，切片（slice）是一等公民。我打赌，在三分之二甚至更多的情况下，切片是比范围检查更合适的写法。我认为大多数人还是习惯于使用范围检查，因此他们还是写出了标准的 C# 写法，而不是使用切片。我会在之后的文章中介绍切片，在大多数情况下，它确实能够替代范围检查。