原文标题：Safe and Efficient, Now
作者：Oleg Kiselyov
原文地址：Lightweight Static Guarantees
本文确立了一种严谨的编程风格（事实上，十多年前就有人确立过）。这一风格通过利用成熟的、实用的语言（如 OCaml、Scala、Haskell 等，某种程度上 Java 和 C++ 也可纳入这一范畴）中的现有类型系统，从而静态地保障一系列广泛的安全性质。
永远不会对空指针解引用，或取空列表的头部元素。
始终对用户提供的输入进行消毒。
只使用数组界内的索引值访问（动态分配的）数组，且数组大小不需要静态可知。
这一技术与模块化开发、分离编译、命令式编程、原生的可变数组、间接索引以及一般递归等编程语言特性兼容。使用这种技术编写的程序所需的运行时检查更少，因此不但更可靠，而且更高效。这一技术并非旨在取代基础的代码形式化验证方法，而是补充并结构化了这种方法：我们可以用形式化方法证明（小而简单的）安全内核的正确性，然后用这一技术将安全内核的静态保障从内核扩展到整个程序。
在研究的过程中，我们发现有两个点令人惊讶：首先，我们上面所列举的内容居然是可行的；其次，这些技术是如此古老（可追溯到 Morris 1973 年的论文），如此简单，但却鲜为人知。
导言
OpenSSL 的心血［Heartbleed］漏洞给人们带来的惨痛回忆已逐渐淡去——毕竟，可被利用的安全漏洞常常都有。但心血漏洞仍然令人瞩目，因为漏洞本身是如此的微不足道，人们却花费了大量精力来修复它的影响。
与许多其他的此类性质的漏洞一样，心血漏洞的出现并未经过太多的酝酿——正如 SSL 的心跳［heartbeat］功能开发者所解释：「我当时正在改进 OpenSSL，提交了大量的漏洞修复，并添加了一些新功能。不幸的是，在其中一个新功能中，我漏了验证某带长度的变量的长度。」而 OpenSSL 的代码审核——「显然也没有注意到这一遗漏。」这位开发者又补充道：「因此这个漏洞从开发分支进入了发布版本。」最终在发布版本中潜藏了两年，一直未被（公开）发现。
最终修复这一漏洞的 OpenSSL 补丁证明：这一漏洞本身确实微不足道，不过是一条语句
memcpy(bp, pl, payload);
这条语句从输入数据包（自指针 pl 开始）中拷贝 payload 大小的数据载荷，然后将拷贝出来的内容放入输出数据包缓冲（自指针 bp 开始）。payload 值是从之前的输入数据包中读取的，当恶意攻击者发送的数据包声明它的载荷量是最大有效值，但实际却没有携带任何数据载荷时，问题就来了：在这种情况下 memcpy 没法从接受到的数据包中拷贝（因为已经结束），反而是从 OpenSSL 输入缓冲区的剩余垃圾中拷贝数据。这些「垃圾」实际上是之前剩余的数据，通常包含密码等敏感信息。
另一个令人不安的点在于：如果禁止程序员直接使用 memcpy 这样的低级函数，而是强制其通过一些封装（例如强制检查 pl + payload 地址是否仍在输入数据包内）来调用，像心血漏洞这样的问题本来很容易避免（因为输入数据包的边界很容易获得）。这种调用限制可以在任何具有模块［module］或命名空间［namespace］抽象机制的语言（C++ 等）中实现，甚至也可以在 C 语言中实现：
「抽象」就是关键所在：通过对内部数据和函数的抽象，迫使程序员使用带有安全检查的公开 API。抽象还能通过「避免外部程序污染内部状态」，从而确保一些已经通过安全检查验证的不变式［invariant］在任何情况下都成立——这样，就不必反复地进行某些安全检查了，甚至可以完全不需要检查。因此我们的口号是：「安全和高效，我全都要。」
这编程风格背后的思想其实稀松平常，甚至可以追溯到计算机的洪荒年代：由硬件保障的内存和设备的访问限制。硬件保护层将计算系统分为（受信任的）内核（在特权模式下运行，可执行底层操作）和用户态［user-level］程序，后者只能通过内核公开的 API（系统调用）访问设备，而内核 API（系统调用）会检查正确性和访问权限。譬如，用户态程序不能随意写入磁盘，它们只能执行 open 系统调用；在经过权限和一系列检查后，系统调用返回一个不透明的标记，即文件描述符［file descriptor］。这一描述符代表了「执行规定的的操作的能力［capability］」，还代表了一种「授权成功」的事实，在进一步的操作中就无需重复验证授权。Jame Morris 1973 年发表的论文 «Protection in Programming Language» 首次将操作系统中的部分理念应用到软件开发中，这些理念包括内存保护、身份验证、整理、作用域控制等等。该论文还展示了软件/语言的保护层是如何帮助我们对程序进行本地化、模块化的推理。而自 1973 年以来，编程语言中的抽象设施变得更加广泛和普及，现在是时候充分利用 Morris 的这一洞见了。
我们现在就可以用现有的、成熟的编程语言做到：
只解引用非空指针。
只把非零数字作为除数。
只取非空链表的头部或尾部。
当访问某静态缓冲区的内容时，仅使用在范围内的索引才能访问。
执行 SQL 指令时，指令不会包含来自外部输入且未经消毒的字符串。
这些功能在 C++ 和 Java 中就已经可以实现，后面我们将举例说明。
我们能做的远远不止这些。通过使用现代语言中的泛型编程设施（参数化多态）或高级模块系统，我们可以保障更多的安全性质。例如，我们可以对一个只有在运行时才知道大小的数组进行安全的索引访问。我们甚至还会展示一个静态确保了不会出现缓冲溢出问题的 KMP 字符串搜索，这是一个命令式的复杂算法，使用了间接索引这样的特性。
Morris 的老方法在现在仍能大放异彩，为什么我们不用呢？
参考资料
- Heartbleed developer explains OpenSSL mistake that put Web at risk
令人吃惊的一点在于：人们在网上找到的许多关于这一问题的「解释」都是有问题的，这些解释错误地将漏洞归因于 OPENSSL_malloc。
修复「心血」漏洞的 OpenSSL 补丁（从 OpenSSL 1.0.1f 更新到 1.0.1g）
「心血」漏洞利用原理。
用户输入净化与 SQL 注入问题
「心血」问题只是忽略了对用户或网络输入数据进行消毒的一个例子。另一个同样不幸的例子则是用户输入注入攻击，其中最为瞩目的就是 SQL 注入：「Bobby Tables」 式攻击。我已经在生产环境中的网络应用程序服务器中实施了静态 SQL 注入保护，实现本身简单明了，而且很有启发性。
我曾经写过一个网络应用程序服务器，它在生产环境中持续运行了至少八年。服务器会使用用户提交的请求数据来执行 SQL 查询，因此我必须关注用户输入验证和 SQL 注入问题。在开发到一半时，我决定尝试上文提及的「软件保护层」想法：利用类型检查程序提醒我某些地方忘记验证外界输入。
这个想法本身其实很容易尝试，不过下面缪缪数行（示例代码使用了 OCaml，也可以使用 C++、Java、Scala 或其他语言）。
module DirtyString : sig (* 接口 *)
type dirty_string (* 抽象 *)
val dirty : string -> dirty_string
val escape : dirty_string -> string
val read_int : dirty_string -> int option
val read_ncname : dirty_string -> (string * dirty_string) option
end = struct (* 实现 *)
type dirty_string = string
let dirty = %identity
let read_int = int_of_string_opt
...
end
dirty 方法会「污染」其输入参数，将其变为抽象 dirty_string 类型的值。一旦字符串被污染了，我们就没法对它做什么了：只能对其应用 escape、read_int 和 read_ncname 方法。最后一个方法会尝试从受污染的字符串中读取一串由字母和数字构成的「安全」字符串，然后将读取出的内容和剩余的脏字符串配对返回；这样返回的字符串是「干净」的，在构建 SQL 查询时可以放心使用。
而在 DirtyString 的具体实现，即「内核」中，dirty_string 只是普通字符串。同理，read_int 方法也不过就是 OCaml 标准库中的对应函数，把模块内联后就没有任何运行时开销。但保护措施仍然存在：对于库的用户而言，dirty_string 和 string 类型不同，不能随意互换使用。
而当我写完这个 DirtyString 库之后，我就把网络读取函数返回的字符串全部「污染」了，然后重新编译程序，并观察编译器提出的类型错误。代码中所有使用了用户输入的地方都被类型检查程序标记了出来：dirty_string 不能用作普通字符串——确实，我们需要对这些输入进行验证/净化。因为我已经实现了这种验证，要修复这些错误也很简单，只需把对 read_ncname 函数的调用重命名为 DirtyString.read_ncname 等。
我还清楚地记得：有一处代码被类型检查程序标记了出来，但是那里却没有任何验证检查。在思考了大约十分钟后，我决定在那个地方插入验证。
事实证明，这次重构的经历非常令人鼓舞。实现 DirtyString 和调整相应代码总共不过花了一个小时的时间，但在此过程中却发现并解决了一个真正的问题。而且，我也没有发现重构引入了运行时开销。
引用文献
宝妈也疯狂（又名「Bobby Tables」）
类似的「污染」技术有助于防止出现「尝试取空列表的 head/tail」类错误（等价于 NullPointerException）
通过「安全列表访问」技术实现反转非空列表的 OCaml 代码
抽象类型——语言保护层
让我们通过一系列简单但有用的例子来解释「抽象」是如何充当保护层这一角色的，它保障了代码执行中的哪些不变式，它对我们有什么好处。
假设我们有几个（假定为常数个）整数数组 a1...an，我们需要反复搜索其中某些元素的出现次数。一个合理的做法是：对这些数组排序得到 a1'...an'，然后利用高效的二分搜索来进行搜索。但这种做法也存在一些问题，首先，如何保障 ai' 的确是原始数组 ai 的排序后版本？数组本质上可变，当我们把 ai' 作为参数传递给某个函数时，无法确保它不会被修改（除非我们仔细检查函数的代码，而且还是在有代码的情况下才可行）。
而更主要的问题在于：二分搜索函数如何确定其参数数组确实经过排序了？在执行查找前先检查数组是否经过排序是不可行的，这会比实际搜索要花费更多的时间。
保护，或者说访问限制就提供了这种「已排序」的保证。请看下面这个以 OCaml 模块形式实现的简单库。
module ArraySearch : sig (* 接口 *)
type t (* 抽象 *)
val sort : int array -> t
val search : int -> t -> bool
end = struct (* 实现：「内核」 *)
type t = int array
let sort : int array -> t = fun a ->
let a' = Array.copy a in
Array.sort compare a'; a'
(* 对排序过的数组执行二分搜索 *)
let search x arr = ...
end
在几乎任何具有模块系统的语言中都可以写出类似的代码（稍后我们也会展示一种利用闭包/对象的实现方法）。该库只提供了两种操作：sort 和 search，前者接收一个整数数组，返回类型为 t 的值。库的用户对 t 的具体类型一无所知，尤其是，用户不能对 t 类型的值进行数组访问或修改：如果用户这么做，类型检查器就会抱怨说 t 不是数组。事实上，t 不等同于任何类型检查器已知的类型，因此只能把 t 类型的值交给多态函数（这些函数能做的就只是传递这些值）或库中的 search 操作。下面是一个使用例（假设我们有 a1 和 a2 两个数组）：
let a1' = ArraySearch.sort a1 (* 首先排序数组 *)
let a2' = ArraySearch.sort a2
... (* 如此 *)
let v1 = ArraySearch.search 1 a1' && ArraySearch.search 2 a2'
... (* 这般 *)
let f x = ArraySearch.search x a1' in
f 1 && f 2
这里也可以先 open ArraySearch，这样就可以省略重复的 ArraySearch 前缀。
研究库的实现（ArraySearch 结构）就可以发现 t 类型实际上是 int array——但这一点只有实现的内部才知道。因此，实现可以将 t 值视为数组，类型检查程序也不会对此有意见。sort 会复制数组然后对复制品进行排序，并不会修改输入参数数组；因此我们可以断定：t 类型的值代表了某个由 sort 排序好的数组，也没有能逃逸出实现的别名，以及对 t 进行的操作会维持它的排序性质。
我们只需观察模块的实现，无需观察任何使用这一模块的用户代码，就能做出这样的判断。因为使用模块的用户无法知道 t 具体代表什么，也无法对其应用 ArraySearch.search 以外的操作，所以与 t 相关的「列表已经过排序」性质显然总是成立。类型抽象，或者说由类型检查器保障的访问限制的优点正是在于此：通过局部推理建立的性质或不变式，在全局范围内也成立。在我们的例子中，「已排序」性质意味着 search 操作无需检查其参数是否为排序过的数组，因为它的参数总是已经排序好的数组。类型抽象有助于我们多快好省地运用算法。
在进入第二个例子前，我们先看看另一种实现已排序数组搜索库的方法。这一方法利用了另一种语言保护机制。
let sort : int array -> (int -> bool) = fun a ->
let a' = Array.copy a in
let () = Array.sort compare a' in
(* 对排序过的数组执行二分搜索 *)
let search x arr = ... in
fun x -> search x a'
这里的 sort 以 int array 为参数，返回一个在该数组中（高效）搜索的操作。我们现在利用头等函数这一抽象机制：将函数作为结果返回。其中最重要的一点在于，返回的函数 fun x -> search x a' 其实是一个闭包，包含了对内部数组 a' 的引用。闭包是不透明的结构，无法被解开，因此其中包含的 a' 引用无法在闭包外使用或查看。不难注意到：库用户无法获得其他的 a' 引用；因此一旦排序过后，a' 会维持在已排序的状态保持不变。我们再次看到了局部的推理（只检查实现，不检查库的使用侧）和「局部不变式在全局下都有效」这一点保证给我们带来的保护。
顺带一提，闭包实现类似于 Morris 1973 年论文中的实现（虽然他使用的具体例子有所不同，但是他也提到了数组排序和二分搜索）。创建和使用闭包都会产生开销，而 ArraySearch 模块则完全没有运行时开销：在模块内部，t 类型的值就是一个 int array，不存在封装或间接访问。
下一个例子是包含了四个操作的模块（库），如下所示：
module Interv : sig (* 接口 *)
type t (* 抽象 *)
val lwb : t
val upb : t
val mid : t -> t -> t
val to_int : t -> int
end = struct (* 实现：「内核」 *)
type t = int
let lwb = 0
let upb = 5
let mid x y = (x + y) / 2 (* 对于我们的例子而言，不可能出现溢出 *)
let to_int x = x
end
我们以 OCaml 为例，但也可以用任意面向对象语言写成带有 protected 字段访问限制的类。
通过观察实现，我们可以得出这样的结论：抽象类型 Interv.t 满足不变式「它只表达 0 到 5 （包括两端）的整数」。具体而言：lwb 返回 0，显然满足；同理，upb 返回 5，也满足。mid 操作会消费 t 值，也会生产 t 值；作为消费者，它可以假定 t 满足上述不变式；利用这一假设，我们可以推断 mid 的结果也是同一范围内的数字。因此，不变式成立，to_int 操作的结果显然是 0 到 5 间的整数（包括两端）。这种保证是安全数组索引的基础，下文会对此进行详细介绍。
总之，语言保护层有助于在全局范围内保留局部推理建立的不变式。具体来说，类型抽象有助于我们将某条不变式（命题）附加到某个抽象类型的值上：例如，让该值代表某个范围内的数字或者已排序的数组。Robin Milner 早在 20 世纪 70 年代初设计 Edinburgh LCF 定理证明器时就提出了「利用抽象数据类型静态表示和强制保障运行时值的复杂性质」的想法。
迄今为止进行的局部推理都没有形式化，但我们可以将这些推理形式化到任意想要的程度。事实上，抽象保护层可以通过局部化和模块化来协助形式推理：对 Interv 接口的实现进行形式分析显然要比对使用该接口的整个程序进行形式分析要容易得多。
必须指出的是：抽象类型提供的保障也在于语言不支持抽象数据类型进行反射［reflect］、扩展［extension］、以及探查［introspection］等功能。顺带一提，OCaml 对此提供的保障其实比较弱，因为多态相等［polymorphic equality］判断函数1会破坏某些不变式。从这一角度来看，语言提供的反射、扩展和探查等功能可能是一种缺点，而非是优点。
引用文献
- James H. Morris Jr.: Protection in Programming Languages
摘要：本文描述了一种可用于「保护一个子程序不受另一个子程序的故障产生的影响」的语言机制。文中考虑了包括「生产函数的函数」以及几种类型标签方法，并提出了一种区分「访问限制」和「身份验证」的尝试。出自 Comm. of the ACM, 1973, V16, N1, pp. 15-21。
消除数组边界检查
现在，我们将详细介绍语言保护层如何帮助确保「所有数组索引操作都在范围内」。我们不仅可以确信程序的任何部分都不会出现越界访问（或者说缓冲区溢出），还消除了动态的数组边界检查，从而提高了程序性能。让我们看看「安全高效，我全都要」的口号是如何在现实的有趣程序中发挥作用的。
本节要呈现的例子其实是一种在已排序数组中进行二分搜索的算法，即奚宏伟与 Pfenning 的著名 PLDI 1998 论文中描述的例子，后面将还会有更多涉及二分搜索的例子。虽然这些代码最早（2004 年）是使用 Haskell 编写的，但这里将使用 OCaml；要用 Scala 或 Java 重新实现之也很容易，我们已经用 C++ 实现了一个比较简单的版本（见章节末的引用文献）。
考虑一个上文提出的 Interv 接口的扩展版本：
module type Index = sig
type index = private int (* i:index => lwb <= i <= upb *)
type indexL = private int (* i:indexL => lwb <= i *)
type indexH = private int (* i:indexH => i <= upb *)
val lwb : indexL
val upb : indexH
val bsucc : index -> indexL
val bpred : index -> indexH
val bmid : index -> index -> index
val bcmp : indexL -> indexH -> (index * index) option
end
Index 接口展示了 OCaml 的另一种抽象机制：所谓「私有」类型2。private int 类型的值总是可以被转换为 int，然后作为普通整数使用——事实上，在运行时 private int 就是 int，优化器也可以看到这一点并进行相应的优化。另一方面，int 不能转换成 private int，在预期是 private int 的场合使用 int 会产生类型操作。唯一创建 private int 类型值的方法是使用接口所提供的操作。
Index 接口上有三个不同的抽象类型：试举一例，bsucc lwb 会导致类型错误。代码间的注释说明了不同抽象类型所蕴含的命题：如果 i 是 index 类型的值，那么它就是闭区间 [lwb,upb] 内的整数（index 类型的值同样也证明了 lwb <= upb）。相反的是，indexL 类型值只保障它大于下界 lwb，indexH 类型的值只保障它小于上界 upb。bsucc 代表递增某个索引，虽然它的返回值可能会溢出 upb，但必定是在 lwb 之上，因此应该返回 indexL 类型；而 bpred 操作则是求索引值的前继数（这样的数也显然必定小于同样的下界）；bmid 操作能求两个在范围内的索引的平均值，结果显然也在范围之内——它的类型就证明了这一点。
最后，bcmp 可以比较两个索引：已知 i: indexL 必然大于下界 lwb，j: indexH 必然小于上界 upb。如果 i<=j，那么 i 和 j 显然都在区间 [lwb,upb] 内，那么函数就应该将它俩作为 index 类型值返回。因此，比较结果不仅代表简单的真或假，一次成功的比较可以更新我们对值的性质的认识，从而有权使用更精确的类型。
下面则是一种直观的接口实现，参数 upb 可以为任意整数，而下界则假定为 0。这一实现就遵守了我们刚才描述的接口不变式，读者自行观察不难。
module IndexF(S:sig val upb:int end) : Index = struct
type index = int
type indexL = int
type indexH = int
let lwb : indexL = 0
let upb : indexH = S.upb
let bsucc : index -> indexL = Stdlib.succ
let bpred : index -> indexH = Stdlib.pred
let bmid : index -> index -> index = fun x y -> x + (y - x)/2
let[@inline] bcmp : indexL -> indexH -> (index * index) option = fun i j ->
if i <= j then Some (i,j) else None
end
在实现内，index, indexL 和 indexH 类型不再私有，可以随意创建这些类型的值，签名 Index 中的私有修饰符负责保证相关的访问限制。而令人感到奇妙深刻的 [@inline] 则是一种内联指令，类似于 C/C++ 中的 inline 关键字。
现在我们知道 index 类型的值总是在 [lwb,upb] 区间内，这样就可以利用其对索引范围同为 [lwb,upb] 的数组进行安全访问。由于我们静态检查了这一安全保证，可以忽略运行时的动态边界检查：
module BArray(S: sig type el val arr : el array end) = struct
include IndexF(struct let upb = Array.length S.arr - 1 end)
let[@inline] bget : index -> S.el =
fun i -> Array.unsafe_get S.arr (i :> int)
end
设 a1 为一整数数组，那么 BArray(struct type el = int let arr = a1 end) 就是一个实现了 Index 接口的模块，此外还附带了一个 bget 操作，用于对数组 a1 进行索引（操作 (i :> int) 会把 index 类型强制［coercion］为 int，这样做始终合法，而且本质上就是把一个值原封不动地返回）。实例化 IndexF 后，lwb 为 0，upb 为 a1 的长度减 1——如果 a1 非空的话，这对上下界就代表了 a1 的索引范围，因此使用 unsafe_get 是合理的（如果 a1 是空数组，使用 unsafe_get 仍然合理，因为这时候 index 类型中没有任何值）。
现在我们已经实现了可信的「安全内核」，它提供了 Index API 以及额外的 bget 方法。这样就可以开始写二分搜索算法本身了：该算法接受一个比较操作 cmp、用于搜索的 key，以及一个数组，如果数组中没有 key，那么就返回 None；反之返回 Some (i,key)，其中 i 代表出现 key 出现位置的索引值。算法会假定数组已经使用 cmp 排序过。这一 bsearch 搜索接口借鉴自奚宏伟与 Pfenning 在 1998 年发布的 PLDI 论文。
let bsearch (type a) : (a*a -> int) -> a -> a array -> (int * a) option =
fun cmp key arr ->
let module M = BArray(struct type el = a let arr = arr end) in
let open M in
let rec look (lo:indexL) (hi:indexH) = (* 类型标注只是为了清楚起见 *)
match bcmp lo hi with
| None -> None
| Some (lo',hi') -> (* lo' and hi' are of the type index now *)
let m = bmid lo' hi' in
let x = bget m in
let cmp_r = cmp (key,x) in
if cmp_r < 0 then look lo (bpred m)
else if cmp_r = 0 then Some ((m :> int), x)
else look (bsucc m) hi
in
look lwb upb
这一实现不但非常的教科书式，而且与奚宏伟与 Pfenning 提供的代码十分吻合：只不过他们用 Dependent ML 写，而我们用普通 OCaml 写。关键部分在于 bcmp lo hi：这一函数会比较 lo（下界为 0）与 hi（上界为 upb，代表数组中的最大索引值），如果 lo 小于等于 hi，那么 [lo,hi] 区间非空，且是 [0,upb] （安全索引范围）的子集。
bsearch 代码本身不属于可信安全内核的一部分，我们可以称其为「用户态」代码。编写它需要使用 BArray 模块的接口（并实例化模块），它能受益于该接口所持有的不变式：接口保证了利用这一接口对数组进行索引总是安全。如果我们用 ocamlopt -O3 编译 bsearch 代码，并查看生成的汇编，就会发现所有数组访问和索引计算都被内联了，不存在数组边界检查，也没有调用报错函数。确实做到了安全和高效全都要。
bsearch 代码有很多种变体，下面的参考文献中就展示了几种。在这些变体中，有一个变化值得我们注意，这一变化与我们上面没有强调的 BArray 的功能有关。
BArray 保证了用索引访问动态数组是安全的。但仔细想想就可能会感到不可思议：类型是在程序运行前静态检查的，而具体的边界只有在运行时才能知道，我们怎么可能用类型来确保索引总是在边界内呢？下面的例子就解释了这一点，先设置初始环境：
let a1 = [|1;3|] and a2 = [|1;3|]
module M1 = BArray(struct type el=int let arr=a1 end)
module M2 = BArray(struct type el=int let arr=a2 end)
求值下述表达式
(M1.lwb :> int);;
- : M1.indexL = 0
M1.bget M1.lwb;;
^^^^^^
Error: This expression has type M1.indexL
but an expression was expected of type M1.index
会产生类型错误。读者可能会对此感到疑惑：「为什么不能用 0 建立数组索引呢？」答案是因为数组可能为空，所以这样的操作并不总是安全。在 Index 接口中，M1.lwb 的类型是 indexL，而非 bget 所期望的 index。想要获得 index 0 的唯一方法是将 lwb 与 upb 进行比较，相当于判定一次数组非空，而类型则强制我们进行了这种判断：
match (M1.bcmp M1.lwb M1.upb, M2.bcmp M2.lwb M2.upb) with
(Some (l1,u1), Some (l2,u2)) -> (M1.bget l1, M2.bget l2);;
- : int * int = (1, 1)
然而，在求值下列代码后
match (M1.bcmp M1.lwb M1.upb, M2.bcmp M2.lwb M2.upb) with
(Some (l1,u1), Some (l2,u2)) -> ((l1:>int),(l2:>int));;
- : int * int = (0, 0)
match (M1.bcmp M1.lwb M1.upb, M2.bcmp M2.lwb M2.upb) with
(Some (l1,u1), Some (l2,u2)) -> M1.bget l2;;
^^
Error: This expression has type M2.index
but an expression was expected of type M1.index
我们已经判断过了两个数组非空，而且 l1 显然是数组 M1 内的索引，但又出现了类型错误！这是因为：虽然 l1 和 l2 都属于 index 类型，且都表示整数 0，但是只有 l1 可以在 M1 数组内索引。l1 和 l2 的类型本质上是不同的：它们分别是 M1.index 和 M2.index 类型的值，每个 BArray 模块的实例都会用不同的数组来创建了不同的，全新版本的 index 类型，这一类型只能在对应 BArray 实例中建立索引。
某种意义上，也可以说 BArray 的实例为其抽象类型建立了一个独特的「信物」，抽象类型只有持有相同信物的模块中使用（这不会导致代码膨胀，因为优化器知道无论是持有什么样信物的 index 类型都不过是整数）。从技术上说，M1.index 和 M2.index 具有不同的路径［path］或出处（这一点很容易就能静态检查），类型检查器会认为它们是不同的类型。OCaml 的这一功能有点类似于 Scala 中的路径依赖类型［path-dependent type］3。
这种「信物」技术，虽然不能算是一种「简单类型」设施，但本身并不奇特，可以在任何具有存在量化类型［existential type］（或抽象包［abstract package］类型）或具有全称量化类型［universal type］的语言中实现。OCaml 中既有存在类型，也有全称类型，这样就产生了另外两种编写安全 bsearch 的方法。引用文献中的代码展示了在 OCaml 和 Haskell 中使用全称量化类型实现的方法。
版本
原始版本（Haskell 版）：二〇〇四年八月；改进后且带有详细解释的 OCaml 版本：二〇一九年八月。
引用文献
- Hongwei Xi and Frank Pfenning: Eliminating Array Bound Checking Through Dependent Types.
这篇著名的论文介绍了一种实用的依值类型系统，并将其作为一种 SML 方言。本文用多种语言忠实地复现了论文中的 bsearch 例子。
本文中使用的 OCaml 代码，内附基于全称类型的旧版信物实现。
bsearch 代码的 Haskell 版本，使用 Haskell 98+高阶类型扩展实现。
带有解释和示例的 Literate Haskell 代码（译文下附）。该文章的第一版最初以 «Eliminating Array Bound Checking through Non-dependent types» 为题，于二〇〇四年八月五日星期四 19:31:36 -0700 发布于 Haskell 邮件列表上。当前的版本修复了 Conor T. McBride 在讨论帖子中指出的问题。
在静态已知边界的数组中进行二分搜索的 C++ 代码。分为含模板和不含模板的版本，以及对应的生成的汇编代码（使用 gcc -O2 编译）。汇编代码证明了「确保数组访问安全」的抽象不存在运行时开销。
用另一个更简单的例子解释「信物」技术。
附件：eliminating-array-bound-check.lhs 翻译
有一种观点认为：为了获得诸如「保证数组索引始终在范围内」或「只对非空列表取 tail」的静态安全保证，我们必须放弃一些重要的东西——放弃数组等数据结构（使用嵌套元组替代）、放弃通用递归、放弃无类型标注编程风格、放弃代码的清晰整洁、放弃那些生态良好的语言……事实并非如此，本文展示了一个涉及原生 Haskell 数组、索引计算以及通用递归的非平凡案例。所有数组索引操作的安全性都有静态保障，可以使用 GHC 提供的高效 unsafeAt 操作。应用静态保障不会引入任何运行时开销，生成的代码也很高效。本示例只使用了 Haskell 98+高阶类型，甚至无需引入新的 typeclass。我们的安全性建构在 Haskell 类型系统、量化类型变量，以及一个紧凑的，通用的可信内核之上。
我们要关注的例子是 bsearch——这一例子来自奚宏伟与 Frank Pfenning 的著名论文 «Eliminating Array Bound Checking Through Dependent Types» (PLDI'98)。奚宏伟的代码是用带有受限形式的依值类型［dependent type］扩展 SML4 编写的。下面是原始代码（摘自该论文的图 3，这里还有更多示例）
datatype 'a answer = NONE | SOME of int * 'a
assert sub <| {n:nat, i:nat | i < n } 'a array(n) * int(i) -> 'a
assert length <| {n:nat} 'a array(n) -> int(n)
fun('a){size:nat}
bsearch cmp (key, arr) =
let
fun look(lo, hi) =
if hi >= lo then
let
val m = (hi + lo) div 2
val x = sub(arr, m)
in
case cmp(key, x) of
LESS => look(lo, m-1)
| EQUAL => (SOME(m, x))
| GREATER => look(m+1, hi)
end
else NONE
where look <|
{l:nat, h:int | 0 <= l <= size /\ 0 <= h+1 <= size } int(l) * int(h)
-> 'a answer
in
look (0, length arr - 1)
end
where bsearch <| ('a * 'a -> order) -> 'a * 'a array(size) -> 'a answer
<| 后面的文字是依值类型注释，这些注释必须由程序员手工指定，即便是类似于 look 的内部函数也如此。
下面则是我们的代码，编写这些代码时特意贴近了奚宏伟代码的风格（此消息本身为完整代码）。而在另一个文件 eliminating-array-bound-check-literally.hs 中，我们利用 Haskell 98+高阶类型，以一种更直白的方式翻译了相同的 bsearch 代码。
{-# OPTIONS -fglasgow-exts #-}
module Dep where
import Data.Array
bsearch cmp (key, arr)
= brand arr (\arrb -> bsearch' cmp (key, arrb)) Nothing
bsearch' cmp (key,(arr,lo,hi)) = look lo hi
where
look lo hi = let m = bmiddle lo hi
x = arr !. m
in case cmp (key,x) of
LT -> bpred lo m (look lo) Nothing
EQ -> Just (unbi m, x)
GT -> bsucc hi m (\m' -> look m' hi) Nothing
该算法的效率与奚宏伟使用的 Dependent ML 代码算法相同：每次迭代只需计算一次中间索引、比较一次元素、比较一次索引、进行一次索引递增或递减。而我们却不需要任何类型注释。(!.) 操作符是静态安全的索引操作符，类型系统和内核的可信性质保证了：对于表达式 arr !. m，索引 m 总是在数组 arr 的范围内。
barr1 = listArray (5,5 + (length s)-1) s where s = "abcdefgh"
btest1 = bsearch (uncurry compare) ('c',barr1)
btest2 = bsearch (uncurry compare) ('x',barr1)
btest3 = bsearch (uncurry compare) ('x',listArray (0,-10) [])
这一代码依赖于一个紧凑的，通用的可信内核，下文将对其进行详细解释。这个内核最好放在一个单独的模块中。
首先我们引入带「信物」的数组和索引
-- 该两类型 *禁止* 导出！
newtype BArray s i a = BArray (Array i a)
newtype BIndex s i = BIndex i
unbi (BIndex i) = i
它们都是 newtype 类型，不会产生运行时开销。其中值得注意的是幽灵类型变量 s，它携带了数组和数组索引的「信物」——若某索引肯定在具有相同信物的数组的范围内，那么它就是一个「已认证」的索引。s 类型变量有点类似于 ST monad 中使用的技术——后者也依靠于类似的 s 来保证序列化。我们并没有对 s 施加任何线性逻辑式的限制，用户可以自由地复制（见下文 bbounds）或丢弃（见 unbi）这些值。不过，s 必须在受控的条件下创建。
我们的安全保障依赖于「试图构造『信物』类型值的函数是可信的」这一点：BIndex 和 BArray 只能在可信内核中调用，禁止在其他任何地方使用。而显式的全称量化为 s 赋予了唯一性，从而避免用户将不同信物的类型混为一谈。这里必须再次重申：代码的安全性取决于「试图构造 BIndex 值的代码」所提供的保证。这种保证的级别很高，我们必须将这些安全性质表述为命题并加以证明。幸运的是，下面的代码十分简洁明了，而且具有通用性。
我们先讨论 BArray 类型的引入规则：
brand:: (Ix i, Integral i) => Array i e
-> (forall s. (BArray s i e, BIndex s i, BIndex s i) -> w)
-> w -> w
brand (a::Array i e) k kempty =
let (l,h) = bounds a
in if l <= h then k ((BArray a)::BArray () i e, BIndex l, BIndex h)
else kempty
该函数接受一个数组和两个延续［continuation］为参数：若数组为空（即下界大于其上界），则返回 kempty，否则调用延续 k。延续 k 以信物数组和两个信物索引为参数，两个索引分别代表数组的上界和下界。
命题. 对于任意延续 k 的任意参数 (a,l,h) ，信物索引 l 与 h 总在非空信物数组 a 的边界内。
证明. 利用函数 bounds 的语义（在此作为公理）和 brand 代码本身易证。 $\blacksquare{}$
brand 函数具有高阶类型——事实上，正是这里 s 类型的存在量化，以及「禁止在其他地方使用 BArray 构造函数」的约定共同保障了：同样的信物总是具有相同的边界。
bmiddle:: (Integral i) => BIndex s i -> BIndex s i -> BIndex s i
bmiddle (BIndex i1) (BIndex i2) = BIndex ((i1 + i2) `div` 2)
命题. l <= i1 <= h, l <= i2 <= h ⊢ l <= (i1 + i2)div2 <= h
证明. 简单算术可证。 $\blacksquare{}$
我们必须强调：bmiddle 类型确保所有相关的索引都具有相同的信物，即它们都有相同的上边界和下边界，信物 s （在类型级）表示了索引边界。虽然在编译时我们不知道它具体是什么，但 s 的不可伪造性从静态上保证了相同的 s 类型值代表了相同的边界。
bsucc:: (Integral i)
=> BIndex s i -> BIndex s i -> (BIndex s i -> r) -> r -> r
bsucc (BIndex upb) (BIndex i) on_within on_out
= let i' = i + 1
in if i' <= upb then (on_within (BIndex i')) else on_out
函数 bsucc 接受两个信物索引，两个索引都对应相同的边界（参见类型变量 s）。函数还接受两个延续 on_within 和 on_out。函数将第一个索引视为上界，然后递增第二个索引，如果结果没有超过上界，就将结果作为参数传给 on_within，否则调用 on_out。
命题. l <= upb <= h, l <= i <= h, (i+1) <= upb ⊢ l <= (i+1) <= h
证明. 由 i < (i+1) 和不等式的性质易证。 $\blacksquare{}$
这一安全命题成立证明了我们使用 BIndex 数据构造器的行为是正确的。
bpred:: (Integral i)
=> BIndex s i -> BIndex s i -> (BIndex s i -> r) -> r -> r
bpred (BIndex lwb) (BIndex i) on_within on_out
= let i' = i - 1
in if i' >= lwb then (on_within (BIndex i')) else on_out
bsucc 的对偶函数
命题. l <= lwb <= h, l <= i <= h, (i-1) >= lwb ⊢ l <= (i-1) <= h
因为信物索引总是在同一信物的数组的边界内，我们可以有
infixl 5 !.
(!.):: (Ix i) => BArray s i e -> (BIndex s i) -> e
(BArray a) !. (BIndex i) = a ! i
事实上，将这里的 a ! i 替换为 unsafeAt a i 也完全安全。