OCaml 中的极简风 GADTs

译自 Simplistic GADTs in OCaml。除非特殊声明，下文中「我」代指原文作者 Oleg Kiselyov
From oleg at http://okmij.org Fri Jul 10 20:05:10 2009
To: caml-list@inria.fr
Subject: GADTs in OCaml
Message-Id: 20090711030510.49092176DE@Adric.metnet.navy.mil
Date: Fri, 10 Jul 2009¹ 20:05:10 -0700 (PDT)
Status: RO

本文展示了一种 OCaml 中的简单、无副作用、且不需要魔法的实现 GADTs²³ 的方法。这种实现足以覆盖 GADTs 的许多常见应用：表达带有不变式（invariant）的数据结构、有类型的 printf/scanf、无标签（tagless）解释器等。本文提出的具体实现只是一个简单的 ML 模块，不需要修改 OCaml 系统本身。由于实现十分简单，理论上可以在任意 ML 系统上运行（不过，就如同嵌套数据类型一样，在不支持多态递归（polymorphic recursion）的 SML 上，GADT 也不是很有用）。

本文的例子涵盖了：

保障数据结构的不变式：静态地保证在一个表示某 HTML 文档的树结构中，一个链接节点不能为另一个链接节点的父节点。
有类型的 printf/scanf 实现，两个实现之间共享相同的格式化描述符。
带有常量和高阶抽象语法（High-Order Abstract Syntax）的简单有类型 $λ$-演算。我们所展示的其实就是奚宏伟等人（Xi et. al）的 POPL 2003 论文⁴中所展示的例子。

请移步 http://okmij.org/ftp/ML/GADT.ml 以获取带有实现和例子的完整代码。

GADT 本身的记法符号很轻量。然而 GADTs 通常是归纳数据类型，处理归纳数据类型又需要多态递归函数，因此又引入了一些（很小的）符号开销。最主要的是，GADTs 常与存在量化类型（existentially quantified type）并辔。在 Haskell 中，GADT 类型声明隐含了存在量化类型声明。遗憾的是，OCaml 却缺乏这样的符号便利，况且在 OCaml 中编码存在量化类型（通过双重否定）⁵并不美观。至于智能构造函数（smart constructor）——靠手搓，或许可以写一个合适的 camlp4 宏来减轻痛苦。

我们从探索的过程中学到的一课是：目前的 OCaml 就已经可以实现常用的 GADTs。在不对目前 OCaml 类型系统进行修改的前提下，我们就已经可以写出之前所提出的，使我们认为需要 GADTs 特性的例子——并且不会有太多记法符号上的麻烦。我们也可以或多或少地将 Haskell 中使用了 GADTs 的代码机械地转译为 OCaml 代码。当然，为 OCaml 的类型系统添加诸如显式存在量化类型，对 Rank-2 类型更好的支持⁶等特性无疑是锦上添花，但并不是使用和享受 GADTs 的必要条件。

希望本文提供的实现能让各位体验一下 GADTs，或帮助各位编写似乎依赖于 GADTs 特性的代码。GADT.ml 文件的结尾还提出了一种更高效的实现方法，这种方法或许可以作为 OCaml 中原生支持 GADTs 实现的基础。

正如 Patricia Johann 与 Neil Ghani 的《Foundations for Structured Programming with GADT》（POPL 2008）⁷所指出的。GADTs 的本质是 EQ GADT，即实现了以下接口的类型：

type ('a, 'b) eq
val refl : ('a, 'a) eq
val apply_eq : ('a, 'b) eq -> 'a -> 'b

类型 ('a, 'b) eq⁸ 的值代表对「两个类型相等」这一命题的证明。而 apply_eq 利用了这一证明以执行安全的类型强制（coercion）。

更准确地说：真正的 GADTs 实现对于任意类型 τ 都提供了一个表示莱布尼茨律（Leibniz’s principle）⁹的函数。该函数有以下类型签名

val apply_eq : ('a, 'b) eq -> 'a τ -> 'b τ

虽然我们的实现只能支持那些 Functor 式（即支持 map 操作）的类型 τ。不过，对于常见案例来说似乎已经足够了。

这一朴素实现也从原理上避免了出现段错误，因此是真正安全的。

module EQ = struct
  type ('a,'b) eq = Refl of 'a option ref * 'b option ref
  let refl () = let r = ref None in Refl (r,r)
  let symm : ('a,'b) eq -> ('b,'a) eq = function 
      Refl (x,y) -> Refl (y,x)
  let apply_eq : ('a,'b) eq -> 'a -> 'b = function
      Refl (rx,ry) -> fun x ->
        rx := Some x;
        match !ry with
        | Some y -> rx := None; y
        |     _  -> failwith "Impossible"
end;;

下面简要展示 GADT.ml 中的一个例子：有类型的 printf/scanf 实现，printf 与 scanf 之间互相共享格式化描述符：

let tp2 = sprintf (f_lit "Hello " ^^ f_lit "world" ^^ f_char) '!';;
(* val tp2 : string = "Hello world!" *)
let ts2 = sscanf tp2 (f_lit "Hello " ^^ f_lit "world" ^^ f_char) (fun x -> x);;
(* val ts2 : char * string = ('!', "") *)
(* 格式化描述符是头等对象，可以增量式创建 *)
let fmt31 () = f_lit "The value of " ^^ f_char ^^ f_lit " is ";;
(* val fmt31 : unit -> ('a, char -> 'a) fmt *)
let fmt3 () = fmt31 () ^^ f_int;;
(* val fmt3 : unit -> ('a, char -> int -> 'a) fmt *)
let tp3 = sprintf (fmt3 ()) 'x' 3;;
(* val tp3 : string = "The value of x is 3" *)
(* 我们不但可以打印值，也可以从字符串中读回值 *)
let ts3 = sscanf tp3 (fmt3 ()) (fun x n -> (x,n));;
(* val ts3 : (char * int) * string = (('x', 3), "") *)

这一例子是对下列 Haskell 代码的 OCaml 直接再实现

我们通过 GADT 定义了描述格式的领域特定语言（Domain Specific Language, DSL），而这一 GADT 正是用 OCaml 实现的，具体如下：

type ('a,'b) fmt =
  | FLit of < m_flit : 'w. (('a,'b) eq -> string -> 'w) -> 'w >
  | FInt of < m_fint : 'w. ((int -> 'a,'b) eq -> 'w) -> 'w >
  | FChr of < m_fchr : 'w. ((char -> 'a,'b) eq -> 'w) -> 'w >
  | FCmp of < m_fcmp : 'w. ('a,'b,'w) fcmp_k -> 'w >
      (* 存在量化类型的标准编码方式 *)
and ('a,'c,'w) fcmp_k = 
    {fcmp_k : 'b. ('b,'c) fmt * ('a,'b) fmt -> 'w}
;;

并（手动地）定义智能构造函数如下：

let f_lit x 
    = FLit (object method m_flit : 'w. (('a,'b) eq -> string -> 'w) -> 'w
        = fun k -> k (refl ()) x end);;
(* val f_lit : string -> ('a, 'a) fmt *)
let f_int 
    = FInt (object method m_fint : 'w. ((int -> 'a,'b) eq -> 'w) -> 'w
        = fun k -> k (refl ()) end);;
(* val f_int : ('a, int -> 'a) fmt *)

下面则展示了上述 DSL 的一个解释器，该解释器把值格式化为字符串：

type print_sig = {pr: 'a 'b. ('a,'b) fmt -> (string -> 'a) -> 'b};;
let rec printer = {pr = 
 function 
   | FLit x -> fun k -> x#m_flit (fun eq x -> apply_eq eq (k x))
   | FInt x -> fun k -> x#m_fint (fun eq   -> apply_eq eq 
         (fun x -> k (string_of_int x)))
   | FChr x -> fun k -> x#m_fchr (fun eq   -> apply_eq eq 
         (fun x -> k (String.make 1 x)))
   | FCmp x -> fun k ->
       x#m_fcmp {fcmp_k = 
          fun (a,b) -> printer.pr a (fun sa ->
                        printer.pr b (fun sb -> k (sa ^ sb)))}
};;
let sprintf fmt = printer.pr fmt (fun x -> x);;
(* val sprintf : (string, 'a) fmt -> 'a *)

代码非常简单，读者可以创建许多类似的解释器：例如，在不修改格式描述符或库本身的情况下，将格式化输出导向任意适合的数据出口。

参考

本文原文发布于 2009 年，译文发布于 2024 年。在译文发布时，OCaml 已经支持原生 GADTs 特性。 ↩︎
https://v2.ocaml.org/manual/gadts-tutorial.html ↩︎
https://dev.realworldocaml.org/gadts.html ↩︎
https://dl.acm.org/doi/abs/10.1145/604131.604150 ↩︎
https://okmij.org/ftp/Computation/Existentials.html#exist-via-foralls.html ↩︎
https://v2.ocaml.org/manual/polymorphism.html ↩︎
https://libres.uncg.edu/ir/asu/f/Johann_Patricia_2008_Foundations_For_Structured_Programming_with_gadts.pdf ↩︎
https://www.bananaspace.org/wiki/%E7%9B%B8%E7%AD%89%E7%B1%BB%E5%9E%8B ↩︎
https://plato.stanford.edu/entries/identity-indiscernible/ ↩︎

参考#

参考