编程语言中的控制结构

翻译说明

大段的无代码和数学的纯文字我会使用机器翻译, 并且一般不调整术语. 一般而言, 这也不会造成任何误解.

作者序言

本书是一段穿越编程语言设计空间与历史的旅程, 视角聚焦于控制结构——即使程序得以掌控其执行流程的语言机制. 全书从早期编程语言中goto跳转指令讲起, 追溯20世纪60年代结构化编程的兴起, 进而探讨命令式语言中的高级控制结构, 如generator与coroutine, 随后转向函数式语言中对控制的另一番诠释——先是continuation及其控制算子, 再到代数效应 (algebraic effects) 与效应处理器 (effect handlers). 本书融历史叙述, 代码示例与理论分析于一体, 为读者提供了一个审视编程语言的独特比较视角, 同时也对代数效应及其他当代编程语言研究前沿课题作了深入介绍.

引论

控制可编程设备

最早的可编程装置——街头风琴 (street organs) 与Jacquard织布机——于18世纪出现在欧洲. 两者均由穿孔卡片控制. 卡片上孔洞的有无决定了演奏哪些音符, 以及选取哪些经线. 卡片被划分为若干行, 按顺序逐一执行. 如图[0.1]所示, 这些卡片往往首尾相连构成一个循环——最后一张卡片的末端与第一张卡片的开头相接——从而使乐曲或织物图案得以无限重复.

我倾向于认为, 计算机编程中顺序与循环的概念, 正是直接源于风琴与织布机对穿孔卡片的这种处理方式. 无论如何, 自20世纪40年代中期现代计算机——即程序存储于内存中的可编程电子计算器——问世以来, 这两个概念便始终在其中扮演着举足轻重的角色. 时至今日, 机器码程序仍由存储在内存中的处理器指令构成, 这些指令依次顺序执行, 唯有分支指令 (branch) 或跳转指令 (jump) 例外——它们会使执行流程跳转至指定的代码地址处继续运行. (示例见图[0.2].)

编程语言中的控制

最早的编程语言 (汇编语言, autocoder, Fortran I, ...) 呈现出一种机器风格的控制视角: 基本指令顺序执行; 无条件跳转与条件跳转——如大名鼎鼎的goto命令——则使计算得以重复或跳过. 到20世纪50年代末, 这一方式的局限性已日渐显露, 促使后续编程语言 (如Algol 60及其众多后继者) 引入了更高层次的控制结构:

• 首先是子程序, 过程与函数, 用以将代码分解为中等规模的单元, 使其得以独立开发与理解;
• 其次是结构化控制构造, 如条件语句 (if-then-else), 计数循环 (for) 与通用循环 (while), 这些构造可自由嵌套, 并由此产生了优雅的语言文法;
• 此后又出现了其他形式的非局部控制, 如coroutine, 协作式或并发线程, 异常, 对象与actor, 它们着重体现了各自独立编写的代码组件之间的控制交错.

从控制视角研究编程语言

本书是一段以控制的概念与范式为引导, 穿越编程语言设计空间与历史时间的旅程. 我们将尝试回答以下问题:

• 语言为程序员提供了哪些构造, 用以表达和约束计算的顺序? 这些构造的表达能力如何? 它们在不同语言之间如何比较?
• 这些语言构造催生或鼓励了怎样的源程序结构, 组织方式与编程风格? 结构化编程究竟是关于消除goto语句, 还是关于使源代码成为程序的首要描述方式, 而非流程图? 声明式编程究竟是关于将控制决策交由编译器处理, 还是关于使程序更接近数学规范?
• 编程语言理论对控制能作出怎样的阐释? 程序逻辑与控制结构之间存在怎样的关联? 控制如何融入更一般的效应 (effects) 框架之中, 例如类型与效应系统 (type and effect systems), monad, 以及代数效应理论?

本书大纲

本书剩余部分分为四篇.

第一篇: 命令式语言的控制结构描述, 比较并呈现了传统命令式语言与面向对象语言中控制结构的历史演变.

• 第1章从非结构化跳转讲起, 继而介绍结构化条件语句与循环, 以及可能涉及的提前退出机制.
• 第2章回顾20世纪60年代末的结构化编程运动, 并探讨goto消除问题, 即仅使用结构化控制进行编程的问题.
• 第3章描述子程序, 过程与函数——它们为代码的结构化与复用提供了语言层面的支持. 本章还讨论它们与非局部跳转及异常之间的交互.
• 第4章研究用于反转或对称化独立程序片段之间控制关系的机制, 如iterator, generator, coroutine与协作式多线程.

第二篇: 函数式语言的控制算子专注于函数式编程语言及其将控制流作为称作continuation的数据加以操纵的能力——这使得将自定义控制结构定义为库成为可能.

• 第5章分多步介绍纯函数式编程 (从电子表格入手), 并讨论求值策略与操作语义.
• 第6章介绍continuation最初引入时的面貌: 作为一种语义工具, 用于表达指称语义与操作语义.
• 第7章说明continuation在函数式编程中同样大有用处——以continuation传递风格 (continuation-passing style, CPS) 编写的程序, 能够定义异常, iterator, coroutine与线程等高级控制结构.
• 第8章描述控制算子, 如Scheme中的call-with-current-continuation, 使所有函数式程序 (即便并非以CPS风格编写) 都能够捕获并操纵continuation.

第三篇: 从异常与monad到代数效应与处理器描述函数式语言控制算子领域的一项近期进展——effect handler及其背后的理论基础代数效应 (algebraic effects).

• 第9章以函数式语言中异常与异常处理的形式化为起点, 开启通往代数效应与handler的旅程, 并讨论未捕获异常问题的解决方案.
• 第10章描述用于用户自定义效应的effect handler——一种融合了异常与定界continuation (delimited continuations) 双重特性的控制算子——以及其在OCaml语言中的集成方式.
• 第11章讨论monad——它为效应的传播与顺序化提供了一种通用描述, 也是将效应引入Haskell等纯函数式语言的流行方式.
• 第12章描述代数效应及其handler的理论, 该理论在monad理论的基础上, 对效应的产生与处理给出了通用描述, 并构成第10章所述effect handler的理论基础.

第四篇: 控制与效应的推理展示如何借助类型系统与程序逻辑, 建立关于控制与效应的安全性与正确性性质.

• 第13章描述带效应语言的类型系统: 简单类型系统确保高级控制结构存在时的数据安全性, 而更丰富的类型与效应系统则进一步确保控制安全性, 以及未捕获异常与未处理效应的缺失.
• 第14章回顾Hoare逻辑——第一个用于演绎验证的程序逻辑——并展示如何将其扩展至第一篇所讨论的各类控制结构.
• 第15章探讨为函数式与命令式语言中的控制算子定义程序逻辑的困难, 并介绍若干基于分离逻辑 (separation logic) 的近期方案——分离逻辑是Hoare逻辑的一种扩展, 便于对资源进行推理.

阅读指南

本书假定读者熟悉至少一门命令式编程语言 (如C, C++, Java或Python) 和至少一门函数式编程语言 (如Haskell, OCaml, Scheme或SML). 配套网站XXX收录了书中所有代码示例并提供运行说明. 技术性较强的章节还需要读者具备一定的编程语言理论基础, 例如可参阅电子教材Programming Languages Foundations (Pierce et al., 2025).

本书有多种阅读方式. 主要对编程语言比较及其历史演变感兴趣的读者, 可重点阅读第1至5章及第8至10章. 对函数式编程及continuation应用感兴趣的读者, 可跳过第一篇, 重点阅读第5至10章. 已熟悉部分内容但希望深入了解代数效应近期进展的读者, 可从第三篇入手, 重点阅读第9至15章. 最后, 对编程语言基础及其在程序验证中的应用感兴趣的读者, 将会在第6, 8章以及第11至15章中大有收获.

全书技术难度并非线性递增, 而是在每篇之内递增, 通常也在每章之内递增. 遇到过于技术性的段落时, 建议读者跳至下一章乃至下一篇继续阅读.

第1章 早期编程语言

第1.1节 处理器之中的控制流

当今绝大多数计算设备都是带存储程序的可编程计算机, 即描述计算过程的程序与其所操作的数据一同存储在内存中. 这种计算机体系结构被称为冯·诺依曼架构 (von Neumann architecture), 因为它最早由von Neumann (1945) 在一份技术报告中加以描述. Turing (1946)也描述了一种类似的架构.

程序计数器与分支. 在冯·诺依曼架构中, 中央处理器 (CPU) 有一个专用寄存器——程序计数器 (PC), 它存储着下一条待执行指令所在内存字的地址. 大多数指令 (算术与逻辑运算, 内存读写等) 在执行时会将PC递增, 使其指向内存中的下一条指令, 从而保证存储在内存中的指令得以顺序执行. 与之相对, 分支指令则显式地设置PC的值, 使程序得以跳转至任意位置继续执行.

第1.2节 机器语言, 汇编语言

第1.3节 FORTRAN

第1.4节 ALGOL 60

第1.5节 条件式和循环

第1.6节 从循环和块之中及早退出

第1.7节 深入阅读

第2章 结构化编程

第2.1节 一场运动和一场争议

如今结构化编程指的是使用高层次控制结构 (条件式, 循环, ...) 而非低层次的goto跳转这一毫无争议的编程实践. 然而, 在1965-1975期间, 结构化编程则是充满争论的主题, 其既可以视为一场迈向看待软件的新角度的运动, 也可以视为关于如何编写良好程序的一场争议.

结构化编程运动提倡将程序视为一种构造而成, 具有结构的源代码文本, 以高级语言书写. 这段源代码应当能够自我解释, 无需借助流程图或其他外部文档, 并且应当支持对程序的推理——初步阶段是非形式化的, 之后则是数学意义上的 (借助程序逻辑).

这一运动的纲领性著作是Dahl等人所著的Structured programming (1972). 该书收录的三篇论文引入了高层编程概念, 对现代软件工程产生了深远影响: formal methods, program refinement, data structures, type algebras, objects and classes, 以及coroutines. 从这本书的视角来看, 程序应当使用还是摒弃goto, 不过是一个无关紧要的细节.

结构化控制之争所聚焦的问题, 远比结构化编程运动本身狭窄得多. 这是两种编程风格之间的争论: 一方是通过对流程图的机械转录而产生的, 充斥大量goto语句的程序; 另一方则是几乎完全或完全只使用控制结构 (条件语句, 循环语句等) 直接编写, 无需借助流程图的程序. 这场争论因Dijkstra (1968) 一篇著名论文的标题而广为人知——Go to statement considered harmful.

早期的迹象. Knuth(1974)列举了计算机文献中结构化编程的早期踪迹. 例如, 1966年, Dewey Val Schorre提到了使用对缩进敏感的文本大纲来代替流程图为汇编代码作文档:

自1960年夏天起, 我便开始以大纲形式编写程序, 以缩进约定来表示控制流. 我从未发现有必要打破这些约定而使用go语句. 我习惯将这些大纲作为程序的原始文档, 而不是使用流程图 ... 然后我再根据大纲将程序用汇编语言编码. 所有人都觉得这些大纲比流程图更好用.

如果你仔细观察, 就会发现一个看似向回跳转的go to语句, 往往其实是一个隐蔽的for语句. 而当你把for子句放回它本该出现的位置时, 你会欣喜地发现算法的清晰度大为提升. 在我看来, 如果(编程课程的)目的是教授Algol编程, 那么使用流程图弊大于利.

引爆争论. 正是Dijkstra的短篇通讯Go to statement considered harmful (Dijkstra, 1968) 引爆了结构化控制之争. 他以信件形式将其寄给Communications of the ACM的编辑, 未附标题; 编辑们加上了这个如今家喻户晓的题目. 一如Dijkstra的一贯风格, 文章开篇便语出惊人:

多年来我一直注意到这样一个现象: 程序员的水平与其所写程序中go to语句的密度成反比. 最近我发现了go to语句之所以产生如此灾难性后果的原因, 并由此确信, go to语句应当从所有高级编程语言中彻底废除 (也许纯机器码除外). 彼时我并未对这一发现给予太多重视; 现在我将我的思考提交发表, 是因为在近来涉及这一议题的讨论中, 我被多方敦促这样做.

对于由一系列基本操作构成的程序, 当前程序点已足以描述执行路径. 对于if-then-else条件语句, 我们还需要知道之前各条件判断的布尔值. 如果程序点处于一个或多个结构化循环之内, 我们还需要知道这些循环已执行了多少次. 请看以下示例:

        while (x < y) {         ⇐ 2nd iteration
          while (a[x] != 0) {   ⇐ 5th iteration
            if (x == 0) {       ⇐ was true
              ...
            }
            if (y == 0) {
              ...               ⇐ you are here
            }
          }
        }

然而, 如果程序使用了任意的go to语句, 正如Dijkstra所写, 要找到一组有意义的坐标来描述进程的推进, 将变得极为困难. 请看以下示例:

        if (x == 0) {
          L: ...;
        }
        if (y == 0) {
          ...
          goto L;
        }

第2.2节 没有goto的编程

在1970年代初, 不使用goto语句的编程方式是许多研究的主题: 首先, 是评估纯粹的结构化编程是否真的比有节制地使用goto更能表达程序结构; 其次, 是设计方法以消除现有程序中的goto语句, 既可逐案处理, 也可通过程序变换系统性地完成.

Knuth的综述Structured Programming with go to Statements (Knuth, 1974) 通过精心挑选的示例探讨了消除goto所带来的影响, 并指出这样做有时会降低代码的清晰度或影响性能, 尤其是当它导致代码片段重复或需要引入额外的布尔标志时.

以下是一个改编自Knuth的示例: 使用线性探测法向哈希表中插入元素. 该表由两个数组表示: A[N]存储键, B[N]存储与之对应的值.

       void add(key k, data d)
       {
           int i = hash(k);
           while (1) {
               if (A[i] == 0) goto notfound;
               if (A[i] == k) goto found;
               i = i + 1; if (i >= N) i = 0;
           }
         notfound: A[i] = k;
            found: B[i] = d;
       }

我们可以用不含提前退出和goto的结构化while循环来改写它, 如下所示:

       void add(key k, data d)
       {
           int i = hash(k);
           while (! (A[i] == 0 || A[i] == k)) {
               i = i + 1; if (i >= N) i = 0;
           }
           if (A[i] == 0) A[i] = k;
           B[i] = d;
       }

第3章 非局部控制

第4章 控制反转

第5章 函数式语言

第5.1节 声明式编程: 抛弃控制?

到目前为止, 我们理所当然地认为源代码必须显式描述程序之中的计算顺序 (sequencing), 并且编程语言必须提供表达这种顺序的控制结构. 然而, 这种假设受到了声明式语言的质疑, 其在源代码之中大体将计算顺序留作隐式, 而依赖于编译器确定计算的正确顺序. 换言之, 声明式语言强调什么 (什么是要被计算的?) 而非如何 (如何将计算分解为基本步骤? 以什么顺序施行这些步骤?).

声明性方法的一个例子是诸如SQL这样的数据库查询语言: 查询描述了要从数据库里拉取什么记录; 如何搜索数据库则留给数据库管理系统确定. 其他的声明性编程范式包括逻辑编程 (Prolog, Datalog), 纯函数式编程 (Haskell, Agda), 以及数据流编程 (Simulink, Lustre). 诸如Verilog和VHDL这样的硬件描述语言本质上也是声明性的.

声明式编程于1970年代引入, 其目的在于简化编程和将编程从von Neumann风格之中解放出来, 如Backus (1978) 所言. 1980年代的焦点转移到了并行计算之上: 人们希望声明式语言比起标准的命令式语言并行执行起来更加容易, 这恰恰是因为前者给予了编译器在调度计算方面更大的灵活性. 自1990年代起, 声明式编程因其安全性和与形式验证的亲缘关系而受到认可.

声明式编程能否摆脱控制结构? 其能否将程序员从表达程序之中的控制的重担中解放出来呢? 本章试图在纯函数式编程的上下文之中回答这些问题, 通过检视三种表达力依次递增的小语言: XL, 一个电子表格语言; APP, 带有与值不同的函数的一个应用性语言; FUN, 将函数作为值的一个函数式语言.

第5.2节 XL: 表达式和电子表格

带有共享的表达式. 考虑以下算术表达式和等式的语言, 昵称XL:$$\begin{array}{rrcll}\text{表达式:}& e& ⩴& 0\left|1.2\right|3.1415|\dots & \text{常量}\\ & & |& x\left|y\right|z|\dots & \text{变量}\\ & & |& \mathrm{op}(e_1,\dots ,e_n)& \text{运算}\\ \text{程序:}& p& ⩴& \{x_1=e_1;\dots ;x_n=e_n\}& \text{等式的集合}\end{array}$$诸如$x+1$和$y\times z$这样的算术表达式是由常量和变量通过使用诸如$+,-,\times ,/$等运算构筑而成的. 程序是变量和表达式之间的等式的集合.

通过等式被绑定至表达式的变量使用捕获了计算共享的概念. 例如, 以下两个程序$$\begin{array}{rcl}{p}_1& =& \{x=2\times 3;y=x+x\}\\ p_2& =& \{x=2\times 3;y=2\times 3+2\times 3\}\end{array}$$能够计算出相同的结果 (其含义之后将会精确化), 但是$p_1$只会对于$2\times 3$进行一次求值, 之后在对于$x+x$的求值过程中共享结果$6$, 而$p_2$会对于$2\times 3$求值三次.

电子表格.

无环条件. 我们希望XL程序容易求值. 这意味着避免难以求解的等式, 例如$x=x^3-2x^2+2$. 我们还要走的远得多, 排除所有这样的等式$x=e$, 其中$e$依赖于$x$, 不论直接依赖还是通过其他等式间接依赖, 如以下例子所示:$$\begin{array}{c}\{x=x+1\}\\ \{x=y+1;y=x-1\}\end{array}$$换言之, 这些等式不能包含依赖循环. 这种无环条件成立当且仅当程序不只是能写作等式的集合, 而且可以写作等式的有序列表$$x_1=e_1;\dots ;x_n=e_n$$其中可以出现在$e_i$之中的变量只能是满足$j<i$的变量$x_j$.

电路和数据流图. 图5.2和图5.3展示了图5.1中电子表格的两种替代表示形式. 第一种是电路, 其中变量 (单元格) 由导线表示, 运算符由门表示. 无环条件对应于电路中不存在回路, 换言之, 这必须是一个组合电路.

另一种替代表示形式是数据流图: 一种以常量和运算符为节点, 以边表示数据流向 (从某节点流向需要其值的运算符) 的有向无环图 (DAG). 无环条件对应于图中不存在环.

程序求值. 对XL程序$\{x_1=e_1;\dots ;x_n=e_n\}$进行求值, 就是确定每个变量$x_i$的数值$v_i$. 这些值即为对应电子表格单元格中所显示的内容.

不拘泥于具体的求值算法, 我们可以将所有可能的求值过程描述为对程序的一系列归约. 每次归约将程序改写为另一个更简单的程序. 当程序被改写为一组平凡方程$\{x_1=v_1;\dots ;x_n=v_n\}$时, 求值过程即告完成, 此时变量$x_i$的值$v_i$已一目了然. 以下是可使用的两条归约规则:$$\begin{array}{rcllr}x& \to & e& \text{, 如果}x=e\text{是一个等式}& \text{(unfold)}\\ \mathrm{op}(v_1,\dots ,v_n)& \to & v& \text{, 如果}v={\mathrm{op}}^{⁎}(v_1,\dots ,v_n)& \text{(prim)}\end{array}$${译注: 根据个人习惯, 严格来说, 这些不仅是所谓的归约规则, 而且是可以在上下文中使用的归约规则. 根据所谓的reduction semantics, 这要使用兼容闭包来定义.}

第5.3节 APP: 表达式和用户定义的函数

第5.4节 FUN: 函数作为第一级值

第5.5节 上下文下的归约

我们如何以数学上的精确性来形式化并定义一种求值策略? 本书始终遵循的方法是: 通过在受限上下文下的规约来定义求值.

上下文. 一个上下文是一个带一个洞的表达式. 洞记作$[]$. 例如, $(1+[])\times 3$是一个上下文.

第5.6节 深入阅读

第6章 延续和CPS变换

第6.1节 延续的概念

程序点的延续. 考虑程序执行过程中的一个点. 这个程序中该程序点的延续是在执行抵达该点之后还要执行的计算序列, 其是为了完成整个程序的执行过程.

在很多情况下, continuation可以用编程语言本身来表示, 形式为一条命令或一个函数 (见下方示例). continuation也可以是一个语义对象, 如第6.3节所示.

基于语句的语言中的continuation示例. 考虑以下四个程序, 其以带有结构化控制的Algol风格命令式语言写成:$$\begin{array}{rcl}{p}_1& =& {s_1}^{\text{(a)}};s_2\end{array}$$

第6.2节 指称语义回顾

指称语义由Christopher Strachey, Dana Scott, Christopher Wadsworth于1960年代后期引入, 其是以数学的精确定义程序的含义之方法. 指称语义以复合性的方式将数学对象与编程语言的每个句法元素 (表达式, 语句, 函数, ...) 联系起来.

例如, 一个牵涉变量的整数算术表达式$e$的含义可以被定义为从存储到整数的映射, 其中存储将整数与变量联系起来:

第6.3节 基于延续的指称语义

第6.4节 标签和跳转的指称语义

第6.5节 CPS变换

第6.6节 CPS变换的语义性质

第6.7节 深入阅读

第7章 延续编程

continuation-passing style (CPS) 在第6章中作为一种语义工具被引入, 彼时CPS变换的作用是使函数式语言中的归约策略变得显式. 本章将说明, CPS及其变体同样是函数式语言中一种实用的编程技术, 它使函数能够访问其调用处的continuation. 由此, 许多高级控制结构 (generator, coroutine, 回溯等) 都可以在任意函数式语言中作为库函数来实现.

第7.1节 以CPS风格编写函数

CPS的核心特征是: 函数不以常规方式返回结果, 而是始终将结果传递给作为额外参数传入的continuation. 例如, 以下是用OCaml以标准直接风格 (direct style) 编写的朴素阶乘函数:

    let rec fact n =
      if n = 0 then 1 else n * fact (n-1)

    let rec cps_fact n k =
      if n = 0 then k 1 else cps_fact (n-1) (fun r -> k (n * r))

上面的cps_fact可以机械地生成——对fact的定义应用第6.5节中某个call-by-value CPS变换即可. 然而, CPS变换设计上是作用于整个程序的, 而CPS编程往往选择性地引入continuation: 并非对所有函数, 而只对那些能从CPS中受益的函数. 例如, 并非要将cps_fact的所有调用方都改写成CPS——部分调用方可以保持直接风格, 以cps_fact n (fun r -> r)来等价地调用fact n.

为何要以CPS风格编写函数? 原因之一是, CPS风格的递归函数在常量栈空间内运行: 所有递归调用都是尾调用. 但这并不意味着它们在常量空间内运行——直接风格中本会分配在栈上的活动记录, 在CPS中以函数闭包的形式分配在堆上. 用堆空间代替栈空间在某些情况下仍有优势, 尤其是当语言实现人为限制了栈的大小时.

但CPS编程的主要动机与上述实现层面的考量无关, 而是赋予CPS函数以多种方式操纵其continuation的能力——而不仅仅是用最终结果调用它.

第7.2节 迭代器

考虑以节点存储值的二叉树:

    type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree

    let rec tree_iter (f: 'a -> unit) (t: 'a tree) =
      match t with
      | Leaf -> ()
      | Node(l, x, r) -> tree_iter f l; f x; tree_iter f r

第8章 控制运算子

控制运算子是由某些函数式语言所提供的语言构造, 其允许表达式捕获延续, 将延续作为第一级值操纵, 以及之后重启延续.

控制运算子使得将高级控制结构 (异常, 回溯, 协作线程, 等等) 编写为库函数成为可能, 其可以在以直接风格写成的程序之中运用. 藉由控制运算子, 我们无需像我们在第7章所做的那样, 通过将程序改写为延续传递风格以使用用户所定义的高级控制结构.

第8.1节 Landin的J运算子

最早发表的控制算子出现在Landin (1965) 关于Algol 60语义的工作中, 该工作基于将Algol 60翻译到他的ISWIM语言.

ISWIM是所有现代严格求值函数式语言 (Scheme, Common Lisp, SML, OCaml等) 的前身. 它以按值调用 (call-by-value) 的lambda演算为基础, 并扩展了基本数据类型和操作. 与lambda演算一样, 与早期的Lisp系统不同, ISWIM保证函数抽象中自由变量的静态作用域. ISWIM的语义以操作风格定义, 使用名为SECD的抽象机 (Landin, 1966). SECD是第一个使用函数闭包 (function closure) 来表示具有静态作用域的一等函数的函数式语言实现.

Landin (1965) 概述了通过将Algol 60翻译到带若干扩展的ISWIM来解释Algol 60的方案. 为了处理多个函数环境共享的可变变量, Landin添加了ML风格的引用 (reference). 为了处理非局部goto跳转, 他添加了一个名为J的控制算子 (J代表jump, 即跳转).

J算子可以被看作C或Java等语言中return语句的推广.

第8.2节 call-with-current-continuation (callcc)

最为知名的控制运算子或许是来自于Scheme语言的call-with-current-continuation, 其经常被缩略为call/cc或者callcc. 其允许一个表达式将其自身的延续以函数的形式捕获. 这个运算子在文献里以各种不同的名字出现:

第8.3节 使用callcc实现控制结构

第8.4节 callcc的语义

第8.5节 定界延续

第8.6节 定界延续运算子的语义

第8.7节 使用定界延续实现控制结构

第8.8节 定界延续的CPS变换

第8.9节 深入阅读

第9章 异常

第10章 用户定义作用的作用处理器

第11章 单子

monad是函数式语言中的一种流行编程模式: 它允许程序员表达语言原生不支持的effect, 例如Haskell中的可变状态以及OCaml中的无界continuation. monad同时也是一种强大的语义工具: 它为编程语言中effect的传播与序列化提供了一种通用的描述方式. 本章对monad的介绍着重于其语义层面, 因为这正是第12章所呈现的algebraic effect理论的出发点.

第11.1节 语义和程序变换的共性

指称语义通过将数学对象$⟦s⟧$与句法对象 (如命令式语言的语句$s$) 相关联来进行处理. 如第6.2节和 6.3 节所示, 指称的domain取决于我们需要描述的编程语言的特性. 例如, 对于简单的命令式语言IMP, 我们考虑了四种不同的domain:$$\begin{array}{rclr}⟦s⟧& :& \mathrm{Store}\to \mathrm{Store}& \text{(1)}\\ ⟦s⟧& :& \mathrm{Store}\to \mathrm{Store}+\{\perp \}& \text{(2)}\\ ⟦s⟧& :& \mathrm{Store}\to (\mathrm{Store}\to \mathrm{Store}+\{\perp \})\to \mathrm{Store}+\{\perp \}& \text{(3)}\\ ⟦s⟧& :& \mathrm{Env}\to \mathrm{Store}\to (\mathrm{Store}\to \mathrm{Store}+\{\perp \})\to \mathrm{Store}+\{\perp \}& \text{(4)}\end{array}$$在(1)中, 我们从一个简单的思想出发, 即语句$s$是一个store transformer, 其中store将变量映射到值. 在(2)中, 我们加入了bottom ($\perp$) 结果, 以处理不终止的循环. 在(3)中, 我们切换到continuation-passing style (CPS), 从而使语句$s$的continuation显式化. 最后, 在(4)中, 我们将一个environment作为参数加入, 例如用于将continuation与代码标签相关联.

随着指称domain的改变, 基本语句的指称也会改变, 尽管它们的直觉语义仍然保持不变. 例如, 以下是$\mathrm{skip}$ (do nothing) 和$x≔e$ (assignment) 在上述四个domain里的指称:$$\begin{array}{rclrclr}⟦\mathrm{skip}⟧\sigma & =& \sigma & ⟦x≔e⟧\sigma & =& \sigma [x≔(⟦e⟧\sigma )]& \text{(1)},\text{(2)}\\ ⟦\mathrm{skip}⟧\sigma k& =& k\sigma & ⟦x≔e⟧\sigma k& =& k(\sigma [x≔(⟦e⟧\sigma )])& \text{(3)}\\ ⟦\mathrm{skip}⟧\rho \sigma k& =& k\sigma & ⟦x≔e⟧\rho \sigma k& =& k(\sigma [x≔(⟦e⟧\sigma )])& \text{(4)}\end{array}$${译注: 我给上述公式的某些地方添加了括号, 使之更容易阅读和理解.} 在所有这些情形之下, $⟦\mathrm{skip}⟧$都会保持初始store $\sigma$不变而返回, 而$⟦x≔e⟧$则会在更新$x$的值后返回$\sigma$, 但是返回这些store的方式有所不同.

在诸如顺序$s_1;s_2$这样的控制结构的情形下, 这种现象甚至更为引人注目.$$\begin{array}{rclr}⟦s_1;s_2⟧\sigma & =& ⟦s_2⟧(⟦s_1⟧\sigma )& \text{(1)}\\ ⟦s_1;s_2⟧\sigma & =& \{\begin{array}{cc}\perp & \text{, 如果}⟦s_1⟧\sigma =\perp \hfill \\ ⟦s_2⟧(⟦s_1⟧\sigma )& \text{, 否则的话}\hfill \end{array}& \text{(2)}\\ ⟦s_1;s_2⟧\sigma k& =& ⟦s_1⟧\sigma (\lambda {\sigma }^{\prime }.⟦s_2⟧{\sigma }^{\prime }k)& \text{(3)}\\ ⟦s_1;s_2⟧\rho \sigma k& =& ⟦s_1⟧\rho \sigma (\lambda {\sigma }^{\prime }.⟦s_2⟧\rho {\sigma }^{\prime }k)& \text{(4)}\end{array}$$在所有这些情形之下, $s_1$执行结束时的store, 如果其是终止的, 就会变成$s_2$执行时的初始store. 然而, 以数学语言表达这种直觉需要四种不同的方式.

此时, 问题在于: 我们能否以这样一种方式为赋值和顺序等基本构造给出指称语义, 使得当语义domain改变时语义等式仍能保持不变?

程序变换是为编程语言赋予语义的另一种方式, 即将其翻译为更简单更易理解的语言. 例如, 第6.5节中的CPS变换阐明了函数式语言中call by name与call by value之间的区别. 与指称语义的情况类似, 针对FUN这类函数式语言的程序变换也具有一些共性. 考虑第6.5节中的call-by-value CPS变换$\mathcal{C}$, 第8.4节中的double-barreled CPS变换${\mathcal{C}}_2$, 以及同样来自第8.4节的ERS (exception-returning style) 变换$\mathcal{E}$. 以下是关于常量, 变量和函数抽象的转换规则:$$\begin{array}{rclrclrcl}\mathcal{C}(c)& =& \lambda k.kc& \mathcal{C}(x)& =& \lambda k.kx& \mathcal{C}(\lambda x.e)& =& \lambda k.k(\lambda x.\mathcal{C}(e))\\ {\mathcal{C}}_2(c)& =& \lambda k.\lambda k^{\prime }.kc& {\mathcal{C}}_2(x)& =& \lambda k.\lambda k^{\prime }.kx& {\mathcal{C}}_2(\lambda x.e)& =& \lambda k.\lambda k^{\prime }.k(\lambda x.{\mathcal{C}}_2(e))\\ \mathcal{E}(c)& =& Vc& \mathcal{E}(x)& =& Vx& \mathcal{E}(\lambda x.e)& =& V(\lambda x.\mathcal{E}(e))\end{array}$$在所有这些情形下, 表达式的值都会立即作为结果返回,

第12章 代数作用

第11章所描述的monad理论, 提供了对效应的传播与排序的通用描述. 然而, 它并未涉及效应如何被生成和实现. 相反, 每个monad都提供其自身特定的操作及其实现.

本章所研究的代数效应 (algebraic effects) 理论, 在monad理论的基础上进一步扩展, 对效应的生成与处理提供了通用描述, 而不依赖于特定monad的具体细节. 该理论为effect handler提供了形式化基础并启发了其设计, effect handler是第10章所描述的控制运算符.

第12.1节 monadic程序的通用语义

一个monadic语言. 作为本节的贯穿示例, 考虑第11.2节的计算性lambda演算, 其配备了state monad的操作get和set, 以及nondeterminism monad的操作choose和fail.

第13章 类型和作用系统

类型系统通常被应用于编程语言, 以提高程序的可靠性和清晰性. 它们能够预防许多常见的编程错误, 并描述程序组件的接口.

类型系统提供数据完整性保证, 例如数组的所有元素具有相同的类型或函数只能应用于预期类型的参数. 它们还能提供关于控制流的保证. 例如, 某些类型系统保证程序的终止性, 而另一些则保证程序中可能抛出的所有exception都在程序内部得到处理, 从而避免第9.4节中描述的uncaught exception问题.

本章从两个角度探讨类型系统与控制结构之间的交互. 首先, 研究如何将纯语言的简单类型系统扩展为支持高级控制结构 (exception, continuation, 用户自定义effect), 同时仍能保证数据完整性. 其次, 讨论类型与effect系统如何追踪控制effect, 以确保关于控制流的安全性保证, 例如不存在uncaught exception或未处理的effect.

第13.1节 类型系统回顾

类型系统. 类型规范将程序所操作的值组织为若干类型. 这些类型包括:

• 基本类型 (base type), 例如整数的int, 布尔值的bool, 字符串的string等;
• 复合类型 (composite type), 例如bool → int (从布尔值到整数的函数) 或string list (字符串的同质列表).

对于FUN这样的表达式语言, 类型系统通常由一组typing rule定义: 即公理和推理规则, 它们定义谓词$\mathrm{\Gamma }⊢e:\tau$, 其含义为在假设$\mathrm{\Gamma }$下, 表达式$e$具有类型$\tau$. 环境$\mathrm{\Gamma }$是从变量$x_i$到其类型${\tau }_i$的部分映射 (partial mapping).

图[13.1]展示了FUN语言的定型规则. 规则(var)表明变量$x$的类型是定型环境中与$x$关联的类型. 规则(const)表明$\mathrm{true}$和$\mathrm{false}$的类型为$\mathrm{bool}$. 规则(abstr)表明, 若在假设$x$具有类型$\sigma$的前提下函数体$e$具有类型$\tau$, 则函数$\lambda x.e$具有类型$\sigma \to \tau$. 规则(app)表明, 类型为$\sigma \to \tau$的函数可以应用于类型为$\sigma$的参数, 产生类型为$\tau$的结果. 最后, 规则(cond)表明, 若条件$e_1$具有类型$\mathrm{bool}$且两个分支$e_2$和$e_3$均具有类型$\tau$, 则条件表达式$\mathrm{if}{e}_1\mathrm{then}{e}_2\mathrm{else}{e}_3$具有类型$\tau$.

类型检查. 尽管类型可以在程序执行期间动态检查, 但通过在程序执行前进行编译期静态分析来检查类型能获得更强的保证. 这种程序分析称为type checker, 它将类型与表达式和变量关联起来, 并验证typing rules是否得到遵守. 在FUN这样的简单类型系统中, 所有类型都可以从未加注解的程序中推断出来. 更丰富的类型系统则需要在程序中提供一些类型信息, 例如函数参数的类型, 即将$\lambda x.e$写成$\lambda x:\tau .e$.

类型安全.

第14章 控制结构的Hoare逻辑

第14.1节 演绎验证回顾

正如数学逻辑为证明数学定义的性质提供推理原则一样, 程序逻辑为证明程序的性质 (如功能正确性) 提供推理原则. 这种基于逻辑的程序验证方法称为演绎验证 (deductive verification).

要使用演绎验证, 程序首先必须用关于其状态的逻辑断言 (logical assertions) 来标注,例如:

• 前置条件 (preconditions): 输入的预期性质;
• 后置条件 (postconditions): 输出的保证性质;
• 附加在循环或数据结构上的不变量 (invariants): 预期在每次循环迭代时或在数据结构的整个生命周期内成立.

例如,下面是一个用ACSL规范语言标注了逻辑断言的C函数:

    /*@
      requires \valid(a + (0..n-1));
      assigns  a[0..n-1];
      ensures  \forall integer i; 0 <= i < n ==> a[i] == 0;
    */
    void set_to_zero(int* a, size_t n) {
      for (size_t i = 0; i < n; i++) {
        /*@ invariant \forall integer j; 0 <= j < i ==> a[j] == 0 */
        a[i] = 0;
      }
    }

第14.2节 Hoare逻辑: 结构化控制的程序逻辑

从Turing到Floyd再到Hoare. 演绎验证最初是在以flowchart (控制流图, CFG) 表示的非结构化程序的背景下发展起来的, flowchart上标注有逻辑断言. 这一方法最早出现在Turing (1949) 的一篇早期通信中, 但该文直到被Morris and Jones (1984) 正式发表并加以评注之后才引起广泛关注. 同一方法被Floyd (1967) 独立地重新发明并深入研究.

然而, Turing (1949) 和Floyd (1967) 都没有涉及程序逻辑的概念. 他们关注的是演绎验证中程序逻辑之后的下一步: 从标注好的程序中生成验证条件 (verification conditions).

程序逻辑作为演绎验证基础的概念出现在Hoare (1969) 的著名论文An Axiomatic Basis for Computer Programming中. Hoare考察的不是flowchart, 而是Algol风格的结构化程序. 这一点意义重大,因为程序逻辑与结构化控制深度交织在一起: 程序验证遵循程序的结构, 而程序逻辑的规则也与编程语言的控制结构几乎一一对应, 正如本章其余部分所示.

第15章 控制运算子的分离逻辑