效应系统

形式陈述 ​

效应系统把普通类型判断扩展为

$$\mathrm{\Gamma }⊢e:A!\epsilon ,$$

表示 $e$ 返回类型 $A$ 的值，而执行它可能产生由 $\epsilon$ 近似的效应。$\epsilon$ 可以是有限集合公理库集合Set由确定成员组成的数学对象；成员关系而非表示顺序决定集合。，也可以来自带偏序 $\le$、空效应 $\varnothing$ 与合并运算 $\bigsqcup$ 的效应代数；具体系统可记录异常标签、读写区域、I/O 或控制操作，不应把某一种集合格当作唯一定义。

在一个基础的集合效应系统中，值本身可有空效应；函数类型记录调用时才发生的潜在效应：

$$\frac{\mathrm{\Gamma },x:A⊢e:B!\epsilon }{\mathrm{\Gamma }⊢\lambda x.e:A\stackrel{\epsilon }{\to }B!\varnothing }.$$

应用与顺序组合累积各子计算及函数体的效应：

$$\frac{\mathrm{\Gamma }⊢e_1:A\stackrel{{\epsilon }_f}{\to }B!{\epsilon }_1\mathrm{\Gamma }⊢e_2:A!{\epsilon }_2}{\mathrm{\Gamma }⊢e_1{e}_2:B!{\epsilon }_1\bigsqcup {\epsilon }_2\bigsqcup {\epsilon }_f}.$$

若 $\epsilon \le {\epsilon }^{\prime }$，subeffecting 允许把较精确的结论放宽为 ${\epsilon }^{\prime }$。这些是声明式规则；实际推断器可生成集合包含、行统一或区域约束并求解，但算法求出的标注必须对应规则中的可推导判断。

可靠性的典型形式是：若闭项 $e$ 被赋予 $A!\epsilon$，则其运行语义公理库操作语义Operational semantics用执行判断、转移规则或抽象机定义程序如何运行。轨迹中实际发生的效应 $\delta$ 满足 $\delta \le \epsilon$。这是上界保证，不表示每次运行都会产生 $\epsilon$ 中所有事件，也不表示效应标注保存了带次数和顺序的完整日志。

直觉 ​

结果类型回答“计算完成后交出什么”，效应标注回答“为得到结果，计算可能触碰什么”。一个返回整数的函数可能只做纯算术，也可能读文件、写数据库或抛异常；仅看 Int 无法区分这些行为。效应系统把这种差别留在静态接口中，使调用者能在不运行程序时作保守判断。

潜在效应与立即效应必须分开。创建一个函数值只封装函数体，通常不执行其中的 I/O；所以 λ 表达式自身可纯，而它的箭头类型记住将来调用时的 io。若漏掉这一层，系统要么错误地把所有函数创建都算成执行效果，要么在真正调用时丢失效果。

例子与边界 ​

设

$$\mathsf{load}:Path\stackrel{\{io,exn\}}{\to }Bytes.$$

表达式 fun p -> load p 在创建闭包时没有读文件，因而外层判断可带 $\varnothing$；所得函数类型却保留 $\{io,exn\}$。调用 load configPath 时，参数求值、函数求值与潜在效应合并，结果判断覆盖 I/O 和异常。若程序先检查缓存并只在未命中时读取文件，静态标注仍可能含 io，即使某次运行没有发生读取。

空效应也只有在系统的可靠性前提成立时才能支持“不会发生所跟踪效应”的结论。不安全外部函数若被错误声明为纯，或语义中存在未纳入效应代数的隐蔽通道，都会破坏推论。效应系统通常也不决定求值顺序：集合 $\{read,write\}$ 不说明先读后写，顺序仍由语言运行语义规定。

效应系统与代数效应处理器位于不同层面。前者静态近似程序可能触发哪些操作；后者在运行语义中规定 perform 如何被 handler 接住和恢复。语言可以同时拥有二者，也可以只拥有其中一个。

推论与应用 ​

效应标注可用于验证纯函数边界、限制异常传播、指导并行化，以及判断表达式移动或重排是否可能改变可观察行为。区域效应还能指出计算读写哪些存储区域，为别名分析和安全优化提供依据。

多态效应或 row polymorphism 允许库函数保留调用者传入函数的未知效应，而不是把它粗略放大为“任意效果”。这是基础效应判断的扩展；只有当固定效应集合造成真实复用问题时，才需要引入行变量和相应约束求解。

参考资料

• John M. Lucassen and David K. Gifford, “Polymorphic Effect Systems,” POPL, 1988。
• Jean-Pierre Talpin and Pierre Jouvelot, “The Type and Effect Discipline,” Information and Computation 111(2), 1994。
• Daan Leijen, “Koka: Programming with Row Polymorphic Effect Types,” EPTCS 153, 2014。