【译】shift/reset 编程入门 (2)：应用

第一节：

Spore：【译】shift/reset 编程入门 (0)&(1)：前言和概述

2 shift/reset 编程

2.1 什么是 Continuation

Continuation，简而言之就是「之后的计算」。程序的执行过程就是选出要执行的部分（称作 redex〔reducible expression，可归约表达式〕），对它求值，再使用它的结果来进行之后的计算。这里的「之后的计算」就是指 continuation。因此，continuation 是任何程序执行时都存在的基本概念。

为了展示 continuation 具体是什么，我们用 $[\,... ]$（称作 hole）来表示一段程序接下来要执行的部分。比如 $3 + 5 * 2 - 1$ 这一算式中，如果接下来要执行的部分是 $5 * 2$ 的话就可以写作 $3 + [5 * 2] - 1$，而这时的 continuation 就是 $3 + [~\cdot~] - 1$。总之，得到 $[~\cdot~]$ 的值（$5 * 2$ 的结果 $10$）之后，「给这个得到的结果加上 $3$ 减去 $1$」就是整个式子当前的 continuation。从「接受 hole 的值之后用它进行计算」这方面来看，continuation 和函数是相似的。

也可以用「抛出异常时扔掉的那部分程序」来看待 continuation。例如，把上述例子中 $[~\cdot~]$ 的部分换成 raise Abort，让它抛出异常，这时候被抛弃的部分 $3 + [~\cdot~] - 1$ 就是 continuation。

随着程序的运行，当前的 continuation 时时刻刻都在变化。例如，在上述例子中，计算完 $5 * 2$，原表达式变成了 $3 + 10 - 1$。这个新的表达式下一步要执行 $3 + 10$，所以可以写作 $[3 + 10] - 1$。因此，这时的 continuation 就变成了 $[~\cdot~] - 1$，也就是「从结果中减去 $1$」。再执行一步，表达式就变成了 $13 - 1$。下一步只剩下 $13 - 1$ 要执行，因此记作 $[13 - 1]$。此时的 continuation 是 $[~\cdot~]$（空 continuation），即「不做任何操作，原样返回值」。

练习问题 1 请在下列表达式中加入 $[~\cdot~]$，将它们分解成「接下来要执行的表达式」和「该表达式的 continuation」。前者的类型是什么？若把这一类型的值传给 continuation，最终的返回值又应该是什么类型？

1. 5 * (2 * 3 + 3 * 4)
2. (if 2 = 3 then "hello" else "hi") ^ " world"
3. fst (let x = 1 + 2 in (x , x))
4. string_length ("x" ^ string_of_int (3 + 1))

2.2 什么是 Delimited Continuation

Continuation 是「之后的计算」，delimited continuation 则是「之后的计算」中范围有限（被划定界限）的一部分。$3 + [5 * 2] - 1$ 中，当前的 continuation 是 $[~\cdot~]$ 外侧的整个计算，也就是 $3 + [~\cdot~] - 1$，而 delimited continuation 则是它的一部分，也就是在某个限定范围内的 continuation。

我们用分隔符 $\langle \cdot\cdot\cdot \rangle$ 来指定 continuation 的范围。比如，像 $\langle 3 + [5 * 2]\rangle - 1$ 这样进行限定，则当前的 delimited continuation 就是 $\langle 3 + [~\cdot~]\rangle$，而不包含 $-~1$。

2.3 Continuation 限定操作符 reset

使用 reset 操作符可以对 continuation 的范围进行限定。本文按照 OchaCaml 的语法，使用

reset (fun () -> M)

这样的写法。这个语句照常对 M 进行求值，但 M 当中捕获的 continuation 以 reset 为界。

例如，以下表达式中，

reset (fun () -> 3 + [5 * 2]) - 1

当前的 delimited continuation 是「给结果加上 $3$」而不包含「减去 $1$」。这个例子中表达式 $5 * 2$ 并没有捕获 continuation，因此求值时等同于没有 reset 的情况。$5 * 2$ 得到 $10$，再加 $3$ 得到 reset 的返回值 $13$，最后减去 $1$ 得到最终结果 $12$。

也可以通过「把 reset 换成 try ... with Abort -> ...」的方式来理解 delimited continuation，此时的 continuation 就是「把当前要计算的表达式换成 raise Abort 时舍弃的部分」。比如说，

reset (fun () -> 3 + [5 * 2]) - 1

这里的 delimited continuation 就是执行

(try 3 + [raise Abort] with Abort -> 0) - 1

的时候舍弃的部分，也就是 $3 + [~\cdot~]$。

练习问题 2 下列表达式中的 delimited continuation 及其类型分别是什么？

1. 5 * reset (fun () -> [2 * 3] + 3 * 4)
2. reset (fun () -> if [2 = 3] then "hello" else "hi") ^ " world"
3. fst (reset (fun () -> let x = [1 + 2] in (x, x)))
4. string_length (reset (fun () -> "x" ^ string_of_int [3 + 1]))

2.4 Continuation 捕获操作符 shift

OchaCaml 中使用 shift 捕获 delimited continuation，用法如下。

shift (fun k -> M)

在这个表达式中，shift 执行下列三个操作。

1. 清除当前的 delimited continuation，
2. 把它绑定到参数 k 上，
3. 然后执行 M。

下文我们将详述它的用途。

2.5 丢弃 Continuation

请看以下表达式。

shift (fun _ -> M)

这里的 _ 代表一个不在程序中任何其他地方出现的变量，等同于表达式 shift (fun k -> M) 中 M 不包含 k 的情况。这个表达式的求值像这样进行：

1. 清除当前的 delimited continuation，
2. 把它作为参数传递给 (fun _ -> M)，但 M 中并不使用它。结果就是丢弃掉当前的 continuation，
3. 并执行 M。

因此，执行这个表达式时当前程序直到最近的 reset 为止的部分会被丢弃，并被 M 取代。

来具体地尝试一下吧。如果想要丢掉 $3 + [5 * 2] - 1$ 的 continuation 而用 $5 * 2$ 作为整体结果，可以把整个表达式放入 reset，并把 $[~\cdot~]$ 的部分换成 shift (fun _ -> 5 * 2)。

# reset (fun () -> 3 + shift (fun _ -> 5 * 2) - 1) ;;
- : int = 10
#

在这个例子中 M 是 $5 * 2$，所以结果就是 $10$ 了。不过，这里的返回结果其实可以不是整数。

# reset (fun () -> 3 + shift (fun _ -> "hello") - 1) ;;
- : string = "hello"
#

这里，被丢弃的 continuation 是 $3 + [~\cdot~] - 1$，类型为 int -> int。尽管原本要返回一个整数，实际的返回值却是一个字符串。然而，上述表达式仍然有着正确的类型〔well-typed〕。关于这里发生的类型变化我们之后再做讨论。

此外，只有 reset 之内的 continuation 会被丢弃。比如，

# reset (fun () -> 3 + shift (fun _ -> 5 * 2)) - 1 ;;
- : int = 9
#

上面的表达式中被丢弃的 continuation 只有 $3 + [~\cdot~]$，减去 $1$ 的部分则保留了下来。并且，这个例子中不能返回整数之外的值，因为 reset 中返回的值最终一定要减去 $1$：

# reset (fun () -> 3 + shift (fun _ -> "hello")) - 1 ;;
Toplevel input:
> reset (fun () -> 3 + shift (fun _ -> "hello")) - 1 ;;
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This expression has type string,
but is used with type int.
#

练习问题 3 请在下列表达式的 $[~\cdot~]$ 中填入形如 shift (fun _ -> M) 的表达式，来丢弃当前的 continuation，并返回合适的值。

1. 5 * reset (fun () -> [·] + 3 * 4)
2. reset (fun () -> if [·] then "hello" else "hi") ^ " world"
3. fst (reset (fun () -> let x = [·] in (x, x)))
4. string_length (reset (fun () -> "x" ^ string_of_int [·]))

练习问题 4 请看以下求整数列表中所有元素之积的函数。

(* times : int list -> int *)
let rec times lst = match lst with
    [] -> 1
  | first :: rest -> first * times rest

例如，以 [2; 3; 5] 为参数调用这个函数就会得到 $30$。现在假设我们给这个函数传入参数 [2; 3; 0; 5]。由于列表中含有元素 $0$，不用继续计算也知道最后的结果是 $0$。可以修改上述程序，使其在遇到列表中的 $0$ 时丢弃当前的 continuation，并直接返回结果 $0$。请在函数定义中加入形如

| 0 :: rest -> ...

的分支来实现这一行为。最后得到的函数应该以怎样的方式调用？

2.6 取出 Continuation

请看以下表达式。

shift (fun k -> k)

这个表达式求值时按下列步骤进行：

1. 清除当前的 delimited continuation，
2. 把它绑定到参数 k 上，
3. 并执行 k。

由于执行 k 就只是返回 k（即捕获的 continuation）的值，而当前的 continuation 在第一步被清除了，外围的 reset 的返回值就会变成 k。即，执行 shift (fun k -> k) 就能以一个函数的形式提取出当前的 continuation。

来具体地尝试一下吧。如果想要得到 $3 + [5 * 2] - 1$ 的 continuation，我们可以把整个表达式放进 reset 里，并把 $[~\cdot~]$ 的部分换成 shift (fun k -> k)，最后把返回值绑定到一个变量上。

# let f x = reset (fun () -> 3 + shift (fun k -> k) - 1) x ;;
f : int -> int = <fun>
#

这里返回的值是一个（表示 continuation 的）函数，所以我们显式地引入了参数 x。实际上像下面这样不写明参数也是可以的。

# let f = reset (fun () -> 3 + shift (fun k -> k) - 1) ;;
f : int => int = <fun>
#

但是，这样的话 f 的右手边就不再是一个普通的值，而是 reset，所以我们得到的函数 f 的 answer type 就成了弱多态的〔weak polymorphic，单一的某个未知类型〕。（这是因为 OchaCaml 的 value restriction）。这样的特殊函数在 OchaCaml 中用 => 符号表示。（详见 3.4 节。）虽然这里弱多态没有太大影响，但显式地指定参数就能避免这个问题。

那么，这里就（以函数形式）得到了 $3 + [~\cdot~] - 1$ 这一 continuation，即 f。把一个值（比如 $10$）传给这个函数，它就会以这个值作为 $[~\cdot~]$ 部分的计算结果来进行之后的计算。

# f 10 ;;
- : int = 12
#

这里的 f 就等同于 fun x -> reset (fun () -> 3 + x - 1)。

练习问题 5 请在下列表达式的 $[~\cdot~]$ 处填入 shift (fun k -> k)，取出它们的 continuation。得到的 continuation 执行什么操作？请尝试用不同的值调用它们。这些 continuation 的类型分别是什么？

1. reset (fun () -> 5 * ([·] + 3 * 4))
2. reset (fun () -> (if [·] then "hello" else "hi") ^ " world")
3. reset (fun () -> fst (let x = [·] in (x, x)))
4. reset (fun () -> string_length ("x" ^ string_of_int [·]))

练习问题 6 请看以下函数。它递归地遍历得到的列表，但不做任何改变地返回原列表。即，它是列表的一个恒等函数。

(* id : 'a list -> 'a list *)
let rec id lst = match lst with
    [] -> []
  | first :: rest -> first :: id rest ;;

现在，以 [1; 2; 3] 作为参数，用以下方式调用该函数。

reset (fun () -> id [1; 2; 3]) ;;

递归遍历的最后，参数 lst 的值就是空列表 []。此时的函数 id 也即将返回一个空列表。那么，此时的 continuation 是怎样的？它的类型是什么？请把函数定义中的 [] 换为 shift (fun k -> k)，实际确认一下你的答案。

2.7 保存 Continuation

可以自由地取出 continuation，就可以暂时中断并随时恢复程序的运行。例如，我们来看以下的树结构。

type tree_t = Empty
            | Node of tree_t * int * tree_t ;;

可以像这样从左到右地深度优先遍历这棵树：

(* walk : tree_t -> unit *)
let rec walk tree = match tree with
  Empty -> ()
  | Node (t1, n, t2) ->
      walk t1;
      print_int n;
      walk t2

这是一个按访问到 Node 的顺序显示 Node 的值的函数。运行效果如下。

# let tree1 = Node (Node (Empty, 1, Empty), 2, Node (Empty, 3, Empty)) ;;
tree1 : tree_t = Node (Node (Empty, 1, Empty), 2, Node (Empty, 3, Empty))
# walk tree1 ;;
123- : unit = ()

这个函数一次遍历完整棵树所有的节点。如果想要每次访问到 Node 时暂时停止运行，处理得到的值后再继续遍历的话，可以这样写：

let rec walk tree = match tree with
    Empty -> ()
  | Node (t1, n, t2) ->
      walk t1;
      yield n;
      walk t2 ;;

其中，yield 定义如下：

(* yield : int => unit *)
let yield n = shift (fun k -> Next (n, k)) ;;

这样修改之后，函数 walk 在遇到 Node 时就会中断执行，把 n 的值和当前的 continuation k 放入 Next 中返回。因此，对于调用方而言，Node 的值 n 立刻返回（此时遍历中断）。需要下一个值时，以 () 为参数调用 k 即可。此时，walk 中的 yield 得到值 ()，walk 继续运行下去。像这样，通过把 continuation 包装在数据结构中返回，就能暂停和恢复函数的运行。

修改后的 walk 因为内部存在 shift，必须在 reset 内调用。但是，仅仅像

reset (fun () -> walk tree1) ;;

这样写的话就会出现类型错误。这是因为，walk 找到 Node 时返回 Next (n, k)，而参数 tree1 是空树时 walk 返回的是 ()。结果，如上直接用 reset 包装 walk 的调用时，reset 的返回值有 () 和 Next (n, k) 两种可能，就出现了类型错误。

为了回避类型错误，我们可以加入表示「已经没有下一个 Node 了」的 Done。然后，不使用 ()，而是以 Done 作为 reset 的最后结果。

(* start : tree_t -> 'a result_t *)
let start tree =
  reset (fun () -> walk tree; Done) ;;

可以看到，reset 的返回类型会受到它内部深处的 yield 中的 shift 的影响。为了给出这样的包含 shift 的程序的类型，必须要确定外围的 reset 的类型（answer type）。

到了这里，需要定义的就只剩下 Next 和 Done 了。它们的定义如下。

type 'a result_t = Done
                 | Next of int * (unit / 'a -> 'a result_t / 'a) ;;

Done 没有参数，而 Next 则以 Node 的值（一个整数）和一个 continuation 作为参数。continuation 接受 () 作为参数，返回 Done 或者 Next，所以它的类型大致上就是 unit -> 'a result_t。但是，在加入了 shift/reset 的类型系统中，还必须指定它的 answer type。这里我们所捕获的 continuation 的 answer type 是多态的，所以用类型参数 'a 表示。后续章节中会对 answer type 作详细说明。

来看看实际例子吧。下面的函数依序打印 tree 的所有节点的值。

(* print_nodes : tree_t -> unit *)
let print_nodes tree =
  let rec loop r = match r with
      Done -> ()       (* no more nodes *)
    | Next (n, k) ->
        print_int n;   (* print n *)
        loop (k ()) in (* and continue *)
  loop (start tree) ;;

最后一行使用 start 开始对树的遍历，用内部定义的递归函数 loop 处理结果。如果为 Done，则不再有新的 Node 并终止遍历，如果是 Node (n, k)，则对现在的值 n 进行处理后，调用 k 继续遍历。以 tree1 为参数调用该函数的结果如下。

# print_nodes tree1 ;;
123- : unit = ()
#

类似地，下面的函数返回树中所有节点的值的总和。

(* add_tree : tree_t -> int *)
let add_tree tree =
  let rec loop r = match r with
      Done -> 0
    | Next (n, k) -> n + loop (k ()) in
  loop (start tree) ;;

运行效果如下。

# add_tree tree1 ;;
- : int = 6
#

用这样的“中断执行”的思路，我们就能实现协程。下面的练习问题可以认为是其最简单的形式。

练习问题 7 请实现函数 same_fringe。该函数接受两棵 tree_t 类型的树，同时从左到右地深度优先遍历两者，并判断所经过的 Node 中包含的数字是否相同。比如，以下面两棵树作为参数调用 same_fringe 则返回 true。

let tree1 = Node (Node (Empty, 1, Empty), 2, Node (Empty, 3, Empty)) ;;
let tree2 = Node (Empty, 1, Node (Empty, 2, Node (Empty, 3, Empty))) ;;

虽然先把两棵树展开成列表来判断就会很简单，但这样的实现即使两个输入在第一个值上就不同也不得不先完整地遍历展开它们。相反，请实现一个在发现两者有不同的第一时间就返回 false 的函数。

2.8 包装 Continuation：printf

把值传给 shift 取到的 k，就可以运行 k 中保存的 continuation。但除了直接运行它，我们还可以把 k 的调用放进 fun 中来推迟之后的计算的执行。并且，这使得我们可以从内部访问到 reset 外的参数。

以下面的表达式为例：

shift (fun k -> fun () -> k "hello")

它把当前的 continuation 作为 k 取出，并暂停了程序的运行。然后，返回 thunk（无参函数）fun () -> k "hello" 作为外围的 reset 的值。从 reset 外接收到参数 () 时，它以 "hello" 为值恢复程序的运行。

把这个表达式填入 [ ] ^ "world" 中，则暂时停止了它之后的程序运行而返回一个 thunk。¹

# let f x = reset (fun () ->
              shift (fun k -> fun () -> k "hello") ^ " world") x ;;
f : unit -> string = <fun>
#

这个 thunk 接收到 () 时以 "hello" 为 shift 表达式的值恢复程序的运行，所以结果如下。

# f () ;;
- : string = "hello world"
#

可以看到，这里 thunk 写在 reset （很深的）内部，而 () 则是从 reset 外部传入的。

shift (fun k -> fun () -> k "hello")

像这样，在 shift 中用函数包装 continuation 并返回该函数，就能够访问到 reset 外侧的信息。使用这种方式，我们可以实现带类型的 printf 函数²。

练习问题 8 在以下表达式 [...] 的部分填入 "world"，就能得到字符串 "hello world!"。

reset (fun () -> "hello " ^ [...] ^ "!")

那么，要填入怎样的表达式才能让 reset 外的参数进入 [...] 中呢？ 换言之，如何实现如下的交互？

# reset (fun () -> "hello " ^ [...] ^ "!") "world" ;;
- : string = "hello world!"
#

可以认为这里的 [...] 和〔printf 中的〕%s 是类似的。进一步地，如果要（像 %d 一样）接收整数参数，并将它插入到输出字符串中的话又应该怎样做呢？（用函数 string_of_int 把整数转换为字符串。）最后，能传递多个参数吗？（请注意 OchaCaml 对参数求值的顺序是从右到左的。）

2.9 Answer Type 的变化

现在我们可以思考一下含有 shift/reset 的表达式的类型是怎样确定的。

reset (fun () -> [...] ^ " world")

这个 continuation 的返回值（reset 的值）应当是 ^ 的计算结果，也就是一个字符串。但是，在printf 的例子里我们把参数 "hello" 传给了这个「字符串」。那么，为什么没有产生类型错误呢？

为了理解 printf 的例子的具体类型，我们需要知道什么是 answer type。Answer type 就是包围当前要运行的表达式的 reset 的返回类型。比如表达式 reset (fun () -> 3 + [5 * 2]) 的 answer type 就是 int，表达式 reset (fun () -> string_of_int [5 * 2]) 的 answer type 就是 string。

当前要执行的表达式不含有 shift 的情况下，只要 hole 的类型合适就能（和整体返回的类型无关地）放入任何上下文中。上面的例子里，$5 * 2$ 这一表达式既能放进 reset (fun () -> 3 + [...]) 中，也能放进 reset (fun () -> string_of_int [...]) 中。也就是说，它的 answer type 是多态的（任意的）。

但如果当前要执行的表达式中含有 shift，情况就变得不同了。因为 shift 以新的表达式（即 shift 的内容）取代当前（直到最近的 reset 为止）的 continuation，reset 的返回值的类型可能和原本不同。请再次考虑以下的 continuation。

reset (fun () -> [...] ^ " world")

它原本以字符串作为 reset 的返回值。因此，它的类型是 string -> string。那么，我们尝试在 [...] 中放入下面的表达式。

shift (fun k -> fun () -> k "hello")

此时，从外围的 reset 中返回来的是一个 thunk。因为 thunk 之中的 k 的类型是 string -> string，返回的 thunk 的类型就是 unit -> string。总的来说，原本这个 reset 要返回的是一个 string 类型的值，但因为执行了含有 shift 的表达式，实际的返回值类型变成了 unit -> string。这个现象被称作 answer type 的变化，也是上面的例子能接受参数 () 的原因。

因为这样的含有 shift 的表达式执行时可以改变外围 reset 的类型，在含有 shift/reset 的语言中推导类型时必须时时记录 answer type 和它的变化。OchaCaml 的类型推导就是这样实现的。详见 3.4 节。

2.10 包装 Continuation：State Monad

用函数包装 continuation 的调用就可以访问到 reset 外的参数。应用这个方法，我们可以实现对「状态」的支持。

现在，我们考虑以一个整数作为状态的情况。为此，要把一个整数（像 printf 例子里的 "world" 一样）作为参数传给 reset。

reset (fun () -> M) 3

这个例子中，状态的初始值是 $3$。在 M 中，可以通过如下函数访问这个状态。

# let get () =
    shift (fun k -> fun state -> k state state) ;;
get : unit => 'a = <fun>
#

get 用 shift 捕获当前的 continuation 之后中断执行，使外围的 reset 返回 fun state -> k state state。因为 reset 接收的参数 $3$ 赋给了变量 state，state 随后被传给了 k，最后就以 state 为 get 的值继续程序的执行。

这里第二次把 state 传给 k 是为了设置 k 执行时的状态的值。shift 所捕获到的 continuation 也包含外围的 reset，所以调用 k state 之后，之后的计算也是在 reset 中进行的〔k state 相当于 reset (fun () -> 剩下的部分)〕。为了在其中再次使用 get，我们重新把状态传给它。由于 get 不改变状态的值，这里就原样传递 state。如果想要达到运行后改变状态的值的效果，这里传入新的值就可以了。比如，下面的函数把当前状态的值加 $1$ 并返回 ()。

# let tick () =
    shift (fun k -> fun state -> k () (state + 1)) ;;
tick : unit => unit = <fun>
#

可以使用如下的函数开始计算。

# let run_state thunk =
    reset (fun () -> let result = thunk () in
                     fun state -> result) 0 ;;
run_state : (unit => 'a) => 'b = <fun>
#

这个函数执行接收到的 thunk，并以 $0$ 为初始的状态。thunk 的执行结束后，无视此时的 state，返回结果 result。

实际运行效果如下。

# run_state (fun () ->
    tick (); (* state = 1 *)
    tick (); (* state = 2 *)
    let a = get () in
    tick (); (* state = 3 *)
    get () - a) ;;
- : int = 1
#

练习问题 9 以下程序的执行结果是什么？

run_state (fun () ->
  (tick (); get ()) - (tick (); get ())) ;;

请实际运行确认一下。（注意 OchaCaml 的求值顺序。）〔++i - ++i 是吧〕

练习问题 10 类似地，请写出变更状态的函数 put。调用 put x，则把状态的值变为 x 并返回 ()。

如上，我们使用 continuation 实现了 state monad 的功能。

2.11 使用 Continuation 改变运算顺序（高阶）

在非尾调用位置调用 k，我们就可以在 continuation 执行结束后进行额外的计算。也就是说，我们可以反转外部和内部的计算的执行顺序。比如，

# reset (fun () -> 1 + (shift (fun k -> 2 * k 3))) ;;
- : int = 8
#

以上表达式执行时，作为上下文的 1 + [...] 和内部的 2 * [...] 的计算顺序互换了。这里，$3$ 先加上 $1$ 之后才乘以 $2$。使用这种方式，我们可以实现 λ 演算的 A-normalization。

请看如下的 λ 项定义。

type term_t = Var of string
            | Lam of string * term_t
            | App of term_t * term_t ;;

接下来，我们尝试实现 A-normalization。A-normalization 是为 λ 项中每个函数应用绑定唯一的名字，并保持与原项等价的变换。比如，对 $S$ 组合子 $\lambda x.\lambda y.\lambda z.(xz)(yz)$ 进行 A-normalization 的结果如下。

为了实现它，我们先定义一个遍历所有 λ 项并原样重新构建的恒等函数。

(* id_term : term_t -> term_t *)
let rec id_term term = match term with
    Var (x) -> Var (x)
  | Lam (x, t) -> Lam (x, id_term t)
  | App (t1, t2) -> App (id_term t1, id_term t2) ;;

现在，因为目标是给所有的函数调用加上名字，我们略微修改最后一个分支，给每个 App 加上一个 let：

(* id_term' : term_t -> term_t *)
let rec id_term' term = match term with
    Var (x) -> Var (x)
  | Lam (x, t) -> Lam (x, id_term' t)
  | App (t1, t2) ->
      let t = gensym () in   (* generate fresh variable *)
      App (Lam (t, Var (t)), (* let expression *)
           App (id_term' t1, id_term' t2)) ;;

由于我们的 λ 项定义中没有 let，这里用和 $\mathsf{let}~t = M~\mathsf{in}~N$ 等价的形式 $(\lambda t.N) M$ 代替。使用上述函数对 $S$ 组合子做变换可以得到以下结果。

这就不太对了。它确实给了每个函数调用一个名字，但结果里的 let 嵌套起来了。所以我们需要想办法把它展平。

假设我们正在使用 id_term' 对 $S$ 组合子进行变换，并且目前正好变换到第一个函数调用 $xz$ 处。当前的 continuation 如下所示，也就是「对 $yz$ 进行变换，在外面构造一个函数调用，最后包上 3 层 λ」：

为了展平所有的 let，我们需要把当前为 $xz$ 构造 let 的计算（也就是 $\mathsf{let}~t_2 = xz~\mathsf{in}~[\,\cdot\,]$）和它外部直到 λ 之前的构造过程（$\mathsf{let}~t_1 = [\,\cdot\,](\mathsf{let}~t_3 = yz~\mathsf{in}~t_3)~\mathsf{in}~t_1$）互换。方式如下。

(* a_normal : term_t => term_t *)
let rec a_normal term = match term with
    Var (x) -> Var (x)
  | Lam (x, t) -> Lam (x, reset (fun () -> a_normal t))
  | App (t1, t2) ->
      shift (fun k ->
        let t = gensym () in    (* generate fresh variable *)
        App (Lam (t,            (* let expression *)
                  k (Var (t))), (* continue with new variable *)
             App (a_normal t1, a_normal t2))) ;;

请看最后的 App 分支。我们以新生成的变量 t 为参数调用当前的 continuation k。通过这种方式，我们把原项的 App 转移给了新生成的变量。当整个项的变换完成之后，才把 t 的定义加在最前面。

为了避免新变量的定义超过 Lam 的作用域，在 Lam 分支中加入 reset。这样我们就得到了 A-normalization 的一个完整实现。这个方法在部分求值的领域称作 let insertion。

练习问题 11 使用上述的 A-nomalization，实际地变换一下 $S$ 组合子试试吧。结果是怎样的？

2.12 复制 Continuation

目前为止的每个例子都只使用了捕获到的 continuation 1 次。如果多次调用，则可以多次地执行之后的计算。通过这种方式我们可以实现回溯。

请看以下函数。

(* either : 'a -> 'a -> 'a *)
let either a b =
  shift (fun k -> k a; k b) ;;

函数 either 被调用时，捕获当前的 continuation k，并先后以 a、b 为参数调用它。也就是说，调用时，它分别以 a、b 为值执行之后的计算 2 次。执行下面的程序，我们可以看到，either 之后的计算（打印 x 和换行）确实被执行了 2 次。

# reset (fun () ->
    let x = either 0 1 in
    print_int x;
    print_newline ()) ;;
0
1
- : unit = ()
#

练习问题 12 不固定参数数量为 2 个，而是接受一个列表作为参数的话，就可以接受任意数量的值了。请实现以一个列表作为参数，并按顺序返回其中每个元素到当前的 continuation 中的函数 choice。

使用函数 either，可以简单地实现在不知道哪个值正确的情况下，把两边都尝试一次的 generate and test 风格的程序。比如，假设我们有 $P$ 和 $Q$ 两个布尔变量，想知道如下的逻辑公式能否被满足：

因为 $P$ 和 $Q$ 都可能是 true 或 false，我们可以写出如下程序。

# reset (fun () ->
    let p = either true false in
    let q = either true false in
    if (p || q) && (p || not q) && (not p || not q)
    then (print_string (string_of_bool p);
          print_string ", ";
          print_string (string_of_bool q);
          print_newline ())) ;;
true, false
- : unit = ()  
#

可以看到，这个程序表面看起来是一个没有循环也没有回溯的顺序执行程序，只是定义变量了 p 和 q，并检查它们是否满足这个逻辑表达式。但实际上，因为函数 either 将之后的计算运行 2 次，程序里的 if 一共运行了 4 次。可以把 either 看做是非确定性地从参数 a、b 中选择一个的函数。

练习问题 13 请使用上个练习中实现的 choice 定义一个搜索 1 到 5 之间三个满足勾股定理的自然数的函数。换言之，请找到三个自然数 $1 \le x, y, z \le 5$，满足条件 $x^2 + y^2 = z^2$。

那么第二节的内容就到这里。

第三节：

Spore：【译】shift/reset 编程入门 (3)：理论

参考