伴随求值

伴随求值是一种类型论, 它将类型分为两类:

•	值类型, 当我们描述它们的实例时, 我们描述它们的构造本身, 换言之它以构造规则为主, 极性为正,

•	计算类型, 当我们描述它们的实例时, 我们描述对于来自外部的输入, 它们如何响应. 换言之这些类型以消去规则为主, 极性为负.

借助这种分层, 计算单子可以被解构成一对伴随.

类似伴随逻辑把命题分为两类, 并且给出一对互相转换的逻辑连接词, 伴随求值也给出了互相转换的连接词. 但与之不同的是, 伴随求值在语法上就区分计算类型和值类型, 并且一般只考虑两类类型.

伴随求值的表达式也随着类型被分类, 但表达式比起类型还多了一种: 栈. 这意味着伴随求值中有三类不同的判断.

1语法

由于伴随求值的框架非常可扩展, 全面地考虑所有可能的类型并不现实, 这里只考虑单位类型、积类型、无交并类型、函数类型这几个基本的类型构造. 值类型和计算类型的语法使用形式语言定义如下:

$$\begin{array}{rl}A& ::=\top \mid A_1\otimes A_2\mid A_1+A_2\mid U(X)\\ X& ::=X_1\times X_2\mid A_1\rightharpoonup X_2\mid F(A)\end{array}$$

其中, $\otimes$ 和 $\times$ 类似积类型, $+$ 类似无交并类型, $\rightharpoonup$ 类似函数类型, 剩下 $U$ 类似伴随逻辑中的 $\uparrow$, $F$ 类似 $\downarrow$.

$\otimes$ 和 $\times$ 非常类似线性逻辑中的 $\otimes$ 和 $\&$, 前者是值, 换言之它的实例是两个值放在一起; 后者是计算, 它的实例包含两个计算, 对它来说外部输入就是对这两个计算中的一个进行一次选择, 然后它的响应方式就是执行该选择.

伴随求值中最核心的类型就是 $F$ 和 $U$ 了. 对于计算 $C$, $F(C)$ 表示类型为 $C$ 的计算的代码, 这个代码可以像值一样被传递、被放进其它的值进行组合, 也可以被恢复成计算并执行. 对于值 $A$, $U(A)$ 表示最终会给出类型为 $A$ 的结果的一段计算.

表达式的语法定义如下:

$$\begin{array}{rl}V::=& x\mid ★\mid V_1\otimes V_2\mid \mathrm{inl}{V}_1\mid \mathrm{inr}{V}_2\mid \mathrm{暂停}(C)\\ C::=& \mathrm{ret}(V)\mid \mathrm{bind}(C_1;x.C_2)\mid ⟨C_1,C_2⟩\mid C.1\mid C.2\mid \\ & \lambda x.C\mid \mathrm{ap}(C;V)\mid \mathrm{执行}(V)\mid {\mathrm{rec}}_{\top }V\{C\}\mid \\ & {\mathrm{rec}}_{\otimes }V\{x_1,x_2.C\}\mid {\mathrm{rec}}_{+}V\{x.C_1\mid x.C_2\}\end{array}$$

其中 $\mathrm{暂停}$ 和 $\mathrm{执行}$ 是 $F$ 的规则, $\mathrm{ret}$ 和 $\mathrm{bind}$ 是 $U$ 的规则.

2类型规则

针对计算和值, 分别有两类判断来处理它们:

•	计算的判断 $\Gamma ⊢V:A$,
•	值的判断 $\Gamma ⊢C:X$.

其中, 语境 $\Gamma$ 是一组值类型. 这至关重要, 因为语境决定了变量的类型和替换操作里面能传入什么样的数据. 既然语境里面都是值类型, 那么变量的类型都是值类型.

针对值类型, 有如下规则:

$$\frac{}{\Gamma ,x:A⊢x:A}\frac{}{\Gamma ⊢★:\top }\frac{\Gamma ⊢V_1:A_1\Gamma ⊢V_2:A_2}{\Gamma ⊢V_1\otimes V_2:A_1\otimes A_2}$$$$\frac{\Gamma ⊢V:A}{\Gamma ⊢\mathrm{inl}V:A+A^{\prime }}\frac{\Gamma ⊢V:A}{\Gamma ⊢\mathrm{inr}V:A^{\prime }+A}\frac{\Gamma ⊢C:X}{\Gamma ⊢\mathrm{暂停}(C):U(X)}$$

针对计算类型, 有如下规则:

$$\frac{\Gamma ⊢V:U(X)}{\Gamma ⊢\mathrm{执行}(V):X}\frac{\Gamma ⊢V:\top \Gamma ⊢C:X}{\Gamma ⊢{\mathrm{rec}}_{\top }V\{C\}:X}$$$$\frac{\Gamma ⊢V:A}{\Gamma ⊢\mathrm{ret}(V):F(A)}\frac{\Gamma ⊢C:F(A)\Gamma ,x:A⊢C^{\prime }:X}{\Gamma ⊢\mathrm{bind}(C;x.C^{\prime }):X}$$$$\frac{\Gamma ⊢C_1:X_1\Gamma ⊢C_2:X_2}{\Gamma ⊢⟨C_1,C_2⟩:X_1\times X_2}\frac{\Gamma ⊢C:X_1\times X_2}{\Gamma ⊢C.1:X_1}\frac{\Gamma ⊢C:X_1\times X_2}{\Gamma ⊢C.2:X_2}$$$$\frac{\Gamma ,x:A⊢C:X}{\Gamma ⊢(\lambda x.C):A\rightharpoonup X}\frac{\Gamma ⊢C:A\rightharpoonup X\Gamma ⊢V:A}{\Gamma ⊢\mathrm{ap}(C;V):X}$$$$\frac{\Gamma ⊢V:A_1\otimes A_2\Gamma ,x_1:A_1,x_2:A_2⊢C:X}{\Gamma ⊢{\mathrm{rec}}_{\otimes }V\{x_1,x_2.C\}:X}$$$$\frac{\Gamma ⊢V:A_1+A_2\Gamma ,x:A_1⊢C_1:X\Gamma ,x:A_2⊢C_2:X}{\Gamma ⊢{\mathrm{rec}}_{+}V\{x.C_1\mid x.C_2\}:X}$$

3语义

除了表达式的类型规则, 为了描述语义, 需要引入栈的概念, 及其对应的判断, 如下所示:

$$\Gamma \mid C{X}_{1}K{X}_2$$

它有前提条件 $\Gamma ⊢C:X_1$ 必须成立. 栈表示 “接下来需要进行的计算”. 这个判断的意思是在语境 $\Gamma$ 中, 我们拿着 $C:X_1$, 在执行完 $C$ 后还要把它的结果传递给 $K$ 完成接下来的计算, 最后给出的结果类型为 $X_2$.

根据 $C$ 的不同, 对栈的操作有两种可能:

•	入栈: 将 $C$ 的一部分拆下来放进 $K$,
•	出栈: 把 $K$ 顶部的数据取出并和 $C$ 结合.

操作语义

范畴语义

在范畴论中解释伴随求值需要分别解释值类型和计算类型. 其中值类型的解释非常类似 Curry–Howard–Lambek 对应中对简单类型 $\lambda$ 演算的解释, 接下来我们把这个范畴记作 $\mathsf{Ctx}$.

需要注意的是, 简单类型 $\lambda$ 演算对应积闭范畴再加上余积, 但对于前文介绍的伴随求值来说这会多出来一些构造, 比如语法里没有值到值的函数, 因此没有指数对象的直接对应物, 但给伴随求值加上这个类型很容易, 所以这种事情可以忽略.

计算类型的解释则相对复杂一些. 我们不直接解释计算类型的实例 $C$, 而是解释栈. 考虑栈的判断 $\Gamma \mid C{X}_{1}K{X}_2$, 由于栈处理一个计算 $C$, 可以把 $C$ 的类型 $X_1$ 视为栈的输入、$X_2$ 视为其输出, 那么这可以看作一个计算类型 $X_1,X_2$ 之间的态射. 注意这里还有值类型构成的语境 $\Gamma$, 因此计算类型的范畴和值类型的范畴构成范畴族, 其中值类型的范畴是指标. 具体来说, 计算类型的范畴是局部 $\mathsf{Ctx}$-范畴族, 定义如下.

定义 3.1. 局部 $\mathsf{Ctx}$-范畴族是$1$-函子 $F:\mathsf{Ctx}\to \mathsf{Cat}$ (换言之这是严格的范畴族), 满足如下条件:

•	对于 $f\in \mathsf{Ctx}(x,y)$, 它诱导的函子 $F(f):F(x)\to F(y)$ 在对象上是恒同映射.

局部 $\mathsf{Ctx}$-范畴族是一种严格的局部常纤维范畴.

由于伴随求值中替换操作不改变类型, 因此我们要求对应替换操作的函子在对象上恒同, 但它不一定在态射上恒同, 这是因为替换操作可能会改变栈. 计算类型的范畴中, 恒同态射对应空的栈, 态射复合对应栈的拼接.

4参考文献

•	Paul Blain Levy (2001). “Call-By-Push-Value”. (web)
•	Robert Harper (2024). “Call-By-Push-Value and the Enriched Effect Calculus”. (web)

术语翻译

伴随求值 • 英文 call-by-push-value

栈 • 英文 stack

入栈 • 英文 push

出栈 • 英文 pop