效果系统

在计算中，效果系统是一个描述计算机程序的计算效果的正式系统，例如副作用。效果系统可以用来对程序的可能效果进行编译时的检查。效果系统扩展了类型的概念，使其具有一个效果组件，它包括一个效果种类和一个区域。效应种类描述了正在做的事情，而区域则描述了正在做的事情。一个效果系统通常是类型系统的扩展。在这种情况下，有时会使用类型和效应系统这个术语。通常，一个值的类型和它的效果一起被表示为类型！效果，其中类型部分和效果部分都提到了某些区域（例如，一个可变的存储单元的类型是由该单元所在的存储区域的标签所参数化的）。代数效应这个词是从类型系统中衍生出来的。效应系统可以用来证明某些内部不纯的定义的外部纯洁性：例如，如果一个函数在内部分配和修改了一个内存区域，但该函数的类型没有提到该区域，那么相应的效应可以从该函数的效应中抹去。

可由效应系统描述的行为的一些例子包括。读、写或分配内存：效果种类是读、写、分配或释放，区域是程序中执行分配的点（即每个执行分配的程序点都被分配一个xxx的标签，区域信息沿着数据流静态传播）。大多数处理内存的函数实际上在区域变量中是多态的：例如，一个交换内存中两个位置的函数，其类型为forallr1r2,unit!{读r1，读r2，写r1，写r2}。与资源一起工作，如文件：例如，效果种类可能是打开、读和关闭，同样，区域是程序中打开资源的点。与连续和长跳的控制转移：效果种类可能是goto（即这段代码可能执行跳转）和comefrom（即。从程序员的角度来看，效果是很有用的，因为它允许将特定动作的实现（如何）与执行何种动作的规范分开。例如，一个询问名字的效果可以从控制台读取，弹出一个窗口，或者只是返回一个默认值。控制流可以被描述为产量（即继续执行）和抛出（即未处理的效果向下传播直至处理）的混合。

核心特征Koka是一种静态类型的函数式编程语言，代数效果处理程序是其主要特征。Eff是一种静态类型的函数式编程语言，以代数效果处理程序为中心。Unison是一种静态类型的函数式编程语言，代数效果处理程序（在语言中称为能力）是类型系统的核心部分。全面支持Haskell是一种静态类型的函数式编程语言，有几个包允许对效果进行编码。然而，Haskell通常更专注于单体。部分支持和原型Scala3.1是一种静态类型的、功能性的和面向对象的编程语言，对效果的实验性支持仅限于异常，其形式是CanThrow能力。Java是一种静态类型的、面向对象的编程语言；其检查的异常是效果系统的一个相对有限的例子。只有一种效果--抛出--是可用的，没有办法用一个值来恢复，而且它们不能用于函数（只有方法），除非函数实现了一个自定义的@FunctionalInterface。JavaScript是一种动态类型的语言，它有一个实现代数效果的建议。