Having an Effect

Oleg Kiselyov (okmij.org). 页面最后更新于2025年9月5日.

翻译术语对照

引论

这项研究是一段追随一条诱人线索的旅程: 关于单子 (monad), 单子变换器 (monad transformer), 自由单子 (free monad) 和可扩展效应 (extensible effect) 的奠基性论文全都是关于可扩展解释器的. 一路上我们已经意识到, 表达式问题 (expression problem), 稳定指称 (stable denotation), 以及可扩展解释器全都是同一事物的不同名字. 我们最终找到了组织原则: 交互——在客户端和服务器之间, 解释器和被解释的代码之间, 表达式和其上下文之间.

很可能交互最好是在进程演算 (process calculus) 中表达. 在顺序演算中, Cartwright和Felleisen的Extensible Denotational Language Specifications是将效应作为交互的最早的完全成熟的严格陈述.

• 本报告给出了Cartwright和Felleisen的方法的现代重构. 我们的重构更简单, 得益于tagless-final陈述, 并且可以立即执行.
• 进一步发展, 我们使得效应处理器 (effect handler) 本身是模块化的和可扩展的——成为程序的一部分, 而不是永久地驻扎在外面. 这使得以下这一步成为可能:
• Cartwright和Felleisen不得不将变量环境烤进基本的语义框架之中, 即便整数, 或者一般而言的一阶子语言, 并不使用它. 我们避免了假定变量环境以及对于高阶的任何特殊处理. 毕竟, 我们将Lambda与State平等对待, 在同一个统一的形式体系之中. 动态或者词法绑定或者各种调用约定归结为处理解引用一个绑定变量的效应的不同方式.

重访这一领域的起源并找回其洞见和被遗忘的替代方案有助于使得我们的程序具有预期的效应.

本报告首先于2016年8月25日在Indiana大学信息学与计算学院 (SoIC) 计算机科学讨论会上呈现. 我感谢Martin Berger的许多有益的讨论, 特别是解释了进程演算的起源. 感谢Shin-Cheng Mu和Matthias Felleisen的有益评论.

版本

当前版本为2017年9月.

参考文献

• EDSLNG.hs——本报告背后完整的, 基本上是Haskell98的代码.
• edlsng.ml——OCaml版本: Cartwright-Felleisen框架的现代重构. 状态, 动态绑定, 传值调用和传名调用的词法绑定是示例效应.
• 于2016年12月2日在台湾台北中央研究院资讯科学研究所讨论会上的报告录像: https://www.youtube.com/watch?v=GhERMBT7u4w

第1章 不稳定的指称, 脆弱的解释器, 难以应用的理论

第1.1节 从实用角度来看指称语义

既然(副)效应无处不在又富有争议, 它们就应该被研究. 而它们也已经被研究过了, 尤其是, 被1970年代的指称语义维也纳学派——其目标是理解PL/I. {译注: 原文此处写作PL\1, 应为笔误.} 我们也将使用指称语义——但是带有实用的倾向, 朝向(定义性)解释器. 它最终将我们引向可扩展效应——一种在现实程序中管理效应的实用方式.

在这一节中, 我们演示众所周知的不稳定指称的问题. 它是使用指称语义研究和定义现实语言及其效应的绊脚石, 正如John Reynolds早在1974年首先指出的那样. 第3章带来了来自进程演算的洞见以克服这一问题.

为了具体起见, 我们将使用Haskell来编写我们的定义性解释器, 尽管OCaml, F#或者Scala, 以及其他语言, 也同样可以. 即便是不熟悉Haskell的读者, 希望也能够通过观察代码并与标准数学记号进行类比, 而领会主要思想. 毕竟, 当拜访异国他乡时, 尽管有语言和文化的隔阂, 我们也能设法生存下来并享受旅程. 交流的意愿大有帮助.

第1.2节 定义性解释器

我们在一个简单到令人尴尬的例子上解释指称语义的定义性解释器方法. 尽管它很平凡, 这个例子已经能够说明需要可扩展解释器的理由.

我们从最简单的算术表达式语言开始: 整数字面量, 增量函数, 以及让我们能够应用增量的应用运算符. 在Haskell中, 我们将这个语言定义为数据类型Expr:

data Expr = EInt Int | EInc | EApp Expr Expr

tinc = EApp EInc (EApp EInc (EInt 2)) -- inc (inc 2)

现在我们引入指称语义以赋予Expr意义. 回忆一下, 指称语义是一个从Expr到其他某种东西的复合性的映射. 我们取下面这个在某种程度上通用的domain Dom作为我们的语言中的表达式的意义, 或者说指称. 它包含整数, 布尔值, 函数, 以及一个代表无意义的表达式的意义的特殊元素.

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

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, 而DInt 9是其意义, 一个Haskell整数. 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

if 3 == inc (inc 2) then 10 else inc (inc (inc 2))

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

解释器eval赋予扩展后的语言以意义. 前三个子句看起来与旧的解释器完全一样. 唉, 我们不能引用它而不得不重新写: Haskell中的函数也是不可扩展的.

eval :: Expr -> Dom
eval (EInt x)      = DInt x
eval EInc          = -- ... as before ...
eval (EApp e1 e2)  = -- ... as before ...
eval EEq           = -- similar to EInc
eval (EIf e et ef) = case eval e of
  DBool True  -> eval et
  DBool False -> eval ef
  _           -> DError

因此我们遇到了不稳定性, 或者说表达式问题: 我们的指称语义是脆弱的而且不可扩展. 我们不能重用之前写过的示例项和之前写过的解释器; 我们不得不重写它们. 可以说, 这是Haskell形式化的问题而不是指称语义的问题. 但它仍然很能说明问题. 通常指称语义是以数学的方式陈述的, 而数学通常是非形式的, 尽管仍然是严格的. 许多问题在形式化中才浮现出来. 幸运的是, 有一种方法可以使得我们的解释器可扩展.

第1.3节 可扩展解释器

让我们回到最简单的整数和增量的语言, 并以不同的方式定义它. 不使用随后不得不被解释为Dom的数据类型, 让我们通过直接告知每个语言句法成分的意义, 以及如何从其组成部分的意义理解一个复合句法成分, 来定义一个语言. 因此我们一开始就引入指称语义, 而没有中间的eval步骤. 毕竟, 定义语义包括定义语言的结构 (句法). 为了一般性, 这在后面会派上用场, 我们并不将指称的domain固定为Dom. 而是, 我们使它成为变量d. 总而言之, 我们通过一组定义来定义一个语言, 每个句法形式一个定义, 每个定义都为该形式定义了domain映射. domain保持抽象. 因此我们将一个语言定义为Haskell中的一个类型类 (或者OCaml中的一个模块类型, 等等):

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

infixl 1 `app`   -- make the infix `app` left-associative

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

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

和之前一样, 我们将一个表达式映射到了其意义, 即Dom的元素. 早先, 这个映射是由Haskell函数eval实现的. 现在, 它被内置于ttinc本身, 而原语的映射被收集在EBasic中. 因此我们已经认识到了数学映射并不一定要对应于一个Haskell函数. 还有其他方式可以编写它.

数学是抽象的, 这是一种福气——它适用于如此之多的情形——也是一种诅咒: 人们必须知道如何应用它.

在新的方法中扩展语言要容易得多. 为了添加相等和条件形式, 我们只需写下相应的定义, 将它们收集到一个新的类型类之中:

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

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

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

总结一下, 定义语言的新方式, 通过指称语义, 让我们能够轻易地扩展语言——重用而不是重写, 之前写过的定义, 解释器和表达式. 因此我们得到了用于语义分析的方便的框架. 现在我们将把它应用于真正的效应, 状态.

参考文献

• Tagless-final风格

第1.4节 定义状态

这一小节为增量和条件的语言添加第一个真正的效应: 全局可变整数状态. 它也让我们直面指称语义的真正问题.

起初, 添加带有其两个操作的状态效应进展顺利. 我们定义原语以访问当前状态以及改变它, 返回新的值:

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))

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实例: 旧特性在新domain中的解释. 诚然, 这是直截了当的, 仅仅是修饰和重用早先的定义, 例如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的意义是合理的并且对于许多例子而言足够了, 但它并不如应有的那般一般. 请读者思考为什么. 第二个小测验是为什么我们无法重用if_的Dom解释.

问题不在于为新的domain编写EBasic, ECond等实例的复杂性, 而在于我们不得不这样做这一事实. 如果我们想要添加带有若干分量 (可变变量) 的全局状态呢? 我们不得不引入另一个domain, 并且再一次编写EBasic, ECond实例. 对于具有许多特性的语言而言, 这是一个重大的实际问题. 这也是令人深感不满的: 诸如EInt 1这样的整数字面量或者增量EInc的真正意义并没有改变. 增量的意义是整数上的后继——无论语言是否具有状态. 整数永远是整数, 而不应该在为了越来越复杂的特性而扩展指称的domain时不得不被重新构想.

第1.5节 第一级函数?

第一级函数和状态一样容易添加, 至少在一开始是这样. 我们只需写下基本操作的签名: 访问绑定于一个(具名)变量的值, 以及创建一个函数.

type VarName = String

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

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

如果我们想要传名调用的函数呢? 协程呢? 非确定性呢? 我们需要越来越多的domain. 每个新的domain都需要重写EBasic, ECond实例, 以给出整数, 增量在这些更为花哨的domain中的意义. 这就是问题所在: 表达式不具有稳定的指称. 当语言被扩展时, 旧的表达式突然改变了意义.

第2章 效应和交互

不稳定的指称反映了一个表达式与其上下文的交互. 编程语言语义的传统方法, 从Landin和Strachey以降, 对于交互几乎没有什么可说的. Robin Milner在他的访谈中说得很好:

但是与此同时 [大约1971年] 我不知怎么地, 我也不知道是如何, 对并发产生了兴趣. 我记得, 并没有特别将其与验证联系起来, 我对交互自动机感到好奇. 我有一个想法, 即自动机理论是不充分的, 因为它没有说两个自动机彼此交互是什么意思. 除了Krohn-Rhodes表示定理, 其说了一些关于将一个自动机的输出馈入另一个的东西. 但是自动机之间并没有交互.

• Petri, 1939年 (13岁时) 和1962年 (博士论文)
• Hewitt, 1976年
• 第五代计算机计划, 1982-1992年
• Robin Milner, 1980年代
• Kohei Honda, 1980年代末
• Cartwright和Felleisen, 1994年

特别值得注意的是Hewitt的有影响力的笔记Viewing Control Structures as Patterns of Passing Messages: 它展示了递归, 迭代和复杂的控制结构如何都可以用参与者 (actor) 之间的交互来表示. 听说进程演算的所有进一步发展都是在使得Hewitt的想法更加精确和形式化. 就效应而言, 其逻辑上的顶点是Cartwright和Felleisen的工作, 我们在下面以现代语言和实用的术语重构它.

同样值得注意的是Abramsky和McCusker的Reynolds理想化Algol的博弈语义——其本质上是一个纯函数式语言, 除了new. Abramsky和McCusker的论文明确地将副作用称为一种交互:

我们想要将new x in C理解为将类型为var[X]的自由标识符x绑定到一个给出存储单元的行为的对象或者进程. 于是new x in C的行为来源于C与这个单元之间的交互...

参考文献

• 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.
• Samson Abramsky and Guy McCusker: Linearity, Sharing and State: a fully abstract game semantics for Idealized Algol with active expressions. Electr. Notes Theor. Comput. Sci., 1996, v3, pp. 2-14.

第3章 稳定指称, 可扩展效应

第3.1节 迈向稳定指称

现在我们以一种显式考虑表达式与上下文的交互的方式来定义表达式的意义. 我们追随Cartwright和Felleisen的引领:

一个完整的程序被认为是一个与外部世界, 例如文件系统, 交互, 并且影响全局资源, 例如存储, 的代理. 一个中央权威管理这些资源. 一个程序句法成分的意义是一个计算, 其可以是一个值或者一个效应. 如果一个程序句法成分的意义是一个效应, 它就被传播至中央权威. 传播过程为效应包添加一个函数, 使得中央权威可以恢复被挂起的算数.

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

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

data ReqT = ReqError ...

err :: Comp
err = Req ReqError (\_ -> err)

以Comp来给出基本语言的意义是相当直截了当的. 我们再写一个EBasic实例; 然而, 这是我们最后一次不得不这样做.

instance EBasic Comp where
  -- old
  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
  -- new
  app (Req r k) e2 = Req r (\x -> app (k x) e2)
  app e1 (Req r k) = Req r (\x -> app e1 (k x))

示例项ttinc作为Comp具有以下意义. (早先写的项在domain上是多态的, 因此其定义可以原样使用. 为了便于参考, 我们在下面重复它.)

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

*EDSLNG> ttinc :: Comp
Done (DCInt 4)

条件表达式以Comp表示的意义同样直截了当:

instance ECond Comp where
  eq = ... like inc

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

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)

参考文献

• Eugenio Moggi: Computational lambda-calculus and monads. LICS 1989.
• Mike Spivey: A functional theory of exceptions. Science of Computer Programming, v14, 1990.

第3.2节 状态, 无痛地

到目前为止, 唯一的效应一直是错误传播. 当我们添加一个真正的效应: 全局可变整数状态, 新方法的关键时刻就到来了. 我们需要再写一个EBasic实例吗? 带有其旧的指称的旧示例项ttinc :: Comp可以与新的带有效应的操作并用吗? 我们将会找到答案.

用于检索和更新当前状态的操作get和put已经在第1章中定义过了. 为了便于参考, 我们在下面重复这些定义, 以及示例项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))

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

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

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)
-- everything else
handleState s (Req r k) = Req r (handleState s . k)

示例表达式ttS在初始状态0下使用状态处理器, 即handleState 0 ttS, 具有DCInt 5的意义. {译注: 原文此处写作DInt 5, 应为笔误.}我们已经指出过处理器是递归的: 在接收到一个回复之后, 一个表达式可能发送进一步的请求, 依次被处理. 因此严格来说, 处理器所建立的数学映射是一个不动点——而我们不得不为一个不终止的处理计算隐式地引入Done bottom. 我们之前没有看到底元素 (bottom), 因为我们没有发散的计算. 顺便一提, 一个发送无尽的Get请求流的表达式并不是发散的: 其意义是能产的请求流.

因此Cartwright和Felleisen的想法确实有效! 我们添加了一个真正的效应, 而无需重写任何早先的domain和解释器. 人们可以同样无痛地引入其他种类的可变状态, 或者一般而言的其他效应. 整数字面量总是意味着整数, 并且可以在任意带有效应的表达式中被如此使用. Cartwright和Felleisen的想法甚至比作者们所描述的效果更好: 我们使得处理器本身是模块化的, 每个负责其自己的请求.

第3.3节 第一级函数, 第一次尝试

早先在第1章中, 我们试图用第一级函数扩展语言, 结果发现这需要如此深入和众多的修改, 以至于我们放弃了. 让我们在稳定指称的框架中再试一次. 我们将要做的事情在效应即交互的框架中尚未有人做过.

第1章以如下操作引入了第一级函数, 通过示例项th0演示: {译注: 实际上第1章中并没有出现示例项th0.}

type VarName = String

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

th0 = lam "x" (inc `app` var "x") -- increment (eta-expanded)

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)

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

第3.4节 第一级函数, 带有词法作用域

在稳定指称框架中赋予第一级函数意义的第一次尝试遇到了可预见的问题: 我们不经意间为绑定变量实现了动态作用域而不是词法作用域. 动态绑定是多么自然, 这真是不可思议: 它是在实现lambda演算时首先想到的. 难怪John McCarthy和Alan Turing都犯了这个错误. {译注: 原文此处写作John McCarty, 应为笔误.}词法绑定需要多得多的努力才能认识到和实现. 毕竟, 闭包 (closure) 这个术语直到1964年才由Landin引入, 此时lambda演算发表已经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)

对于词法作用域而言, 情况恰恰相反. 回忆一下, 一个词法作用域的函数在其创建之处捕获变量环境 (绑定上下文): 如Landin所言, 闭合 (close over)上下文. 因此, 构建一个闭包确实依赖于上下文, 并且根据我们的定义, 是带有效应的. 当闭包被应用时, 这个被捕获的环境被用来满足所有变量解引用请求:

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)

另一方面, 为了创建一个闭包, 我们必须向上下文询问其中绑定的所有变量. 因此, 捕获环境是一个效应. lam形式发起捕获, 发送ReqClosure v请求. 当它到达一个handleVar解释器——回忆一下, 其包含关于在其作用域内绑定的变量的完整信息——时, 解释器通过将其变量环境向下传递给函数体的处理器来创建闭包. 顶层的handleVar []传递空环境, 因为在顶层不应该有变量被绑定. 现在,

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

我们刚刚演示了即便是添加词法作用域的第一级函数也保留了早先定义的特性的指称. 增量inc仍然意味着后继, 而整数字面量仍然意味着整数, 无论它们是否出现在函数体中. 我们的指称让人想起lambda演算在pi演算中的嵌入. 我们的语义的一个或许出人意料的特点在于lam被视为一个效应. 人们不应该太过惊讶: 毕竟, 闭包创建确实不得不与上下文交互, 并且确实不得不为环境分配空间. 语言FX和ATS同样将闭包创建视为一个效应, 这并非偶然.

参考文献

• 作为变量绑定环境的栈: 通过动态绑定实现的词法绑定, 严格的和惰性的——动态绑定和词法绑定的概览和比较讨论.

第3.5节 可扩展效应

细心的读者一定已经注意到了, 我们隐式地将请求的数据类型ReqT视为好像它是可扩展的. Haskell数据类型是不可扩展的; 伴随本文的源代码不得不预先定义请求类型. 这在实践中是不可行的.

幸运的是, 通过嵌套余积 (co-product) (Either类型), 引入一个可扩展的请求类型并不需要太多痛苦. Haskell和其他语言中的可扩展效应库正是这样做的. 最终结果是真正可扩展的——而且是有类型的——框架, 其让我们的程序具有所欲的效应.

参考文献

• Extensible Effects: an alternative to Monad Transformers——特别参见论文Freer Monads, More Extensible Effects的第2.5节.

第4章 高阶编程是一个效应

我们主张, 高阶编程与各种效应的交互这一核心问题可以通过消除区分来解决: 高阶设施本身就是一个效应, 与状态效应并没有太大不同.

我们演示第一级抽象可以像任何其他效应一样被统一对待, 从而完成Cartwright和Felleisen的Extensible Denotational Language Specifications计划:

• 变量代换与解引用一个类C的变量无法区分;
• lambda, 或者说创建一个闭包, 也是一个效应.
• (词法)闭包充当在其体的执行过程中所产生的所有变量解引用效应的处理器.

与call-by-push-value以及语言ATS或者FX一样, 我们将lambda抽象视为一个带有效应的表达式. 与这些演算和语言不同, 我们也将变量视为一个带有效应的表达式. 绑定变量本质上是在第一级存储中分配的单次赋值引用单元. 这正是它们在机器码中通常被编译的方式. 因此我们的方法有望对分布式和异构系统给出忠实的描述, 其中变量解引用是一个非平凡的效应.

通常将一个带有效应的语言设计为lambda演算的扩展, 带有以下熟悉的定型判断: $$\mathrm{\Gamma }⊢M:Tea$$ 即表达式$M$具有类型$Tea$. 这里, $a$是成功求值$M$时所产生的值的类型, 而$e$描述了$M$在此过程中可能执行的效应. ($T$是二元类型构造子: 可以将其设想为一个(以效应为索引的)单子.) $\mathrm{\Gamma }$是熟悉的定型环境, 告知$M$中自由变量的类型. 我们谦逊地提议将类型判断简化为仅仅是 $$⊢M:Tea$$ 也就是说, 移除定型环境——以及作为起点的lambda演算. 那么如何判断, 比如说, $\mathtt{x}+1$的类型呢, 其中$\mathtt{x}$是一个自由变量? $\mathtt{x}$的类型从何而来? 让我们考虑$\mathtt{ask}+1$. 为了给这样的带有效应的表达式定型, 我们需要假定$\mathtt{ask}$是一个产生整数的带有效应的操作. 因此我们写: $$⊢\left(\mathtt{ask}+1\right):T\{\mathtt{ask}:\mathtt{int}\}\mathtt{int}$$ 将效应注解$\{\mathtt{ask}:\mathtt{int}\}$视为表达式内效应操作$\mathtt{ask}$的绑定: 即作为效应的定型环境. 解引用一个变量也是一个效应! 因此, 我们完全可以写 $$\begin{array}{c}⊢\left(\mathtt{x}+1\right):T\{\mathtt{x}:\mathtt{int}\}\mathtt{int}\\ ⊢\left(\mathtt{ask}+\mathtt{x}\right):T\{\mathtt{x}:\mathtt{int},\mathtt{ask}:\mathtt{int}\}\mathtt{int}\\ ⊢\lambda \mathtt{x}.\left(\mathtt{ask}+\mathtt{x}\right):T\{\mathtt{ask}:\mathtt{int}\}\left(\mathtt{int}\to \mathtt{int}\right)\\ ⊢\mathtt{handle}\left(\mathtt{ask}+\mathtt{x}\right)\mathtt{with}\mathtt{ask}\Rightarrow 10:T\{\mathtt{x}:\mathtt{int}\}\mathtt{int}\end{array}$$ 既然效应注解充当尚待处理的效应的绑定环境, 它也完全可以描述尚待绑定的变量的类型. $\mathrm{\Gamma }$确实变得多余了.

整个程序$P$应该是闭的: $$⊢P:T\{\}a$$ 它不应该有未绑定的变量——也不应该有未处理的效应.

总而言之, 一个像可扩展效应这样支持多种效应的框架因此在抽象和代换效应上不应该有任何问题——这给出了HOPE.

版本

当前版本为2017年9月.

参考文献

• HOPE-talk.pdf——在与ICFP 2017联合举办的HOPE研讨会上所作报告的幻灯片. 2017年9月3日. 英国牛津.
• edlsng.ml——OCaml版本: Cartwright-Felleisen框架的现代重构. 状态, 动态绑定, 传值调用和传名调用的词法绑定是示例效应.
• EDSLNG.hs——代码的基本上是Haskell98的版本.

第5章 结论

那么什么是效应呢? 它是与上下文的交互. 如果一个表达式向上下文发送消息, 那么它就是带有效应的. 一个词法作用域的lambda不得不向上下文询问绑定环境, 因而是带有效应的. 一个闭包的体, 在被求值时, 发送对其自由变量的值的请求. 然而, 整个闭包满足所有这样的变量请求, 并且 (在没有状态, IO等的情况下) 不需要进一步的上下文交互. 因此闭包是不带效应的, 纯的.

因此, 某样东西是否是副作用, 是一个视角的问题. 当聚焦于计算的一小部分时, 所有与上下文的交互——无论是访问外部存储器还是访问一个绑定变量——都是副作用. 甚至lambda也可以被视为一个效应, 即闭包创建的效应.

我们是否应该将Lambda或者State视为一个效应取决于手头的任务: 我们是在对一个表达式求值还是在编译它, 我们是只对表达式的结果感兴趣还是也对计算它的时间感兴趣. 因此, 效应作为一种便利和一种抽象而浮现, 让我们能够聚焦于整个系统的一部分, 将其余部分抽象为要通过固定协议与之交互的上下文. 不同的协议容许不同程度的等式推理.

这就是为什么, 当涉及效应时, 明确和有意识是如此重要.