为什么 GADTs 对性能至关重要 (2015)

Why GADTs matter for performance (2015)

Source | HN Comments

文章探讨了 GADTs（广义代数数据类型）在 OCaml 编程中对性能的重要性。作者通过构建一个兼顾通用数组和 `bytes` 的紧凑数组类型为例，说明了 GADTs 如何帮助程序员更精确地控制内存表示，从而优化性能。文章对比了未使用 GADTs 和使用 GADTs 的两种实现方式，展示了 GADTs 如何解决类型推断问题，并最终实现更高效的内存管理，这对于构建高性能应用程序至关重要。

为什么 GADTs 对性能至关重要

2015年3月30日 | 阅读时间：9分钟

作者: Yaron Minsky

当 GADTs (Generalized Algebraic Data Types) 在 OCaml 中出现时，我并不是特别高兴。我认为这就像让编译器编写者设计你的编程语言时会出现的那种无稽之谈。也就是说，标准的 GADT 示例似乎都是关于编译器编写者所做的事情，比如嵌入特定领域的语言或构建类型化的抽象语法树。但这似乎与我所考虑的那种系统编程没有特别的关联。

但很快我就意识到我错了。特别是，自从 GADTs 出现以来，在 Jane Street，我们发现了很多 GADTs 对性能至关重要的例子。这些示例的主题是，GADTs 使你能够以某种方式调整你的内存表示，否则在 OCaml 中这样做会很痛苦或不可能安全地完成。

多态性的问题

我想通过一个简单的例子来说明 GADTs 的这个方面，但首先，关于 OCaml 的内存表示法的一些说明。 OCaml 的多态性在重要方面取决于内存表示。特别是，考虑一个简单的多态函数，如 List.iter，它具有以下类型：

val iter: 'a list -> f:('a -> unit) -> unit

多态类型告诉你 List.iter 可以在任何类型的列表上操作，在 OCaml 中，这是通过单个编译版本的代码来实现的。这是可能的，因为列表元素的内存表示是统一的：你总是可以在单个字中引用一个 OCaml 值，要么是指向堆分配值的指针，要么是适合该字内的立即数。

这意味着某些 OCaml 数据类型在空间上不如你想象的那么有效。例如，数组每个元素占用相同的空间量，无论这些元素是字节、32 位整数还是 64 位整数。（实际上，编译器中对浮点数组有一些特殊的技巧，但正如 Alain Frisch 在这里所描述的，这可能比它值得的麻烦更多。但现在让我们忽略浮点数组。）

OCaml 确实对字节数组有更紧凑的表示，称为 bytes。但它是一个完全不同的类型，因此构建一个通用数据结构，在有意义的时候使用 bytes，否则使用普通数组，这有点尴尬。

在没有 GADTs 的情况下控制内存表示

让我们看看如果我们尝试（在没有 GADTs 的情况下）设计一种数组类型，该类型有时使用通用数组表示，有时使用 bytes 会发生什么。

你可以想象使用普通变体来表示这样的值。

type 'a t = | Array of 'a array
      | Bytes of bytes

然后，我们可以实现我们对新数组类型所需的每个操作，并根据特定表示法以不同的方式实现每个操作。让我们看看如果我们只是接受这个想法并运行它，以最直接的方式实现所有必需的函数会发生什么。

> module Compact_array = struct
  type 'a t = | Array of 'a array
        | Bytes of bytes
  let of_bytes x : char t = Bytes x
  let of_array x = Array x
  let length = function
   | Array a -> Array.length a
   | Bytes s -> Bytes.length s
  let get t i =
   match t with
   | Array a -> a.(i)
   | Bytes s -> s.[i]
  let set t i v =
   match t with
   | Array a -> a.(i) <- v
   | Bytes s -> s.[i] <- v
 end;;
module Compact_array :
 sig
  type 'a t = Array of 'a array | Bytes of bytes
  val of_bytes : bytes -> char t
  val of_array : 'a array -> 'a t
  val length : 'a t -> int
  val get : char t -> int -> char
  val set : char t -> int -> char -> unit
 end

乍一看，这似乎非常好，但推断的类型与我们想要的略有不同。特别是，get 和 set 仅适用于包含字符的 Compact_array。如果你考虑类型推断是如何工作的，这并不是那么令人惊讶。如果你考虑 get 的代码：

let get t i =
 match t with
 | Array a -> Array.get a i
 | String s -> String.get s i

OCaml 编译器正在寻找一个类型来分配给匹配的所有情况的返回值。鉴于 String.get 始终返回 char，那么 Compact_array.get 将被限制为仅返回 char。

解决此问题的一种方法是基本上将我们想要的东西实现为一个简陋的对象。在这里，我们只是为不同的情况分别编写代码，并将这些函数塞进一个充满闭包的记录中。这是它的样子。

> module Compact_array = struct
 type 'a t = { len: unit -> int
       ; get: int -> 'a
       ; set: int -> 'a -> unit
       }
 let of_string s =
  { len = (fun () -> String.length s)
  ; get = (fun i -> String.get s i)
  ; set = (fun i x -> String.set s i x)
  }
 let of_array a =
  { len = (fun () -> Array.length a)
  ; get = (fun i -> Array.get a i)
  ; set = (fun i x -> Array.set a i x)
  }
 let length t = t.len ()
 let get t i = t.get i
 let set t i x = t.set i x
end;;
module Compact_array :
 sig
  type 'a t = {
   len : unit -> int;
   get : int -> 'a;
   set : int -> 'a -> unit;
  }
  val of_string : bytes -> char t
  val of_array : 'a array -> 'a t
  val length : 'a t -> int
  val get : 'a t -> int -> 'a
  val set : 'a t -> int -> 'a -> unit
 end

这或多或少解决了这个问题，但它仍然不是我们真正想要的内存表示。特别是，我们必须为每个 Compact_array.t 分配三个闭包，并且随着我们添加更多行为取决于底层数组的函数，闭包的数量只会增加。

GADTs 来拯救

让我们回到我们失败的基于变体的实现，但使用 GADT 语法重写它。请注意，这次我们根本没有尝试更改类型，只是用 GADT 的语言重写了我们之前的相同类型。

type 'a t = | Array : 'a array -> 'a t
      | Bytes : bytes -> 'a t

此声明的语法建议将变体构造函数（如 Array 或 Bytes）视为从构造函数参数到结果值的类型函数，其中 : 右侧的内容大致对应于构造函数的类型签名。

请注意，对于 Array 构造函数，'a 的类型值取决于参数的类型：

> Array [|1;2;3|];;
- : int t = Array [|1; 2; 3|]
> Array [|"one";"two";"three"|];;
- : bytes t = Array [|"one"; "two"; "three"|]

但对于 Bytes 构造函数，类型 'a 在类型中仍然是自由的。

> Bytes "foo";;
- : 'a t = Bytes "foo"

这确实是有问题的案例，因为我们希望 Bytes "foo" 的参数 'a 是 char，因为在 Bytes 案例中，这就是我们数组的元素类型。

因为 GADTs 使我们能够指定箭头右侧的类型，所以我们可以得到它。

type 'a t = | Array : 'a array -> 'a t
      | Bytes : bytes -> char t

现在，Bytes 构造函数的行为符合我们的预期。

> Bytes "foo";;
- : char t = Bytes "foo"

现在让我们看看当我们尝试编写 length 函数时会发生什么。

> let length t = 
   match t with
   | Bytes b -> Bytes.length b
   | Array a -> Array.length a
 ;;
val length : char t -> int = <fun>

令人失望的是，我们再次陷入了没有正确类型的函数。特别是，编译器已经确定此函数只能对 char t 进行操作，而我们希望它可以用于任何类型的数组。

但现在的问题是，在存在 GADTs 的情况下，类型推断很困难，编译器需要一些帮助。粗略地说，如果没有一些提示，OCaml 的类型系统将尝试将所有类型识别为在给定函数中具有单个值。但在这种情况下，我们需要一个类型变量，该变量在匹配语句的不同分支中可能具有不同的值。

我们可以通过创建一个局部抽象类型 el 来表示 t 的类型参数（和元素类型），并相应地注释 t 来做到这一点。

> let length (type el) (t:el t) = 
   match t with
   | Bytes b -> Bytes.length b
   | Array a -> Array.length a
 ;;
val length : 'a t -> int = <fun>

现在我们看到我们得到了正确的类型。我们可以将这种方法推到完整实现。

> module Compact_array = struct
  type 'a t = | Array : 'a array -> 'a t
        | Bytes : bytes -> char t
  let of_bytes x = Bytes x
  let of_array x = Array x
  let length (type el) (t:el t) =
   match t with
   | Array a -> Array.length a
   | Bytes s -> Bytes.length s
  let get (type el) (t:el t) i : el =
   match t with
   | Array a -> Array.get a i
   | Bytes s -> Bytes.get s i
  let set (type el) (t:el t) i (v:el) =
   match t with
   | Array a -> Array.set a i v
   | Bytes s -> Bytes.set s i v
 end;;
module Compact_array :
 sig
  type 'a t = Array : 'a array -> 'a t | Bytes : bytes -> char t
  val of_bytes : bytes -> char t
  val of_array : 'a array -> 'a t
  val length : 'a t -> int
  val get : 'a t -> int -> 'a
  val set : 'a t -> int -> 'a -> unit
 end

正如我在一开始所说的那样，这实际上只是一个更通用主题的示例。 GADTs 不仅仅是聪明的类型化解释器；它们是一种强大的机制，用于构建易于使用的抽象，使你可以更精确地控制你的内存表示。并且获得正确的内存表示对于构建高性能应用程序通常至关重要。

Yaron Minsky 于 2002 年加入 Jane Street，并声称自己说服公司开始使用 OCaml 是一个值得怀疑的荣誉。