第 17 章：推导编译器（Calculating compilers）
原文：Graham Hutton, Programming in Haskell, Second Edition, Chapter 17。维护者已确认本书可翻译并发布用于学习研究。
在最后一章中，我们展示上一章介绍的推理技术如何用于推导编译器。我们先说明如何通过一系列步骤把某种语言的语义转换为编译器，然后说明如何把这些步骤合并起来，使得编译器可以直接从正确性陈述中推导出来。
17.1 引言（Introduction）
推导编译器的能力，自程序变换领域早期以来就是一个关键目标。给定源语言的高层语义，目标是把这个语义变换为一个编译器，用来把源程序翻译为更低层的目标语言，并得到一个执行目标程序的虚拟机。
这种方法有两个主要优点。首先，编译器、目标语言和虚拟机会在变换过程中系统化地推导出来，而不需要用户手工定义。其次，所得的编译器和虚拟机通常不需要后续的正确性证明，因为它们是按构造正确的。
第 16 章中，我们给出了一个算术表达式编译器，并证明了它的正确性。本章说明如何直接从正确性陈述中推导出这个编译器。我们分两个阶段发展这种方法：先用一系列变换步骤介绍基本思想，然后展示如何把这些独立步骤合并为单个步骤。为简单起见，我们只关注算术表达式，但同样的技术也可以用于推导更复杂语言的编译器。
17.2 语法与语义（Syntax and semantics）
我们以与上一章编译器正确性示例相同的方式开始，给出两个定义，分别捕获一种简单算术表达式语言的语法（形式）和语义（含义）。这种语言由整数值和加法运算符构成：
data Expr = Val Int | Add Expr Expr
eval :: Expr -> Int
eval (Val n) = n
eval (Add x y) = eval x + eval y
例如，表达式 1 + 2 可以如下求值：
eval (Add (Val 1) (Val 2))
= { applying eval }
eval (Val 1) + eval (Val 2)
= { applying the first eval }
1 + eval (Val 2)
= { applying eval }
1 + 2
= { applying + }
3
现在我们说明如何基于这个语义，通过三个变换步骤推导编译器。前两个步骤推广求值函数，最后一步简化所得定义。
17.3 添加栈（Adding a stack）
第一步是把求值函数 eval 转换为使用栈的版本，以便显式呈现参数值的操作。特别地，与其返回一个类型为 Int 的单个值，我们希望定义一个更一般的求值函数 eval'，它额外接收一个整数栈作为参数，并返回一个修改后的栈：这个栈会把表达式的值压入栈顶。更精确地说，如果用整数列表表示栈，其中头部是栈顶元素：
type Stack = [Int]
那么我们希望定义函数：
eval' :: Expr -> Stack -> Stack
并满足下面性质：
eval' e s = eval e : s
我们不先定义 eval'，再通过对表达式 e 归纳证明它满足上面的方程，而是使用上一章介绍的技术，直接计算出满足这个方程的 eval' 定义，并以应用归纳假设的需求作为计算过程的驱动力。在基本情况 Val n 中，计算很容易：
eval' (Val n) s
= { specification of eval' }
eval (Val n) : s
= { applying eval }
n : s
= { define: push n s = n : s }
push n s
注意，在最后一步中，我们定义了一个辅助函数 push，用来捕获把一个数字压入栈的思想。通过上面的计算，我们发现了 eval' 对形如 Val n 的表达式的定义：
eval' (Val n) s = push n s
在归纳情况 Add x y 中，计算如下：
eval' (Add x y) s
= { specification of eval' }
eval (Add x y) : s
= { applying eval }
(eval x + eval y) : s
现在看起来卡住了，因为没有更多定义可以应用。不过，由于我们正在做归纳计算，可以使用两个参数表达式 x 和 y 的归纳假设：
eval' x s' = eval x : s'
eval' y s' = eval y : s'
为了使用这些假设，显然必须把 eval x 和 eval y 的值压入栈。这可以通过引入另一个辅助函数 add 来轻松实现，它捕获把栈顶两个数字相加的思想。剩余计算就很直接：
(eval x + eval y) : s
= { define: add (m : n : s) = n+m : s }
add (eval y : eval x : s)
= { induction hypothesis for x }
add (eval y : eval' x s)
= { induction hypothesis for y }
add (eval' y (eval' x s))
注意，上面先把 eval x 压入栈，再压入 eval y，对应加法从左到右求值参数。反过来压入这些值同样完全有效，那会对应从右到左求值。总之，我们推导出了下面的定义：
eval' :: Expr -> Stack -> Stack
eval' (Val n) s = push n s
eval' (Add x y) s = add (eval' y (eval' x s))
其中：
push :: Int -> Stack -> Stack
push n s = n : s
add :: Stack -> Stack
add (m : n : s) = n+m : s
最后，把空栈 s = [] 代入构造 eval' 时所用的方程 eval' e s = eval e : s，并用函数 head 选择所得单元素栈中的唯一值，就可以从新函数恢复原始求值函数 eval：
eval :: Expr -> Int
eval e = head (eval' e [])
例如，使用这个新定义，1 + 2 的求值现在会先把两个值压入栈，然后再把它们相加：
eval (Add (Val 1) (Val 2))
= { applying eval }
head (eval' (Add (Val 1) (Val 2)) [])
= { applying eval' }
head (add (eval' (Val 2) (eval' (Val 1) [])))
= { applying the inner eval' }
head (add (eval' (Val 2) (push 1 [])))
= { applying eval' }
head (add (push 2 (push 1 [])))
= { applying push }
head (add (2 : 1 : []))
= { applying add }
head (3 : [])
= { applying head }
3
17.4 添加续延（Adding a continuation）
下一步是把基于栈的求值函数 eval' 转换为续延传递风格，从而显式呈现控制流。特别地，我们希望定义一个更一般的求值函数 eval''，它额外接收一个从栈到栈的函数（续延）作为参数；这个续延用于处理表达式求值之后得到的栈。更精确地说，如果定义续延类型：
type Cont = Stack -> Stack
那么我们希望定义函数：
eval'' :: Expr -> Cont -> Cont
使得：
eval'' e c s = c (eval' e s)
我们通过对表达式 e 归纳，直接从这个方程计算 eval'' 的定义。基本情况再次很简单：
eval'' (Val n) c s
= { specification of eval'' }
c (eval' (Val n) s)
= { applying eval' }
c (push n s)
归纳情况则计算如下：
eval'' (Add x y) c s
= { specification of eval'' }
c (eval' (Add x y) s)
= { applying eval' }
c (add (eval' y (eval' x s)))
= { unapplying . }
(c . add) (eval' y (eval' x s))
= { induction hypothesis for y }
eval'' y (c . add) (eval' x s)
= { induction hypothesis for x }
eval'' x (eval'' y (c . add)) s
总之，我们推导出了下面的定义：
eval'' :: Expr -> Cont -> Cont
eval'' (Val n) c s = c (push n s)
eval'' (Add x y) c s = eval'' x (eval'' y (c . add)) s
把恒等续延 c = id 代入构造 eval'' 时所用的方程 eval'' e c s = c (eval' e s)，就可以恢复前一个求值函数 eval'：
eval' :: Expr -> Cont
eval' e s = eval'' e id s
例如，1 + 2 的求值现在会在第一个参数求值完成后，把控制转交给第二个参数的求值：
eval' (Add (Val 1) (Val 2)) []
= { applying eval' }
eval'' (Add (Val 1) (Val 2)) id []
= { applying eval'' }
eval'' (Val 1) (eval'' (Val 2) (id . add)) []
= { applying the outer eval'' }
eval'' (Val 2) (id . add) (push 1 [])
= { applying eval'' }
(id . add) (push 2 (push 1 []))
= { applying . }
id (add (push 2 (push 1 [])))
= { applying push }
id (add (2 : 1 : []))
= { applying add }
id [3]
= { applying id }
[3]
17.5 去函数化（Defunctionalising）
第三步也是最后一步，是使用去函数化把求值函数转换回一阶风格。特别地，我们不再使用类型为 Cont = Stack -> Stack 的函数作为参数传递和作为结果返回，而是定义一个新类型，用来表示求值函数实际需要的那些具体续延形式。
在 eval' 和 eval'' 的定义中，只使用了三种续延形式：一种用于停止求值过程，一种用于把数字压入栈顶，一种用于把栈顶两个数字相加。我们先把这三种形式分离出来，为它们命名，并把变量作为参数传递。也就是说，我们定义三个组合子，用来构造所需续延形式：
haltC :: Cont
haltC = id
pushC :: Int -> Cont -> Cont
pushC n c = c . push n
addC :: Cont -> Cont
addC c = c . add
使用这些组合子，求值器现在可以重写如下：
eval' :: Expr -> Cont
eval' e = eval'' e haltC
eval'' :: Expr -> Cont -> Cont
eval'' (Val n) c = pushC n c
eval'' (Add x y) c = eval'' x (eval'' y (addC c))
通过展开定义，很容易检查这些定义与前面的版本等价。应用去函数化的下一步，是定义一个新类型 Code，其构造子表示这三个组合子：
data Code = HALT | PUSH Int Code | ADD Code
deriving Show
这个类型的构造子与对应组合子具有相同类型，只是新类型 Code 现在扮演 Cont 的角色：
HALT :: Code
PUSH :: Int -> Code -> Code
ADD :: Code -> Code
这个类型名为 Code，反映出它的值表示用于虚拟机的代码，而虚拟机会使用栈来求值表达式。例如，代码 PUSH 1 (PUSH 2 (ADD HALT)) 对应表达式 1 + 2。类型 Code 的值表示类型 Cont 的续延这一事实，可以通过定义一个从前者映射到后者的函数来形式化：
exec :: Code -> Cont
exec HALT = haltC
exec (PUSH n c) = pushC n (exec c)
exec (ADD c) = addC (exec c)
接着，通过展开类型 Cont 及其三个组合子的定义，可以简化 exec 的定义。
HALT 情况：
exec HALT s
= { applying exec }
haltC s
= { applying haltC }
id s
= { applying id }
s
PUSH 情况：
exec (PUSH n c) s
= { applying exec }
pushC n (exec c) s
= { applying pushC }
(exec c . push n) s
= { applying . }
exec c (push n s)
= { applying push }
exec c (n : s)
ADD 情况：
exec (ADD c) s
= { applying exec }
addC (exec c) s
= { applying addC }
(exec c . add) s
= { applying . }
exec c (add s)
= { assume s of the form m : n : s' }
exec c (add (m : n : s'))
= { applying add }
exec c (n+m : s')
总之，我们推导出下面的定义：
exec :: Code -> Stack -> Stack
exec HALT s = s
exec (PUSH n c) s = exec c (n : s)
exec (ADD c) (m:n:s) = exec c (n+m : s)
也就是说，exec 是一个使用初始栈执行代码并得到最终栈的函数。换言之，exec 是执行代码的虚拟机。
最后，去函数化本身现在只需把求值函数 eval' 和 eval'' 中组合子 haltC、pushC 和 addC 的出现，分别替换为类型 Code 中对应的 HALT、PUSH 和 ADD。这样得到下面两个新定义：
comp :: Expr -> Code
comp e = comp' e HALT
comp' :: Expr -> Code -> Code
comp' (Val n) c = PUSH n c
comp' (Add x y) c = comp' x (comp' y (ADD c))
也就是说，我们现在推导出了函数 comp，它把表达式编译为代码；而它本身根据辅助函数 comp' 定义，后者额外接收一段代码作为参数。这与上一章开发出的编译器本质上相同，只是现在所需的全部编译机制，包括编译器、目标语言和虚拟机，都已经使用等式推理从源语言语义中系统化地推导出来。唯一不同的是，现在代码不是用列表表示，而是用一个专门的递归代码类型表示。例如，[PUSH 1, PUSH 2, ADD] 现在写作 PUSH 1 (PUSH 2 (ADD HALT))。
编译函数 comp 和 comp' 的正确性由下面两个方程捕获。它们是去函数化的结果，也可以通过对表达式参数进行简单归纳证明：
exec (comp e) s = eval' e s
exec (comp' e c) s = eval'' e (exec c) s
使用函数 eval' 和 eval'' 的原始规约展开这些方程右侧，就得到上一章使用过的相同编译器正确性方程：
exec (comp e) s = eval e : s
exec (comp' e c) s = exec c (eval e : s)
17.6 合并步骤（Combining the steps）
现在我们已经展示了如何通过一个系统化的三步过程，把算术表达式的求值函数转换为编译器：
- 推导一个使用栈的推广求值函数；
- 推导一个进一步推广、使用续延的版本；
- 去函数化，产生编译器和虚拟机。
不过，这个过程似乎还有简化机会。特别是，步骤 1 和步骤 2 都推导了原始求值函数的推广版本。能否合并这些步骤，避免单独的推广步骤？接着，步骤 2 引入续延，而步骤 3 立刻又移除了续延。能否合并这些步骤，避免对续延的需求？事实上，所有变换步骤都可以合并在一起。本节说明如何做到这一点，并解释由此带来的好处。
为了简化上面的逐步过程，先更详细地考察这个过程中涉及的类型和函数。我们一开始定义了类型 Expr 表示源语言的语法，并定义求值函数 eval :: Expr -> Int 作为该语言的语义，以及类型 Stack 表示整数值栈。随后推导出了四个额外组件：
- 类型
Code，表示虚拟机代码； - 函数
comp :: Expr -> Code，把表达式编译为代码； - 函数
comp' :: Expr -> Code -> Code，额外接收代码参数； - 函数
exec :: Code -> Stack -> Stack，执行代码。
此外，语义、编译器和虚拟机之间的关系由下面两个正确性方程捕获：
exec (comp e) s = eval e : s
exec (comp' e c) s = exec c (eval e : s)
合并变换步骤的关键，是直接把这两个方程作为四个额外组件的规约，然后尝试推导满足该规约的定义。考虑到这些方程涉及三个已知定义（Expr、eval 和 Stack），以及四个未知定义（Code、comp、comp' 和 exec），这看起来似乎是不可能的任务。然而，借助前几节计算中获得的经验，这其实很直接。
从 comp' 的正确性方程开始，并对表达式 e 进行归纳。每种情况下，我们都希望把方程左侧 exec (comp' e c) s 重写为某个代码 c' 对应的形式 exec c' s，由此推出定义 comp' e c = c' 在该情况下满足规约。为了做到这一点，会发现需要向类型 Code 中引入新构造子，并为这些构造子给出函数 exec 的解释。在基本情况 Val n 中，计算如下：
exec (comp' (Val n) c) s
= { specification of comp' }
exec c (eval (Val n) : s)
= { applying eval }
exec c (n : s)
现在看起来卡住了，因为没有更多定义可以应用。不过，回忆我们的目标是得到某个代码 c' 对应的项 exec c' s。因此，为完成计算，需要求解下面的方程：
exec c' s = exec c (n : s)
注意，不能简单地把这个方程用作 exec 的定义，因为定义主体中的变量 n 和 c 会没有绑定。解决办法是通过类型 Code 中一个新构造子把这两个变量打包进代码参数 c' 中，该构造子接收这些变量作为参数：
PUSH :: Int -> Code -> Code
并为 exec 定义一个新方程：
exec (PUSH n c) s = exec c (n : s)
也就是说，执行代码 PUSH n c 会先把值 n 压入栈，再执行代码 c，这也解释了新构造子的名字。使用这些思想后，计算很容易完成：
exec c (n : s)
= { unapplying exec }
exec (PUSH n c) s
最后一项现在具有形式 exec c' s，其中 c' = PUSH n c，于是可知基本情况中规约通过下面定义得到满足：
comp' (Val n) c = PUSH n c
对于归纳情况 Add x y，先像上面一样应用规约和求值函数定义：
exec (comp' (Add x y) c) s
= { specification of comp' }
exec c (eval (Add x y) : s)
= { applying eval }
exec c (eval x + eval y : s)
再次看起来卡住了，因为没有更多定义可以应用。然而，由于我们正在进行归纳计算，可以使用两个参数表达式 x 和 y 的归纳假设：
exec (comp' x c') s' = exec c' (eval x : s')
exec (comp' y c') s' = exec c' (eval y : s')
为了使用这些假设，显然必须通过把正在操作的项变换为某个代码 c' 对应的形式 exec c' (eval y : eval x : s)，把 eval x 和 eval y 的值压入栈。也就是说，需要求解下面方程：
exec c' (eval y : eval x : s) = exec c (eval x + eval y : s)
首先从具体值 eval x 和 eval y 推广，得到：
exec c' (m : n : s) = exec c (n+m : s)
不过，这一次同样不能把这个方程直接用作 exec 的定义，因为变量 c 没有绑定。解决办法是通过类型 Code 中的新构造子把这个变量打包进代码参数 c'：
ADD :: Code -> Code
并为 exec 定义一个新方程：
exec (ADD c) (m : n : s) = exec c (n+m : s)
也就是说，执行代码 ADD c 会先把栈顶两个值相加，再执行代码 c，这也解释了新构造子的名字。使用这些思想后，计算很容易完成：
exec c (eval x + eval y : s)
= { unapplying exec }
exec (ADD c) (eval y : eval x : s)
= { induction hypothesis for y }
exec (comp' y (ADD c)) (eval x : s)
= { induction hypothesis for x }
exec (comp' x (comp' y (ADD c))) s
最后一项现在具有形式 exec c' s，于是可知归纳情况中规约通过下面定义得到满足：
comp' (Add x y) c = comp' x (comp' y (ADD c))
注意，与前面推导基于栈的求值器时一样，我们选择把栈变换为 eval y : eval x : s。也可以同样选择相反顺序 eval x : eval y : s，那会为 Add 得到从右到左的求值。我们在计算中拥有这种自由，是因为由 eval 定义的语义并没有指定求值顺序。
最后，考虑方程 exec (comp e) s = eval e : s 所规约的函数 comp :: Expr -> Code，从而完成编译器开发。与上面类似，我们希望把方程左侧 exec (comp e) s 重写为某个代码 c 对应的形式 exec c s，由此推出定义 comp e = c 满足规约。这种情况下不需要使用归纳，简单计算就足够；在计算中，我们引入新构造子 HALT :: Code，以把被操作的项转换为所需形式：
exec (comp e) s
= { specification of comp }
eval e : s
= { define: exec HALT s = s }
exec HALT (eval e : s)
= { specification of comp' }
exec (comp' e HALT) s
总之，我们推导出下面这些定义：
data Code = HALT | PUSH Int Code | ADD Code
comp :: Expr -> Code
comp e = comp' e HALT
comp' :: Expr -> Code -> Code
comp' (Val n) c = PUSH n c
comp' (Add x y) c = comp' x (comp' y (ADD c))
exec :: Code -> Stack -> Stack
exec HALT s = s
exec (PUSH n c) s = exec c (n : s)
exec (ADD c) (m:n:s) = exec c (n+m : s)
这些定义与上一节得到的定义完全相同，只不过现在它们是直接从编译器正确性规约中推导出来的，而不是通过一系列独立变换步骤间接得到。此外，合并方法还有一个优点：它只使用简单的等式推理技术。特别是，不再需要使用续延和去函数化！
17.7 章注（Chapter remarks）
关于推导编译器的更多细节可见文献 [39]，本章即基于该文。该文展示了如何用同样方法为广泛的编程语言特性及其组合推导编译器，包括算术表达式、异常、状态以及各种形式的 lambda 演算。类似方法也可用于推导抽象机 [40]，例如第 8 章中的例子。
17.8 练习（Exercises）
- 假设把算术表达式语言扩展为带有简单的抛出和捕获异常原语，如下所示：
data Expr = Val Int
| Add Expr Expr
| Throw
| Catch Expr Expr
非正式地说，Catch x h 的行为与表达式 x 相同，除非对 x 求值会抛出异常；在这种情况下，catch 会表现为处理器表达式 h。如果尝试求值 Throw，就会抛出异常。为了给这个扩展语言定义语义，先回忆 Maybe 类型：
data Maybe a = Nothing | Just a
也就是说，类型 Maybe a 的值要么是 Nothing，这里把它看作异常值；要么形如 Just x，这里把它看作正常值。使用这个类型，可以把原始表达式求值函数重写为考虑异常的版本：
eval :: Expr -> Maybe Int
eval (Val n) = Just n
eval (Add x y) =
case eval x of
Just n -> case eval y of
Just m -> Just (n + m)
Nothing -> Nothing
Nothing -> Nothing
eval Throw = Nothing
eval (Catch x h) =
case eval x of
Just n -> Just n
Nothing -> eval h
使用本章描述的方法，为这个语言推导一个编译器。提示：这是一个有挑战性的练习！
练习 1 的解答见附录 A。