这是对于Oleg Kiselyov博客的翻译.
这个研究是追寻某条旖旎线索的旅程: 关于monad, monad变换器, 自由monad和可扩展作用的奠基性论文都是关于可扩展解释器的. 沿着这条道路我们意识到表达式问题, 稳定指称, 以及可扩展解释器都是相同东西的不同名字. 最终我们发现了组织性的原则: 交互——一个客户端和一个服务器之间, 一个解释器和被解释的代码之间, 一个表达式和其上下文之间.
或许交互最好使用某种进程演算进行表达. 若以顺序性演算的语言, Cartwright和Felleisen的Extensible Denotational Language Specifications
是最早的将作用当作交互进行全然处理的呈现.
实用角度来看指称语义
既然(副)作用无处不在又充满争议, 那么其理应得到研究. 并且, 显然其已被指称语义的Vienna学派于1970年代进行研究——目的在于澄清PL/1(的语义). 我们也将会使用指称语义——但是带有实用的倾向, 面向(定义性)解释器. 它最终将我们导向可扩展作用
——一种管理真实程序之中的作用的实用方法.
本章我们刻画了人尽皆知的不稳定指称问题. 它是使用指称语义研究和定义真实语言及其作用的绊脚石, 这首先是由John Reynolds于1974年注意到的. 第3章使用从进程演算那里得到的洞察解决了这个问题.
为了具体, 我们将会使用Haskell来编写我们的定义性解释器, 尽管使用OCaml, F#, Scala等语言也没有问题. 我们希望即便是不熟悉Haskell的读者也应该能够通过阅读代码并将其与标准数学记号进行类比以理解主要的想法. 毕竟当我们来到未知之地时, 即便语言和文化不通, 我们也总是会设法生存并且享受旅行. 交流的意愿才是最重要的.
我们将通过极其简单的例子来解释指称语义的定义性解释器方法. 尽管其相当平凡, 这个例子已经澄清了可扩展解释器的价值.
我们从最简单的算术表达式语言开始: 整数字面量, 增量函数, 以及让我们应用增量的应用运算符. 在Haskell之中, 我们将这个语言定义为一个数据类型Expr:
data Expr = EInt Int | EInc | EApp Expr Expr2施行增量两次——looks then as tinc {译注: 这里所说的示例表达式, 指的是具体句法}: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)
_ -> DErrorEApp EInc (EInt 8) signifies the phrase (a mere string) inc 8 in our language, DInt 9是其意义, 一个Haskell整数. eval的最后一个子句展示了复合性: EApp e1 e2的意义仅仅依赖于eval e1和eval e2: 即依赖于参数e1和e2的意义, 但是并不依赖于参数本身, 也就是并不依赖于其结构. 因此, 指称语义藉由一个结构归纳性的解释器定义, 即一个折叠 (fold).这语言急需新的特性; 例如, 布尔, 整数上的相等检测, 以及条件表达式. Alas, Haskell中的数据类型是不可扩展的. 因此, 我们不得不重新定义Expr以容纳扩展:
data Expr = EInt Int | EInc | EApp Expr Expr
| EEq | EIf Expr Expr Exprif 3 == inc (inc 2) then 10 else inc (inc (inc 2))tif below. 我们想要重用之前为inc (inc 2)定义的tinc, 但是并不可行: 类型Expr已然发生了改变. 我们不得不使用新的Expr来重新定义tinc, 尽管其看起来和之前毫无二致.tinc1 = EApp EInc (EApp EInc (EInt 2))
tif = EIf (EApp (EApp EEq (EInt 3)) tinc1) (EInt 10) (EApp EInc tinc1)eval给出了经过扩展的语言的意义. 前三个子句和旧有的解释器一模一样. Alas, 我们不能引用旧的解释器, 而不得不写一个新的出来: 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让我们回到只有整数和增量的最简单的语言上来, 然后以不同的方式定义它. 我们不再使用某个数据类型, 因为若是这样的话其又不得不被解释为Dom了. 让我们通过直接告知 (tell) 每个语言phrase的意义, 以及如何根据复合phrase的分量的意义来make sense of这个复合phrase, 来定义语言. 因此, 我们即刻引入了指称语义而不需要中间的步骤eval. {译注: 这两句话需要结合后文 (特别是程序) 进行理解. 当前的意义其实并非具体的语义, 而只是语义的大致框架/形状.} 为了一般性 (这在之后会派上用场), 我们并没有固定指称的论域为Dom. 转而, 我们将其作成了变量d. 总而言之, 我们藉由一集定义来定义了一个语言, 每个句法形式都对应于一个定义, 而这每个定义都定义了相应形式的论域映射. {译注: 虽然这里有一些绕, 但其实就是之前说的, 根据分量的意义来得到复合的意义.} 论域是保持抽象的. 因此, 我们将语言定义为Haskell中的类型类 (或者OCaml中的模块类型, 诸如此类):
class EBasic d where
int :: Int -> d
inc :: d
app :: d -> d -> d
infixl 1 `app` -- make the infix `app` left-associativeapp. 复合之意义是由子表达式之意义d所确定的. 根据这个设计, 语义的确是复合性的. 示例项inc (inc 2)现在具有以下形式:ttinc = inc `app` (inc `app` int 2)ttinc :: EBasic d => d. 我们或许可以将其读作: ttinc是EBasic语言之中的项, 或者说给定一个合适的论域——对于我们的语言足够有表达力——ttinc给出了phrase inc (inc 2)在这个论域之中的意义. {译注: 仅仅有论域并不足够, 实际上还需要解释.} 剩下来我们所要做的事情是表明Dom的确适合于给出这个基本语言的意义:
instance EBasic Dom where
int = DInt
inc = injI succ
app (DFun f) e2 = f e2
app _ _ = DErrorinjI succ以将Haskell的后继函数提升至Dom, 若增量的值并非一个DInt则其会返回DError. 然后, 示例表达式的意义就是ttinc :: Dom了, 也就是说, ttinc被特化于论域类型Dom之上.和之前一样的是, 我们将一个表达式映射为了其意义, 即Dom的元素.
这一节给增量和条件式的语言添加了第一个真实的作用: 全局的可变的整数状态.