时间旅行的故事

译自 A Time-Travel Story。除非特殊声明，下文中「我」指原文作者凤凰院██ Oleg Kiselyov。

导言

这是一个真实的故事，有据可查，我也被卷入其中。故事讲述了有关回到过去然后做出不同选择的经历。但出乎意料的是，一件隐私，一件被认为绝对安全的秘密被曝光了。

时间旅行的故事通常以「改变过去最终了造成预料之外的结果」为题，这个故事也不例外：穿越时空意外地揭露了一个肮脏的诡计，一项瞒天过海的暗箱操作，然而……言归正传，我们开始吧。

某天，我收到了来自一位 Hansei 用户的消息：这位用户的概率程序给出了明显错误的结果。Hansei 是一个 OCaml 语言编写的概率编程库，它的工作原理是：通过不断地回到过去做出不同选择从而创造新的世界线，并统计潜在的世界线的历史记录。这位用户最终发现库函数 List.map 是罪魁祸首：当他使用自己写的 map 函数时，问题就消失了。我感到很困惑，列表的 map 函数应该很简单，不可能出错。用户还提到了他用了 Batteries¹，这是一种 OCaml 标准库的替代品。我亲自查看 Batteries 库源码之后发现了这个……

版本

当前版本为 2014 年 9 月版

引用资料

• Why List.map does not be implemented

2014 年 9 月 29 日至 10 月 1 日间在 Caml-list 邮件列表上讨论的主题

• HANSEI: Embedded Probabilistic Programming

• Hayo Thielecke: Using a Continuation Twice and Its Implications for the Expressive Power of call/cc

讲述了更多的关于时间旅行带来意想不到后果的故事。例如：事实证明，即使不改变过去发生的任何事情，时空旅行也是可以被察觉的（见「the refutation of the idempotency hypothesis」）。发表于： Higher-Order and Symbolic Computation, volume 12, April 1999,pp. 47-73.

List.map 的小秘密

Batteries 中的 List.map 与人们所想的不太一样……

首先展示一个标准的，耳熟能详的 List.map 函数：

let rec map : ('a -> 'b) -> 'a list -> 'b list = fun f -> function
| []     -> []
| h :: t -> f h :: map f t

这个 map 函数是非尾递归的，因此运行该函数消耗的栈空间与输入列表的大小成正比。当 map 一个长列表时，程序可能会爆栈（或者导致耗时的栈重分配操作），因为栈通常比堆小得多。

OCaml 的 Batteries 是一个经过精心优化的库。它的 List.map 函数是尾递归的，运行时消耗恒定的栈空间。严格来说，这样的实现不可能高效率——但这就是秘密所在，让我们探索一下它的源码。函数源码经过解糖之后是：

type 'a mut_list = {
    hd: 'a;
    mutable tl: 'a list
  }

let map_mut : ('a -> 'b) -> 'a list -> 'b list = fun f -> function
  | []     -> []
  | h :: t ->
      let rec loop dst = function
        | []     -> ()
        | h :: t ->
            let cell = {hd = f h; tl = []} in
            dst.tl <- Obj.magic cell;
            loop cell t
      in
      let r = {hd = f h; tl = []} in
      loop r t;
      Obj.magic r

loop 显然是尾递归函数，同样显然的是代码里面有 Obj.magic。让我们通过自己的推导来理解这些代码。

List.map 把输入列表中的元素映射到输出列表的元素。这种操作不需要缓冲区，理论上可以在恒定空间内完成。但 map 需要维持列表的顺序：每当它从输入列表的头取出一个元素时，它应该把映射后的结果放在输出列表的末尾。

module V1 = struct
  let snoc : 'a -> 'a list -> 'a list = fun x l -> l @ [x]

  let map : ('a -> 'b) -> 'a list -> 'b list = fun f l ->
    let rec loop acc = function
      | []     -> acc
      | h :: t -> loop (snoc (f h) acc) t
    in loop [] l
end

V1 的 map 是尾递归函数，它用 snoc 向输出列表尾部追加元素。遗憾的是：snoc 需要的栈空间与输入列表的大小成正比。我们的目标是让 snoc 在常数级时间内完成运行。

在准备优化之前，我们先分离空列表的情况。这样 snoc 就只关心非空列表了。

module V2 = struct
  let snoc : 'a -> 'a list -> 'a list = fun x l -> l @ [x]

  let map : ('a -> 'b) -> 'a list -> 'b list = fun f -> function
    | []     -> []
    | h :: t -> 
        let rec loop acc = function
          | []     -> acc
          | h :: t -> loop (snoc (f h) acc) t
        in loop [f h] t
end

然后我们仔细研究 map 真正需要的列表操作，并把这些操作抽象到只关心非空列表的 NList 模块中：

module type NList = sig
  type 'a t
  val singleton : 'a -> 'a t
  val to_list : 'a t -> 'a list
  val snoc : 'a -> 'a t -> 'a t
end

我们可以借助 NList 抽象把列表的 map 操作改写成下面这种通用形式。本文剩余部分的代码中都使用这个 map。

module ListMap(NL:NList) = struct
  let map : ('a -> 'b) -> 'a list -> 'b list = fun f -> function
    | []     -> []
    | h :: t -> 
        let rec loop acc = function
          | []     -> NL.to_list acc
          | h :: t -> loop (NL.snoc (f h) acc) t
        in loop (NL.singleton (f h)) t
end

普通的 OCaml 列表可以作为一种幼稚的 NList 实现：

module NL_list : NList = struct
  type 'a t = 'a list
  let singleton x = [x]
  let to_list x = x
  let snoc x l = l @ [x]
end

ListMap(NL_List) 等效于之前展示过的 V2 版低效 map 实现，我们的目标变为：找到一个更好的 NList 实现。模块化抽象使我们的代码拥有底层表示独立性（representation independence）：map 不依赖也不可能依赖特定的 NList 底层实现。因此我们可以自由地选择底层实现，从而优化 snoc 函数。

在研究 Batteries 时我们发现了一种新的列表技术：通过嵌套尾部可变的二元组来实现列表（出于某些历史原因，下文中把这种二元组称为 cons cell²）。cons cell 的头部表示当前元素，尾部表示下一个 cons cell，列表则由第一个和最后一个 cons cell 组成。这里尝试实现之。

module NL_twocons : NList = struct
  type 'a cons = {hd : 'a; mutable tl : 'a cons option}
  type 'a t = 'a cons * 'a cons

  let new_cell : 'a -> 'a cons = fun x -> {hd=x; tl=None}
  let singleton x = let l = new_cell x in (l,l)

  let to_list (first,_) = 
    let rec go = function 
      | {hd;tl=Some t} -> hd :: go t
      | {hd;tl=None}   -> [hd] 
    in go first

  let snoc x (first, last) = 
    let cell = new_cell x in
    last.tl <- Some cell;
    (first,cell)
end

当向列表的尾部追加内容时，只需简单修改最后一个 cons cell 的尾部，令其指向一个新的 cons cell 即可。但现在最优 snoc 实现的优势反而被 to_list 抵消了。

需要一些 OCaml 黑魔法知识才能让 to_list 也在常数时间内完成：

module NL_magic : NList = struct
  type 'a cons = {hd : 'a; mutable tl : 'a list}
  type 'a t = 'a cons * 'a cons

  let from_cons : 'a cons -> 'a list = Obj.magic

  let new_cell : 'a -> 'a cons = fun x -> {hd=x; tl=[]}

  let singleton x = let l = new_cell x in (l,l)
  let to_list (first,_) = from_cons first

  let snoc x (first, last) = 
    let cell = new_cell x in
    last.tl <- from_cons cell;
    (first,cell)
end

结构体 'a NL_magic.cons 与普通列表中的 h :: t 具有相同的内存布局。因此，我们可以把其中一个类型的值重铸（cast）为另一个类型。严格来说，从不可变的 h :: t 重铸为 'a cons 并不安全，因为 OCaml 编译器会基于数据结构的不可变性进行优化。但是我们只是把可变的数据重铸为不可变的数据，这是安全的。现在所有的 NList 操作都只花费常数级时间，我们的任务圆满结束。将 ListMap(NL_magic).map 代码经过内联和简单优化后，便可得到本节开头的 map_mut 代码（编译器可以自动完成这些优化）。

这段代码中包含了常见的「初始化模式」：在最开始分配结构体时，结构体内含有一些尚未初始化的字段。然后我们通过可变操作填充这些值，最后「冻结」结构体，使其不可变。from_cons 就是这种「冻结」操作。只要代码持有未填充完整的结构体的独占所有权，不把它泄漏给别人，这种延迟的就地初始化是安全的。在我们的例子中，'a cons 是 NL_magic 的内部结构，不可能在 ListMap(NL_magic) 之外获取指向该数据的引用。修改私有数据的过程其实是暗箱操作。然而这种暗箱操作却被曝光了，怎么会这样？

引用资料

• maps.ml

本文用于推导问题的完整 OCaml 代码，附有测试。

时间旅行与多重世界线

时间旅行与多重世界线不只是科幻小说中的概念，同时也是非确定性计算领域的家常便饭。在非确定性计算中，我们可以回溯时间，改变过去作出的选择，从而观察并统计不同时间线的历史记录——这就是本故事中 Hansei 概率编程库的原理。也正是在 Hansei 中，我们首次发现了 List.map 存在的问题。Caml-list 邮件列表的讨论中也以 Hansei 为例，不过在本文中，我们将用一个很简单的库来解释这个问题。这个库只有两个操作：

val choose : 'a -> 'a -> 'a
val top    : (unit -> 'a) -> 'a list

choose x y 表示非确定地选择 x 或 y，而 top thunk 返回一个列表，列表包含了有所有可能世界线中 thunk 的返回值。例如：

top (fun () -> not (choose false true))

返回 [true; false]，代表两种可能的选择。

在回溯到过去前，必须保存程序的状态或者说上下文——这样才能在结束回溯后正确地回到当前时空。时间旅行必然涉及到续延（continuation），我们可以利用 delimcc 库的定界控制操作子（delimited control operator），通过简单几行代码实现 choose 和 top。

open Delimcc

let p = new_prompt ()

let choose : 'a -> 'a -> 'a = fun x y -> 
  shift p (fun k -> k x @ k y)

let top : (unit -> 'a) -> 'a list = fun th ->
  push_prompt p (fun () -> [th ()])

掷硬币式的操作 choose false true 首先捕获上下文 k，然后作出 false 选择：因此整个 choose false true 表达式变为 false，程序依此继续运行，最终返回了 [true]。然而这时我们回溯时间并在 choose 处作出不同选择，在重新运行程序后得到了 [false]。最后收集不同世界线下产生的结果得到了 [true; false]。

下面举一个更复杂的例子，例子中有两次相互独立的非确定性选择：

top (fun () -> map (fun _ -> choose false true) [1;2])
(* [[false; false]; [true; false]; [false; true]; [true; true]] *)

注释中随附的运行结果展示了两次相互独立的抛硬币事件产生的四种所有可能。这里我们使用标准库中的 List.map，任何效率底下的 map 实现（如 V1、V2 或 ListMap(NL_List)）都能得到相同的结果。而高效的尾递归版本 ListMap(NL_magic) 或 map_mut 则不然：两次掷硬币的结果无法同时为 true！简而言之，这正是 Hansei 用户所汇报的问题。

发生甚么事了？我们再观察一下 ListMap：

module ListMap(NL:NList) = struct
  let map : ('a -> 'b) -> 'a list -> 'b list = fun f -> function
    | []     -> []
    | h :: t -> 
        let rec loop acc = function
          | []     -> NL.to_list acc
          | h :: t -> loop (NL.snoc (f h) acc) t
        in loop (NL.singleton (f h)) t
end

读者可以认为 choose false true「分裂了世界线」（这就像一个关于量子力学的多重世界解释的实验）。在一条世界线中，choose false true 返回 false，而在另一条中则返回 true。然而分裂后的两条世界线共享同一个堆内存。因此，任意世界线中更改可变量的行为都会被其他世界线观测到。从编程语言的术语来说：定界续延（delimited continuation）可以捕获调用栈，却不能捕获堆。如果捕获的续延中含有修改堆的操作，重放该续延就会产生竞态条件。再从另外一个角度看：分裂后的世界线仍共享同一个部分构造好的输出列表，仅当这样的部分列表被某条世界线独占时，对其进行变更才是安全的。世界线分裂后，私有数据仍是私有数据，却不是被某条世界线唯一私有的数据了。

这个问题之所以难以捉摸，令人摸不着头脑，正是因为它与「外部代码污染数据」无关。map 的私有数据无法从外部访问，不可能存在这种污染。恰恰相反，是 map 本身被愚弄了，从而自己污染了自己的数据。

穿越安全且无锁

非确定性编程确实类似于共享内存并行编程。优化后的 List.map 不再线程安全，从而导致了我们遇到的问题。下面提出的解决方案是线程安全且无锁的——因为非确定性计算中没有锁，所以是无锁的。这个修复的想法来自 Gabriel Scherer 在 Caml-list 上的留言，要解释和实现这个想法也很简单，不需要「金丝雀」值³这样的技术。

幸运的是，非确定性不像一般的共享内存并行那么糟糕。首先，非确定性计算中的「线程抢占」只能发生在特定的时间，即 map 函数调用其回调函数时。⁴更主要的一点是，我们仍可以保证私有的数据只有其所有者才能修改。因此，我们只需检查 map 代码，无需关心回调函数或者 map 的结果的消费者可能会做什么。

仔细观察 NL_magic 的代码

let snoc x (first, last) = 
  let cell = new_cell x in
  last.tl <- from_cons cell;
  (first,cell)

我们可以发现这段代码暗含了一个 snoc 的前置条件（pre-condition）：last 顾名思义应该是列表中最后一对 cons cell，即 last.tl 必须为 []。我们却没有检查这个条件——在单线程环境下 map 自动满足了这个条件，因为它不会对同一个列表调用两次 snoc。

当对同一个列表调用两次 snoc 时，snoc 会发现它操作的列表已经被其他人所扩展过。它不再独占该列表，而是和别人共享从 first 到 last 之间的列表片段。我们应该通过深拷贝（deep copying）这些共享片段来恢复 snoc 对列表的独占所有权，如下面代码所示：

let snoc_simple : 'a -> 'a cons -> 'a cons = fun x dst ->
    let cell = new_cell x in
    dst.tl <- from_cons cell;
    cell

      (* Copy from first to last inclusive *)
  let deep_copy : 'a t -> 'a t = fun (first,last) ->
    let rec loop first last dst =
      if first == last then dst 
      else match first with
      | _ :: ((h :: _) as t) -> loop t last (snoc_simple h dst)
      | _      -> assert false
    in
    let res = new_cell first.hd in
    let last = loop (from_cons first) (from_cons last) res in
    (res,last)

  let snoc x ((first, last) as l) =
    if last.tl = [] then (first,snoc_simple x last)
    else 
      let (first,last) = deep_copy l in
      (first, snoc_simple x last)
end

这里仅展示 NL_magic 代码中有修改的部分。新版本的代码在「单线程」条件下仍和之前一样快（我们只添加了一个 last.tl = [] 的检查），而在非确定性计算的情况下也不再有竞态条件。深拷贝列表的做法正合世界线分裂的本意：分裂后的两个新世界相互独立。

引用资料

• Gabriel Scherer: Re: Why List.map does not be implemented

于 2014 年 10 月 29 日星期三在 Caml-list 邮件列表上发布的消息

结论

前置条件、不变式、底层表示独立性、隔离，这些概念的确有助于编写更好的程序，至少它们有助于我们理解和消灭问题。事实上，我们遇到的问题与一个「显然」（因此没有明确指出）的前置条件有关。但出乎意料的是，这个前置条件并没有人们所默认的那么显然。本文还证实了续延往往会打破一些显然的前置条件。而至于时间旅行的复杂性——敬请收看什恩・卡鲁斯导演的《命运之门》⁵。

引用资料

• https://en.wikipedia.org/wiki/Primer_(film)

参考