Header

译自 Having an Effect。除非特殊说明，下文中的『我』指原文作者 Oleg Kiselyov。

简介

本研究如同一次追寻表象之下草蛇灰线的旅程：Monad，Monad Transformer，Free Monad 以及可扩展副作用（Extensible Effects）的创始论文本质上都是关于所谓『可扩展解释器』问题的研究。一路走来，我们意识到表达式问题（expression problem），稳定指称问题，以及可扩展解释器问题都是同一事物的别称。最终我们找到了组织原则：交互－－客户端与服务器之间的交互、解释器与被解释代码之间的交互、表达式与其上下文之间的交互。

可能用『进程演算（process calculus）』能更好描述交互。而在各种序贯式的演算中，最早的把计算副作用视为交互，并且做出形式化表述的工作则是 Cartwright 与 Felleisen 发表的著作《Extensible Denotation Language Specifications》。

  • 本文用现代的方法重构了 Cartwright 与 Felleisen 方法。得益于 tagless-final 形式，我们重构后的版本更简单，可以直接给计算机运行。

  • 本文也在前人的工作之上做了进一步发展。本文令副作用处理程序变得模块化且可扩展－－它变成程序的一部分，而非永久独立于程序之外。这使得下面的做法成为可能。

  • 尽管整数和一般的一阶子语言不需要变量和环境，Cartwright 与 Felleisen 的方法也必须将变量和环境融入基本语义框架；我们避免特殊对待可变环境和任意高阶编程特性，而是将 Lambda 与 State 一视同仁。动态绑定和词法绑定，以及各种调用约定（按值调用，按需求调用，按名调用）可以视为用不同方式解释副作用『解引用绑定变量』。

对研究领域溯本求源，寻回直达本质的洞见，发掘其沧海遗珠。这一探索过程有助于为我们为程序重新发明副作用。

本演讲稿于 2016 年 8 月 25 日在印第安纳大学信息与计算学院 (SoIC) 计算机科学研讨会上首次发表。我要感谢 Martin Berger 与我进行了许多令人受益匪浅的讨论，特别是解释了进程演算的起源。此外还要感谢穆信成与 Matthias Felleisen 提出的宝贵意见。

版本

当前版本为 2017 年 9 月版

引用资料

本文所使用的 Haskell 98 代码的完整版

Cartwright-Felleisen 框架现代重构 OCaml 版本。附带全局状态、动态绑定、按值调用和按需求调 用的词法绑定示例

不稳定的指称，脆弱的解释器，难以应用的理论

从『实用』角度看指称语义

鉴于副作用普遍存在又颇具争议，对其进行研究很有必要。最值得我们注意的研究莫过于 20 世纪 70 年代，『维也纳指称语义学派』在研究如何形式化 PL/I 编程语言中的工作中作出的1。该研究主要基于指称语义，我们也使用指称语义，但将从更实用的角度出发－－即（定义）解释器。它将引导我们最终实现『可扩展副作用』，一种在实际编程中管理副作用的实用方法。

本节将演示众所周知的所谓『不稳定指称』问题，John Reynolds 于 1974 就指出这是使用指称语义研究和定义实际编程语言以及其副作用的绊脚石。而在第三节，本文介绍了来自进程演算的洞见并解决这个问题。

为具体起见，本文使用 Haskell 语言来编程定义解释器，不过实际上也可以使用 OCaml、F# 或者 Scala 等语言。但即使是不熟悉 Haskell 的读者也可以通过阅读代码并类比常规数学符号来理解本演讲的主要思想。毕竟，在访问异国他乡时，纵然有语言和文化障碍，我们也能满足生存需求并且享受旅途。沟通的意愿最为重要。

定义解释器

本节用一个极其简单的例子展示用定义解释器的方法描述指称语义。虽然简单，但是足以说明什么是『可扩展解释器』问题。

首先从最简单的由算术表达式组成的语言开始，该语言由整数字面量，递增函数，以及用于应用递增函数的应用操作符组成。在 Haskell 中，我们用 Expr 数据类型定义语言 。示例表达式 tinc 代表『整数字面量 2 递增两次』：

data Expr = EInt Int | EInc | EApp Expr Expr
tinc = EApp EInc (EApp EInc (EInt 2)) -- inc (inc 2)

现在引入指称语义来赋予 Expr 含义。『指称语义』是从 Expr 到其他东西的可组合映射。下面定义的数据类型 Dom 包含了整数、布尔值、函数和标记『无意义表达式』的特殊元素，我们用这个有些通用的语义域为我们的语言中的表达式赋予含义，或者说指称。

data Dom = DError | DInt Int | DBool Bool | DFun (Dom -> Dom)

然后构造性地定义『语义（从 Expr 到 Dom 的映射）』为 Haskell 函数 eval。即我们的简单语言的解释器：

eval :: Expr -> Dom
eval (EInt x) = DInt x
eval EInc     = DFun $ \x -> case x of
                          DInt n -> DInt (succ n)
                          _      -> DError
eval (EApp e1 e2) = case eval e1 of
  DFun f -> f (eval e2)
  _      -> DError

EApp EInc (EInt 8) 代表我们的语言中的 inc 8，其含义为 Haskell 整数 DInt 9。eval 的最后一个子句说明了何为组合性：EApp e1 e2 的含义取决于 eval e1 和 eval e2。即仅取决于参数 e1 和 e2 的含义，而不取决于参数本身，或者说不取决于参数的结构。指称语义实际上是用结构化归纳解释器（fold）定义的。

该语言急需像布尔值、整数相等判断和条件表达式这样的新功能。可惜，Haskell 中的数据类型是不可扩展。为了添加新特性必须重新定义 Expr：

data Expr = EInt Int | EInc | EApp Expr Expr
          | EEq | EIf Expr Expr Expr

下面定义的 tif 即示例条件表达式：if 3 == inc (inc 2) then 10 else inc (inc (inc 2))。虽然我们想复用上面的 tinc 取代 inc (inc 2)，但却不能这么做：Expr 的类型已经变了，必须用新的 Expr 重新定义 tinc 这看起来一模一样的表达式。

tinc1 = EApp EInc (EApp EInc (EInt 2))
tif   = EIf (EApp (EApp EEq (EInt 3)) tinc1) (EInt 10) (EApp EInc tinc1)

下面为扩展后的语言赋予指称。前三个子句看起来和旧解释器里的一模一样，同样可惜的是我们无法复用它们，必须重新编写：Haskell 中的函数也不可扩展。

eval :: Expr -> Dom
eval (EInt x)      = DInt x
eval EInc          = -- ... 同上 ...
eval (EApp e1 e2)  = -- ... 同上 ...
eval EEq           = -- 类似于 EInc
eval (EIf e et ef) = case eval e of
  DBool True  -> eval et
  DBool False -> eval ef
  _           -> DError

至此，我们发现了其中的不稳定性，或者说『表达式问题』：我们的指称语义太过脆弱，无法扩展。当语言添加特性时，无法复用已有的项的解释器。或许可以反驳说这是 Haskell 的缺陷而非是指称语义的缺陷，但仍说明了一些问题。指称语义常常以数学的方式呈现，数学尽管严格，但通常是非形式化的。形式化的过程中会遇到很多问题。幸运的是，有一种方法可以让我们的解释器变得可扩展。

可扩展解释器

让我们回到只有整数和递增的最简单的语言里，用另一种方式定义之。我们之前把语言定义为数据类型，然后用函数解释为 Dom。现在我们直接编写『语言项如何映射到其指称』以及『如何从子项的指称中组合成复合项的指称』来定义语言，这样无须中间的eval 步骤便引入了指称语义－－毕竟，『语义』的定义其实也自然包含了『语言的结构（语法）』的定义。为了通用起见，下面用类型变量 d 而非具体的 Dom 表示语言的指称的域（在后面的部分有用）。总而言之，我们的语言由一组『定义』组成，对于每一种语法形式，都有一个其到语义域的映射。语义域是抽象的而非具体的。在 Haskell 中我们将语言定义为 typeclass（或者 OCaml 中的 module 类型，诸如此类）：

class EBasic d where
  int :: Int -> d
  inc :: d
  app :: d -> d -> d

infixl 1 `app`   -- 令中缀运算符 `app` 左结合

该 typeclass 表明我们的语言有整型字面量以及递增两个原子表达式，一个含有两个子表达式的复合表达式 app。从设计的角度看，复合表达式的含义由其子表达式决定，其语义当然是可组合的。我们举例的项 inc (inc 2) 现在有以下形式

ttinc = inc `app` (inc `app` int 2)

推导出其类型为 ttinc :: EBasic d => d。读者可以这样理解：ttinc 是 EBasic 语言中的一个项。也可理解为：给定一个合适的域，ttinc 在该域中为构成我们的语言的原子表达式以及复合表达式（即 inc (inc 2)）赋予指称。

instance EBasic Dom where
  int = DInt
  inc = injI succ
  app (DFun f) e2 = f e2
  app _ _         = DError

injI succ 表示把 Haskell 函数 succ 提升至 Dom 中，且当要递增的值不是 DInt时直接返回 DError。示例表达式的含义为 ttinc :: Dom，即 ttinc 特化到了域 Dom 类型。

像之前一样，我们要把表达式映射到其含义，即 Dom 中的元素。此前这种映射是由 Haskell 函数 eval 实现的。现在，它被连接到 ttinc 本身，而对原子表达式的一系列映射则收集在 EBasic 中。由此我们明白，数学中的映射并非一定要对应于 Haskell函数，也可以用其他编程手段。数学是抽象的，这是它的优点，说明它适用于很多情况。但同时也是它的缺点，因为人们必须知道如何正确应用它。

在新方法中扩展语言要容易得多。若要添加相等判断以及条件分支语句，只需写下对应的定义，然后组装到一个新的 typeclass 中：

class ECond d where
  eq  :: d
  if_ :: d -> d -> d -> d

可以立即使用新特性

ttif = if_ (eq `app` (int 3) `app` ttinc) (int 10) (inc `app` ttinc)

现在我们复用了而非重写之前写过的 ttinc。同理，我们复用而非重写解释器。ttif 推导出的类型 (EBasic d, ECond d) => d 告诉我们：为了给该表达式赋予含义，需要基本表达式和条件表达式到语义域的映射。此前已定义过 EBasic 到 Dom 域的映射，剩下的就是新特性的了：

instance ECond Dom where
  eq = -- 类似 inc
  if_ (DBool True)  et ef = et
  if_ (DBool False) et ef = ef
  if_ _             _  _  = DError

小结：新的指称语义式语言定义方法能使我们轻松地扩展语言，复用而不是重写已有的定义，表达式和解释器。因此，我们得到了一个方便的语义分析框架。下面应用其到实际副作用 State 中。

定义 State

本小节为我们的已经包含递增和条件表达式的语言添加第一个副作用：全局可变整数状态。这也使我们面临指称语义的真实问题。

起初，添加全局可变状态和它的两个操作原语很顺利。先定义『访问当前状态』和『更改当前状态之后返回之』的原子表达式：

class GlobalIntState d where
  get :: d
  put :: d -> d

以下为例

ttS :: (EBasic d, ECond d, GlobalIntState d) => d
ttS = if_ (eq `app` (int 3) `app` (put ttinc))
          (put (int 10)) (put (inc `app` get))

因为 ttinc 中包含之前定义的递增，所以 ttS 同时展示了新操作和旧操作。写起来容易，为其赋予含义却难得多。我们应当如何将 get 操作映射到 Dom 中？『当前全局状态』会发生变化，没有固定值，因而需要一个新的『状态转换器』语义域表示它。该语义域要能把当前状态映射到新状态，也要能基于不同的当前状态赋予表达式不同含义。

type DomIntState = Int -> (Dom,Int)

instance GlobalIntState DomIntState where
  get   = \s -> (DInt s,s)
  put e = \s -> case e s of
      (DInt s',_) -> (DInt s',s')
      (_,s)       -> (DError,s)

唉，为了赋予 ttS 含义，我们还需要 EBasic DomIntState 和 ECond DomIntState 实例以在新语义域中解释已有的语法。不过这很简单，只需复用已有的定义并稍加修饰，以 app 为例：

instance EBasic DomIntState where
  int x = \s -> (DInt x,s)
  inc   = \s -> (injI succ,s)
  app e1 e2 = \s0 -> let (f,s1) = e1 s0
                         (x,s2) = e2 s1
                     in (app f x,s2)

instance ECond DomIntState where
  eq = \s -> (eq,s)
  if_ e  et ef = \s -> case e s of
    (DBool True,s)  -> et s
    (DBool False,s) -> ef s

尽管可以我们举出可以许多证明这个 app 实现合理且够用的例子，但它其实并没有应有的那么完善。具体原因请读者自行思考。第二个随文小测是：为什么我们不能复用 Dom 语义域下的 if_ 解释器。

其实，问题不在于为新语义域写 EBasic、ECond 的实例有多复杂，而在于我们必须这么做。如果我们想添加有多个组件组成的（可变变量）全局状态怎么办？我们必须引入令一个语义域，然后又重新写 EBasic、ECond 的实例。对于具有许多特性的语言来说这是一个无法忽略的问题。另一方面，这也让人十分不满意：像 EInt 1 这样的整型字面量或者递增 EInc 的『实际』含义没有改变。整数永远表示整数，递增永远表示某个整数的后继数。无论语言是否有状态，它们的含义都保持不变。当为了越来越复杂的语言特性而扩张语义域时，不应该重新思考已有的事物在新语义域的含义。

头等函数？

至少在最开始的时候，头等函数和全局状态一样易于添加。只需定义该特性的基本操作：『访问某个已绑定的（绑定到某个名字）变量的值』，还有『创建函数』：

type VarName = String

class Lam d where
  var :: VarName -> d
  lam :: VarName -> d -> d

问题在于在所有之前定义的语义域都不能正确地赋予这些操作含义：变量不与任何固定的值关联，只有应用函数时才会绑定到某个值。对于不同变量，这样的过程可能会发生多次。需要一个新的语义域来表示『表达式的含义取决于其上下文』这一概念，即为变量提供指称语义的『环境』。

type DomFCF = Env -> Dom
type Env    = VarName -> Dom

尽管 DomFCF 看起来可能适用于 var 和 lam，但实际并非如此。其中原因留作读者思考。

如果我们想要按名调用的函数怎么办？协程？非确定性运算？我们需要越来越多的语义域。每个新域都需要相应的 EBasic 和 ECond 实例，才能在这些奇形怪状的语义域中赋予整数和递增含义。这就是问题所在：表达式没有稳定的指称语义。当语言扩展后，旧的表达式突然改变了含义。

交互

副作用与交互

不稳定的指称语义反映了表达式与其上下文的交互。滥觞于 Landin 和 Strachey 的传统编程语言语义研究方法很少涉足交互。正如 Robin Milner 在一次采访中所谈到：

But meanwhile [around 1971] I got somehow interested, and I don’t know how, in concurrency. I remember that, without linking it to verification particularly, I wondered about interacting automata. I had an idea that automata theory was inadequate, because it hadn’t said what it was for two automata to interact with each other. Except for the Krohn-Rhodes Representation Theorem, which said something about feeding the output of one automata into another. But there wasn’t interaction between the automata.
译文：与此同时（大约 1971 年左右）我对并发产生了兴趣，但我却感到无从下手。我记得当时我想研究自动机之间的交互，不过没将它与程序验证联系在一起。我认为自动机理论是不完善的，因为它没有描述两个自动机之间如何交互。除了 Krohn-Rodes 定理，该定理提到了『把一个自动机的输出输入到另一个自动机』之类的东西，但它也没有涉及自动机之间的交互。

『交互』这一主题贯穿于下列学者的研究中：

  • Petri，1939（年仅 13 岁）以及 1962（PhD 论文）
  • Hewitt，1976
  • Fifth Generation Project, 1982-1992
  • Robin Milner，20 世纪 80 年代
  • 本田耕平，20 世纪 80 年代末
  • Cartwright 与 Felleisen，1994

特别值得注意的是 Hewitt 极具影响力的《Viewing Control Structure as Patterns of Passing Messages》：该短文阐述了如何用 actor 之间的交互表达递归、迭代以及各种光怪陆离的控制结构。有传言道：『进程演算的每一步发展都不过只是把 Hewitt 的想法更加精确和形式化。』对于副作用而言，逻辑上的顶峰则是 Cartwright 与 Felleisen 的联合作品。下面将用现代语言和实践术语重构之。

引用资料

  • Robin Milner 访谈资料

http://users.sussex.ac.uk/~mfb21/interviews/milner/

  • Carl Hewitt: Viewing Control Structures as Patterns of Passing Messages

MIT A.I. Memo 410, 1976.

  • Robert Cartwright, Matthias Felleisen: Extensible Denotational Language Specifications

Symposium on Theoretical Aspects of Computer Software, 1994. LNCS 789, pp. 244-272.

稳定指称语义，可扩展副作用

通往稳定指称语义

现在，我们定义表达式的含义时，将明确考虑其与上下文的交互。我们遵循 Cartwright 与 Felleisen 的思路：

A complete program is thought of as an agent that interacts with the outside world, e.g., a file system, and that affects global resources, e.g., the store. A central authority administers these resources. The meaning of a program phrase is a computation, which may be a value or an effect. If the meaning of a program phrase is an effect, it is propagated to the central authority. The propagation process adds a function to the effect package such that the central authority can resume the suspended calculation.
译文：完整的程序可以视为与外部世界（如文件系统）交互并对全局资源施加影响（如存储）的代理，该类资源由某个『中央集权机构』负责管理。程序代码的含义是一种『计算』，可以是一个值，也可以是一种副作用。如果一段代码的含义是副作用，它将被传递给中央集权机构。传递时会在副作用中附加一个函数，以便中央集权机构恢复被暂停的计算。

Cartwright 与 Felleisen 的核心思想可用以下程序代码表示：

data Comp = Done DomC | Req ReqT (DomC -> Comp)

data DomC = DCInt Int | DCBool Bool | DCFun (DomC -> Comp)

从现在起，表达式的指称为 Comp。Comp 是 DomC（类似之前的 Dom）与副作用请求的无交并（disjoint union）。副作用请求 Req 中包含消息的回复到其接收者的映射（类型签名为 DomC -> Comp 的函数），即『返回地址』。ReqT 则表示具体副作用，即表达式到底要请求什么。目前的副作用是 ReqError，代表错误消息（稍后我们将揭示更多不同副作用）。

应用函数 err 会发送一个表示计算错误的副作用请求。与第二节中 Dom 不同的是，DomC 中不包含 DError 元素，我们把错误视为一种副作用：请求终止计算。

在 Comp 域为基本语言中的项赋予含义是很直观的。我们再写一个 EBasic 实例，我保证这是最后一次。

instance EBasic Comp where
  -- 旧
  int = Done . DCInt
  inc = Done . DCFun $ \x -> case x of
    DCInt x -> int (succ x)
    _       -> err
  app (Done (DCFun f)) (Done e2) = f e2
  app (Done _)         (Done e2) = err
  -- 新
  app (Req r k) e2 = Req r (\x -> app (k x) e2)
  app e1 (Req r k) = Req r (\x -> app e1 (k x))

上述实例中大部份代码类似于 EBasic Dom，这并不奇怪 。不过值得注意的是，无论语言中有什么副作用（请求），整数字面量都被映射到 DCInt Int，整数永远是整数。同理，inc 始终表示递增一个整数。为了实现副作用的传播，EBasic Comp 新增了两行有关 app 的处理子句：如果某函数应用的参数是副作用请求，则它会在修改『返回地址』之后再发送相同的请求，收到副作用请求的回复后重新尝试应用函数。事实上，副作用从子表达式中向上传播。

下面的示例项 ttinc 的指称的类型是 Comp（可以直接复用之前的 ttinc，因为它是多态的。但为了便于参考，下面重复了该定义。）

ttinc :: EBasic d => d
ttinc = inc `app` (inc `app` int 2)

-- *EDSLNG> ttinc :: Comp
-- Done (DInt 4)

在 Comp 域中赋予条件表达式含义也同样很直观：

instance ECond Comp where
  eq = ... -- 类似 inc

  if_ (Done (DCBool True))  et ef = et
  if_ (Done (DCBool False)) et ef = ef
  if_ (Done _)              _  _  = err
  -- 新
  if_ (Req r k) et ef = Req r (\x -> if_ (k x) et ef)

和 EBasic Comp 一样，大部份内容类似与旧的 ECond Dom 实例。新定义的最后一行描述的副作用传播，看起来和之前写的 app 的副作用传播没什么不同，这样的重复描述有点令人厌烦。下面将这一通用模式重构成为一个单独的函数，然后重写 ECond Comp 使其更清爽：

instance ECond Comp where
  eq = ...
  if_ e et ef = bind e $ \x -> case x of
    DCBool True  -> et
    DCBool False -> ef
    _            -> err

bind :: Comp -> (DomC -> Comp) -> Comp
bind (Done x) k    = k x
bind (Req r k1) k2 = Req r (\x -> bind (k1 x) k2)

bind e k 代表了一种的常见的消费表达式 e 的模式：如果表达式不代表值，而代表发送副作用请求，那么修改请求的返回地址然后传播之。看起来是不是有点眼熟？在交互的视角中，Monad 的登场是自然而然的。事实上，Mike Spivey 与 Moggi 差不多在同一时间提出将范畴论中的 Monad 应用于编程语言，他所推崇的『错误传播』思想与我们方才展示的并无二至。

引用资料

  • Eugenio Moggi: Computational lambda-calculus and monads

LICS 1989.

  • Mike Spivey: A functional theory of exceptions

Science of Computer Programming, v14, 1990.

无痛 State

到目前为止，唯一的副作用是错误传播。是时候添加一个真实的副作用来展示新方法的关键之处了：全局可变整数状态。我们仍需要再写一个 EBasic 的实例吗？之前的项ttinc :: Comp 的原有指称语义可以与新的副作用操作一起使用吗？我们将一探究竟。

在第 1 节中已经定义了用于获取和更新当前状态的 get 与 put 操作。下面重复其定义和示例项 ttS 以便参考：

class GlobalIntState d where
  get :: d
  put :: d -> d

ttS :: (EBasic d, ECond d, GlobalIntState d) => d
ttS = if_ (eq `app` (int 3) `app` (put ttinc))
          (put (int 10)) (put (inc `app` get))

在第 1 节中，为了给 get、put 以及 ttS 赋予含义，必须引入特殊的语义域 DomIntState，以及为对应的 EBasic 等 typeclass 实现实例。而新方法中只要有 Comp 就足够了，我们将揭示 ReqT 更多的部分：获取和更新状态的请求。

data ReqT = ReqError | ReqState StateReq ...
data StateReq = Get | Put Int

instance GlobalIntState Comp where
  get   = Req (ReqState Get) Done
  put e = bind e $ \x -> case x of
    DCInt x -> Req (ReqState (Put x)) Done
    _       -> err

get 与 put 的含义 ReqState 请求：如，get 发送获取请求，收到回复后立刻返回。由于我们没有改变 Comp，EBasic Comp 和 ECond Comp 之前也定义过了，我们立刻可以看到 ttS 的含义

*EDSLNG> ttS :: Comp
ReqState (Put 4)

ttS 代表『将当前状态更新为 4』的请求，剩余计算的含义（GHCi 此处未打印）则取决于该请求的回复。鉴于我们暂时还没有任何副作用处理程序，它已经做到最好了。ReqError 不是用来回复的，未处理的 ReqError 代表一个错误。不过我们应该回复 ReqState，并按其要求获取和更新全局状态。

handleState :: Int -> Comp -> Comp
handleState _ (Done x)    = Done x
handleState s (Req (ReqState r) k) = case r of
  Get   -> handleState s $ k (DCInt s)
  Put s -> handleState s $ k (DCInt s)
-- 其他请求
handleState s (Req r k) = Req r (handleState s . k)

处理程序 handleState 即 Cartwright 与 Felleisen 所探讨的『权力机构』，负责管理资源（本例中为可变状态）并批复副作用请求。当处理程序收到某计算发送给它的 Get 请求时，它回复其当前状态。handleState 中最后一行把 ReqState 以外的请求向上传播。这也是本文的方法与 Cartwright 与 Felleisen 方法的不同之处：本文方法中不存在程序之外的中央集权机构。副作用处理程序是本地化的，可以作为程序的一部分，从而形成一种官僚机构。若某处理程序无法处理某件事，它会将这件事移交给上级。

ttS 的副作用处理程序的初始状态为 0，因此 ttS 的含义为 DInt 5。注意到这里的处理函数会递归调用自身，这是因为收到处理程序的回复之后，表达式可能会再次发送请求。严格来说，副作用处理函数建立的数学映射是不动点，为了形式化永不终止的运算，需要隐式引入 Done bottom。之前我们没有看到 bottom，是因为之前没有发散的计算。顺便一提，如果表达式无休止地发送 Get 请求，那么它不是发散的计算，而是一个生产副作用请求的流。

由上可见，Cartwright 和 Felleisen 的想法确实可行！当添加真实的副作用时无需重写任何之前的语义域或解释器。你可以在任意含副作用的表达式中使用整数字面量，而无论有什么副作用它都是整数。Cartwright 和 Felleisen 的想法比它们所描述的效果更好：我们把副作用处理程序模块化了，每个程序都负责处理自己的副作用请求。

头等函数，第 1 次尝试

在第一节时我们尝试过扩展语言支持头等函数，结果发现为了支持头等函数需要进行如此深入和大量的的修改，不得不放弃了。现在我们在稳定指称语义的框架内再试一次。我们下面要做的事情，之前的『副作用作为交互』的框架中都没有尝试过。

第一节引入了带有下列操作的头等函数，以 th0 为例：

type VarName = String

class Lam d where
  var :: VarName -> d
  lam :: VarName -> d -> d

th0 = lam "x" (inc `app` var "x") -- 递增函数 (η-扩展 后的形式)

现在用 Comp 为 var 和 lam 赋予含义。var 操作有点类似与之前的访问当前全局状态的 get 操作。

data ReqT = ReqError | ReqState StateReq | ReqHO HOReq
data HOReq = ReqVar VarName 

instance Lam Comp where
  var v      = Req (ReqHO (ReqVar v)) Done
  lam v body = Done . DCFun $ \x -> handleVarD [(v,x)] body

type Env = [(VarName,DomC)]

handleVarD :: Env -> Comp -> Comp
handleVarD _ (Done x) = Done x
handleVarD env (Req (ReqHO (ReqVar v)) k) | Just x <- lookup v env =
  handleVarD env $ k x
-- everything else
handleVarD env (Req r k) = Req r (handleVarD env . k)

看起来确实能正常运行，如 app th0 ttinc :: Comp 得到 5，符合我们的预期。但是，

*EDSLNG> (lam "z" (lam "x" (var "z" `app` var "x"))) `app` inc `app` int 1 :: Comp
ReqHO (ReqVar "z")

（上述函数可以视为计算 inc 1 的花哨版本）返回了对变量 z 的值的请求－－即变量未绑定错误。读者能猜出来哪里出问题了吗？

词法作用域下的头等函数

在稳定指称语义框架下第一次尝试实现头等函数就遇到了可预见的问题：我们无意中为绑定变量实现了动态作用域，而非词法作用域。令人感到不可思议的是：动态作用域是如此自然，以至于人们实现 λ-演算 时首先就想到它，难怪 John McCarthy 和 Alan Turing 都搞错了。需要花费更多精力才能发现和实现词法作用域。毕竟，『闭包』这一术语是 Landin在 1964 年才提出的，比 λ-演算 的首次发表晚了 20 余年。

现在我们重新观察之前编写的实现了动态绑定的代码中的关键部分：

lam v body = Done . DCFun $ \x -> handleVarD [(v,x)] body

handleVarD env (Req (ReqHO (ReqVar v)) k) | Just x <- lookup v env =
  handleVarD env $ k x
handleVarD env (Req r k) = Req r (handleVarD env . k)

创建头等函数非常简单：只需将函数体包装在处理『请求 lambda 绑定的变量 v 的值』的程序中。如果函数体还请求其他变量，那么 handleVarD[(v,x)] 将把这些请求传播出去，交给（动态）作用域内的其他处理程序。因此，创建头等函数毋需上下文信息，遑论上下文交互，我们称这样的操作是『纯』的。另一方面，将这样的头等函数应用于一个值时，可能会发送 ReqVar 请求 v 之外的变量。因此，函数的应用并与其上下文有关，所以是有副作用的。

词法作用域的情况却恰恰相反。如上文所说，创建词法作用域里的函数需要捕获创建时的变量环境（绑定上下文），即 Landin 指出的『封闭其上下文』。所以创建闭包确实需要引用上下文，按我们的定义，这样的操作是有副作用的。当应用一个闭包时，闭包所捕获的环境会满足所有『解引用变量』请求。

data ReqT = ReqError | ReqState StateReq | ReqHO HOReq

data HOReq = ReqVar VarName | ReqClosure VarName Comp
type Env = [(VarName,DomC)]

instance Lam Comp where
  var v      = Req (ReqHO (ReqVar v)) Done
  lam v body = Req (ReqHO (ReqClosure v body)) Done

handleVar :: Env -> Comp -> Comp
handleVar _ (Done x) = Done x
handleVar env (Req (ReqHO r) k) = case r of
  ReqVar v | Just x <- lookup v env -> handleVar env $ k x
  ReqVar _  -> err          -- unbound variable
  ReqClosure v body ->
    handleVar env $ k (DCFun $ \x -> handleVar ((v,x):env) body)
-- everything else
handleVar env (Req r k) = Req r (handleVar env . k)

现在，我们将函数体包裹在 handleVar ((v,x):env) 中执行，handleVar 表达式不仅处理与 v 变量（创建闭包的 lambda 绑定的变量）有关的 ReqVar 请求，同样处理函数体内有关其他变量的请求。当应用闭包时，变量请求不会传播到闭包外并要求上下文处理。应用闭包是上下文无关的：闭包是纯的。

另一方面，创建闭包时必须查询上下文中绑定的所有变量。因此『捕获环境』这一行为是种副作用。lam 形式向上下文发送 ReqClosure v 请求以捕获环境，当该请求到达解释器 handleVar 时（回想一下，它包含有关在其范围内绑定的变量的完整信息）。解释器把其变量环境传递给函数体内部的处理程序从而创建闭包。顶层没有任何变量，所以顶层的 handleVar [] 传递空环境。现在：

handleVar [] $ (lam "z" (lam "x" (var "z" `app` var "x"))) `app` inc `app` int 1 :: Comp

的含义是我们预期的：整数 2。

上述例子证明了，即便添加了词法作用域的头等函数，之前定义的语言特性也保持了稳定的指称语义。无论是否在函数体内，递增 inc 仍表示递增数字，整数字面量仍意味着整数，这种指称语义方法令人联想起在 π-演算 中嵌入 λ-演算 的方法。可能令人出乎意料的是，在我们的语义中 lam 是一种副作用。不过读者也不必对此过分惊讶：毕竟，创建闭包必须与上下文交互，并且要为变量环境分配内存。FX 语言2和 ATS 语言3同样将创建闭包视为一种副作用，这并非偶然。

可扩展的副作用

细心的读者可能已经发现，本文将 ReqT 默认为可扩展的。但 Haskell 数据类型是不可扩展的，在本文附带的源代码中，ReqT 预先定义为包含了本文使用到的三种副作用请求类型，在实践中这种做法是不可能的。

所幸的是通过嵌套『余积（coproduct）』类型（即 Either 类型）来引入可扩展的请求类型不会太痛苦－－Haskell 以及其他语言中的可扩展副作用库正是这样做的。最终我们得到了真正的可扩展，有类型的，能让我们的程序使用任意想要的副作用的框架。

引用资料

具体见论文 《Freer Monads, More Extensible Effects》中的第 2.5 节。

高阶函数编程是一种副作用

我们认为高阶函数与各种副作用的交互的核心问题可以通过消除他们之间的区别来解决：高阶函数特性自身就是一种副作用，和全局状态副作用没有本质上的不同。

本文证明了，人们可以将头等函数抽象与其他任意副作用一视同仁，从而完善了 Cartwright 与 Felleisen 的《Extensible Denotational Language Specifications》：变量替换与解引用一个 C 语言式的变量没有区别，而 lambda，或者说创建闭包，也是一种副作用。其函数体执行期间发生的所有变量解引用副作用都由闭包处理。我们的方法可以统一处理动态作用域与词法作用域，以及各种调用约定。

本文将『λ-抽象』视为带有副作用的表达式，这有点类似于 call-by-push-value 演算4和 ATS 语言和 FX 语言。但与这些演算和语言不同的是，我们也将『变量』视为带有副作用的表达式。绑定变量本质与其典型编译方式编译后生成机器码表示一样，是对在头等存储中分配的引用单元赋值。我们的方法有望忠实地描述分布式或异构系统，在这些系统中，解引用变量产生往往是一种非平凡的副作用。

习惯上人们将副作用设计为 λ-演算 的扩展，并使用以下的熟悉的类型断言

$ \Gamma \vdash \mathcal{M}\;\colon\;\mathtt{T\;e\;a}$

即表达式 $\mathcal{M}$ 的类型为 $\mathtt{T\;e\;a}$ 。其中 $\mathtt{a}$ 是求值该表达式会产生的值的类型， $\mathtt{e}$ 则代表求值该表达式产生的副作用的类型。 $\mathtt{T}$ 则是一个双参数的类型构造器，读者可以类比 Indexed Monad。$ \Gamma $ 则是耳熟能详的『类型环境』。在此提出我的一得之见：将类型断言简化为

$ \vdash \mathcal{M}\;\colon\;\mathtt{T\;e\;a}$

即移除类型环境，甚至也移除作为基础的 λ-演算。那么，我们要如何判断诸如 $\mathrm{x+1}$ 这样的带有自由变量的表达式的类型呢？ $\mathrm{x}$ 的类型从何而来？考虑 $\mathrm{ask+1}$ ，为了为这样带有副作用的表达式赋予类型，我们假设 $\mathrm{ask}$ 是一个生成整数的带有副作用的操作。我们这样写

$\vdash \mathrm{ask+1} \;\colon\;\mathtt{T}\,\{\mathrm{ask}\colon\mathtt{int}\}\,\mathtt{int}$

我们把副作用标记 $\{\mathrm{ask}\colon\,\mathtt{int}\}$ 视作表达式中副作用操作 $\mathrm{ask}$ 的绑定：即作为副作用的类型环境。注意解引用变量同样也是一种副作用！因此有

$\vdash \mathrm{x+1}\;\colon\;\mathtt{T}\,\{\mathrm{x}\colon \mathtt{int}\}\,\mathtt{int}\\ \vdash \mathrm{ask+x}\;\colon\;\mathtt{T}\,\{\mathrm{x} \colon \mathtt{int}, \mathrm{ask} \colon \mathtt{int}\}\,\mathtt{int}\\ \vdash \mathrm{\lambda x. ask+x}\;\colon\;\mathtt{T}\,\{\mathrm{ask} \colon \mathtt{int}\}\,(\mathtt{int} \to \mathtt{int})\\ \vdash \mathbf{handle}\;\mathrm{ask+x}\; \mathbf{with}\;\mathrm{ask}\Rightarrow10\;\colon\;\mathtt{T}\,\{\mathrm{x}\colon\mathtt{int}\}\,\mathtt{int}$

鉴于副作用标记可以描述尚未被处理的副作用的类型环境，那么它也可以完美的描述尚未绑定的变量的类型。$ \Gamma $ 确实是多余的。

而整个程序 $\mathcal{P}$ 应是『封闭』的。

$ \vdash \mathcal{P}\;\colon\;\mathtt{T}\,\{\}\,\mathtt{a} $

它不应该有尚未绑定的变量，也不应该有尚未处理的副作用。

总而言之，类似『可扩展副作用』这样的框架在把 λ-演算 的函数抽象和函数应用视为带有副作用的操作时不会有任何问题，即 HOPE（High-Order Programming is an Effect，高阶编程是一种副作用）

引用资料

ICFP 2017 附属 HOPE 研讨会上发表的演讲幻灯片。September 3, 2017. Oxford, UK。

结论

何为副作用？副作用即为与上下文的交互。若某表达式向其上下文发送消息，那么它是有副作用的。词法作用域的 lambda 必须向上下文询问绑定环境，因此是有副作用的。在求值闭包的函数体时，函数体会请求访问自由变量。然而完整的闭包可以处理所有此类请求，在没有全局状态、IO 等其他副作用的情况时，不再需要进一步的上下文交互。因此闭包是无副作用的，纯的。

某事物是否存在副作用则取决于我们看待它的方式。当专注于计算的一小部分时，无论是访问外部存储还是访问绑定变量都是一种副作用。由于创建闭包，甚至 lambda 也可视为有副作用的。

我们是否应该将 Lambda 或者 State 视为副作用？这取决于我们的实际工作：我们在求值某个表达式，还是要编译它？我们是否只对表达式的求值结果感兴趣，还是对求值的时间复杂度也感兴趣？副作用作为一种便利和抽象可以让我们专注于系统的一小部分，而将其余部分视为通过固定的协议进行交互的『上下文』。不同的协议可以做到不同程度的等式推理。这就是为什么当我们讨论副作用时，明确并注意这一点是如此重要。

参考

  1. 1967 年，IBM 维也纳实验室启动了一个形式化研究编程语言 PL/I 的项目，在 《Extensible Denotation Language Specification》中，Cartwright 与 Felleisen 称其为『Vienna School of Denotations』，即『维也纳指称语义学派』 ↩︎

  2. https://www.researchgate.net/publication/235093309_Report_on_the_FX-91_Programming_Language ↩︎

  3. https://www.cs.bu.edu/~hwxi/atslangweb/ ↩︎

  4. https://ncatlab.org/nlab/show/call-by-push-value ↩︎