第二节：

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

3 Delimited Continuation 操作符的理论基础

本节对 delimited continuation 操作符 shift/reset 的理论基础进行概述。我们使用的语言是一个从左到右求值1的 call-by-value λ 演算，并加入了多态的 let 和 shift/reset 操作符。

3.1 语法

$$\begin{alignat}{1} \text{(value)}& \quad V& \quad::=&\quad x \ | \ \lambda x. M \\ \text{(term)}& \quad M& \quad::=&\quad V \ | \ M~M \ | \ \mathsf{let}~x = M~\mathsf{in}~M \ | \ \mathcal{S}k.M \ | \ \langle M \rangle \\ \text{(pure evaluation context)}& \quad F& \quad::=&\quad [~] \ | \ F~M \ | \ V~F \ | \ \mathsf{let}~x = F~\mathsf{in}~M \\ \text{(evaluation context)}& \quad E& \quad::= &\quad [~] \ | \ E~M \ | \ V~E \ | \ \mathsf{let}~x = E~\mathsf{in}~M \ | \ \langle E \rangle \end{alignat} \\$$

其中，shift (fun k -> M) 记作 $\mathcal{S}k.M$，reset (fun () -> M) 记作 $\langle M \rangle$。Evaluation context 分为两种，hole $[~]$ 外没有 reset 时即为 pure evaluation context。

3.2 归约规则

$$ \begin{align} (\lambda x.M)~V \enspace &\leadsto \enspace M[x := V] \\ \mathsf{let}~x = V~\mathsf{in}~M \enspace &\leadsto \enspace M[x := V] \\ \langle V \rangle \enspace &\leadsto \enspace V \\ \langle F[\mathcal{S}~V] \rangle \enspace &\leadsto \enspace \langle V (\lambda x. \langle F[x] \rangle) \rangle \quad x \text{ is fresh} \end{align} \\$$

前两条规则是普通 λ 演算的 β-归约，第三条规则表示 reset 内部只有一个值时可以去除 reset，最后一条规则意为下一个要执行的表达式是 shift 的情况下，取出当前直到最近的 reset 的 continuation。这个 continuation 用 pure evaluation context $F[~]$ 表示。它被变换成函数 $\lambda x. \langle F[x] \rangle$ 并传递给 $V$。请注意右手边的结果中，外围的 reset 保留了下来，并且取出的 continuation 的周围也有 reset。（这两点任意一点有不同时，得到的就是其他的 delimited continuation 操作符。）

3.3 求值规则和求值顺序

求值规则定义如下：

$$ E[M] \quad \to \quad E[M'] \quad \text{if} \quad M \quad \leadsto \quad M' \\$$

根据 evaluation context 的定义，求值顺序从左到右（函数部分先于参数部分）。

求值过程可以分为以下三步。

  1. 待求值的表达式已经是一个值的情况下，以这个值作为求值结果。否则，就将它分解成 $E[M]$ 的形式。这里的 $M$ 表示一个 redex。
  2. 根据归约规则把 $M$ 归约成 $M'$。
  3. 把 $M'$ 放回原来的 evaluation context，得到结果 $E[M']$。这就是单步归约之后的表达式了。

3.4 类型规则

类型和 type scheme 定义如下，其中 $t$ 表示类型变量。

$$ \begin{alignat}{1} \text{type}& \quad \tau \quad &::= \quad t\ |\ \tau/\tau \to \tau/\tau \\ \text{type scheme}& \quad \sigma \quad &::= \quad \tau\ |\ \forall t. \sigma \end{alignat} \\$$

这里 $\tau_1/\alpha \to \tau_2/\beta$ 表示一个输入类型为 $\tau_1$，输出类型为 $\tau_2$，并且执行时 answer type 从 $\alpha$ 变化为 $\beta$ 的函数2。若函数不包含 control effect（即不使用 shift），则 $\alpha$ 和 $\beta$ 就是同一类型。这样的函数被称为 pure 函数。Answer type 可以是多态的。Answer type 的相关内容请看下一节。

OchaCaml 中，pure 函数的类型省略了 answer type，显示为 $\tau_1 \texttt{ -> } \tau_2$。（含有 shift 的）非 pure 的函数默认也省略了 answer type，但为了表明 answer type 不是多态的，显示为 $\tau_1 \texttt{ => } \tau_2$。 若想要看到所有的 answer type，可以使用指令 #answer "all";;。之后非 pure 函数的类型显示为$\tau_1 \texttt{ / } \alpha \texttt{ -> } \tau_2 \texttt{ / } \beta$。

类型断言的形式如下。

$$ \displaylines{ \Gamma \vdash_p M : \tau \\ \Gamma,\alpha \vdash M : \tau, \beta } \\$$

前者表示「类型环境 $\Gamma$ 中，表达式 $M$ 是 pure 的并有类型 $\tau$」，后者表示「类型环境 $\Gamma$ 中，表达式 $M$ 有类型 $\tau$，并且执行 $M$ 时 answer type 由 $\alpha$ 变为 $\beta$」。可以给出如下的类型规则。

$$\displaylines{ \frac {(x : \sigma) \in \Gamma \quad \sigma \succ \tau} {\Gamma \vdash_p x : \tau} \ \text{(var)} \quad \frac {\Gamma, x : \tau_1, \alpha \vdash M : \tau_2, \beta} {\Gamma \vdash_p \lambda x. M : \tau_1/\alpha \to \tau_2/\beta} \ \text{(fun)} \\ \frac { \Gamma, \gamma \vdash M_1 : \tau_1/\alpha \to \tau_2/\beta, \delta \quad \Gamma, \beta \vdash M_2 : \tau_1, \gamma } {\Gamma, \alpha \vdash M_1\,M_2 : \tau_2, \delta} \ \text{(app)} \quad \frac {\Gamma \vdash_p M : \tau} {\Gamma, \alpha \vdash M : \tau, \alpha} \ \text{(exp)} \\ \frac { \Gamma \vdash_p M_1 : \tau_1 \quad \Gamma, x : \mathsf{Gen}(\tau_1, \Gamma), \alpha \vdash M_2 : \tau_2, \beta } {\Gamma, \alpha \vdash \mathsf{let}~x = M_1~\mathsf{in}~M_2 : \tau_2, \beta} \ \text{(let)} \\ \frac {\Gamma, k : \forall t. (\tau/t \to \alpha/t), \gamma \vdash M : \gamma, \beta} {\Gamma, \alpha \vdash \mathcal{S}k. M : \tau, \beta} \ \text{(shift)} \quad \frac {\Gamma, \gamma \vdash M : \gamma, \tau} {\Gamma \vdash_p \langle M \rangle : \tau} \ \text{(reset)} } \\$$

这里， $\sigma \succ \tau$ 表示类型 $\tau$ 是 type scheme $\sigma$ 的实例， $\mathsf{Gen}(\tau, \Gamma)$ 则表示一个通过泛化类型 $\tau$ 中不在 $\Gamma$ 中出现的类型变量得到的 type scheme。

3.5 Answer Type

Answer type 就是「当前的上下文的类型」。举例来说会比较清楚。比如，

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

这一表达式中，现在要执行的表达式 [5 * 2] 的类型是 int，环绕这个表达式的上下文 3 + [5 * 2] - 1 整体的类型（在 5 * 2 执行前后都）是 int。因此，5 * 2 的 answer type （两边都）是 int。可以用以下的类型断言表示。

$$\Gamma, \texttt{int} \vdash \texttt{5 * 2} : \texttt{int}, \texttt{int} \\$$

第一个 int 是 5 * 2 执行之前的 answer type（上下文的类型），第二个是 5 * 2 自身的类型，最后的 int 则是 5 * 2 执行之后的 answer type。

上例中现在要执行的表达式的类型和 answer type 恰好相同，但它们不同的情况也是很常见的。比如

reset (fun -> if [2 = 3] then 1 + 2 else 3 - 1)

这个表达式中，现在要执行的表达式 2 = 3 的类型是 bool。同时，上下文的类型是 1 + 2 或者 3 - 1 的类型，也就是 int（2 = 3 执行前后相同）。因此，它的类型断言就是以下的形式。

$$\Gamma, \texttt{int} \vdash \texttt{2 = 3} : \texttt{bool}, \texttt{int} \\$$

虽然要执行的表达式的类型和 answer type 不同是常有的，但 pure 表达式的两个 answer type 必然相同。并且 pure 表达式自身的类型不会受 answer type 的影响，所以可以完全忽略 answer type。

下面请看一个 answer type 发生了变化的例子。

reset (fun () ->
  [shift (fun k -> fun () -> k "hello")] ^ " world")

想直接看出现在要执行的表达式 shift (fun k -> fun () -> k "hello") 的类型可能并不容易，但观察它的周围就很容易确定了。[...] ^ " world" 中 [...] 的结果被传给了 ^，所以 [...] 的部分就该是 string，shift (...) 的类型也就是 string 了。然后，[...] 执行之前的上下文形如 [...] ^ " world"，所以这里的 answer type 也是 string。那么，[...] 执行之后 answer type 会变成怎样呢？执行后，当前的 continuation 被取出并绑定到 k 上，返回的是 fun () -> k "hello" 这个函数。这个函数接受参数 unit 而返回字符串（"hello world"），所以类型大致是 unit -> string。更准确地说，因为每个函数类型都需要指定 answer type，而它又是一个纯函数，它的类型就是 unit / 'a -> string / 'a。因此，类型断言如下。

$$\Gamma, \texttt{string} \vdash \texttt{shift (fun k -> ...)} : \texttt{string}, \texttt{unit / 'a -> string / 'a} \\$$

像这样，使用 shift 时 answer type 会发生各种变化。这个现象叫做 answer type modification。

可以用同样的方式来理解函数的类型。比如，我们来看 2.10 节出现的函数 get。这个函数接受参数 ()，返回现在的状态（一个整数），所以忽略 answer type 的话它的类型就是 unit -> int。我们可以观察 get 使用时的上下文来确定它的 answer type。比如

reset (fun () ->
  let result = [get ()] + 2 * get () in
  fun i -> result)

中，上下文最终返回 fun i -> result，answer type 就是函数类型 int -> int。因为不论是否使用了 get，answer type 都是同样类型的函数，所以 get 的类型就是 unit / (int -> int) -> int / (int -> int)。更准确地说，因为 get 的定义中状态的类型不局限于整数，上下文的类型也可以进行泛化，它的实际类型应该是 unit / ('a / 'b -> 'c / 'd) -> 'a / ('a / 'b -> 'c / 'd)。

像这样，加入了 shift/reset之后就不得不把 answer type 纳入考虑范围了。这相当于始终关注上下文的类型是什么，以及它在执行过程中如何变化。

那么全文内容就到这里。感谢阅读。

参考

  1. 注：不同于 OchaCaml ↩︎

  2. Danvy, O., and A. Filinski “A Functional Abstraction of Typed Contexts,” Technical Report 89/12, DIKU, University of Copenhagen (July 1989). ↩︎