什么是类型和效果系统？

Question

维基百科上的效应系统文章目前只是一个简短的存根，我一直在想什么是效应系统。

• 是否有任何同时具有类型系统和效应系统的语言？
• 对于你熟悉的主流语言，一个可能的（假设性）符号表示会是什么样子？

- marxidad

---

你可以看一下 http://www.haskell.org/haskellwiki/DDC 这是实现了效果系统的Haskell版本。 - skyde

Answer 1

"类型和效应系统"不仅描述程序中的值种类，还描述这些值的变化。 "类型状态(typestate)"检查是一个相关的概念。

一个例子可能是跟踪文件句柄的类型系统: 而不是拥有一个返回类型为void的函数close，该类型系统会记录close的"效应"，即释放文件资源 - 调用close后尝试从文件读取或写入任何数据将会成为类型错误。

我不知道任何主流编程语言中出现过的类型和效应系统。它们已被用于定义静态分析(例如，可以自然地定义proper locking/unlocking(正确的锁定/解锁)分析来描述效应)。因此，效应系统通常使用推理方案而不是具体语法来定义。你可以想象一种看起来像这样的语法：

File open(String name) [+File]; // open creates a new file handle
void close(File f)     [-f]   ; // close destroys f 

如果您想了解更多，以下论文可能会很有趣（警告：这些论文相当理论）。

• Types for Atomicity: Static Checking and Inference for Java. Flanagan, Freund, Lipshin, 和 Qadeer。
• Enforcing High-Level Protocols in Low-Level Software. Robert DeLine 和 Manuel Fändrich。
• Type and Effect Systems. Nielson 和 Nielson。

- Chris Conway

Answer 2

（这不是权威的答案；只是尝试回忆一下。）

从某种意义上说，任何时候你在编写语言中的“状态单子”，你都在使用类型系统作为潜在的效果系统。因此，Haskell中的“State”或“IO”捕获了这个概念（IO还捕获了许多其他效果）。我模糊地记得读过有关使用高级类型系统（包括依赖类型）来控制更细粒度的效果管理的各种语言的论文，以便例如类型/效果系统可以捕获有关在给定数据类型中将修改哪些内存位置的信息。这很有用，因为它提供了使两个修改互斥状态位的函数被允许“交换”的方式（单子通常不交换，并且不同的单子不总是与彼此良好地组合，这通常使得对“合理”程序进行类型（即：分配静态类型）很困难）……

一个非常手摇的类比是Java具有检查异常。您在类型系统中表达有关某些效果的额外信息（您可以将异常视为类比的“效果”），但是这些“效果”通常在整个程序中泄漏，并且在实践中无法组合（您最终会有数百个“throws”子句，否则就会使用大量未经检查的运行时异常类型）。

我认为在这个领域正在进行很多研究，无论是针对研究型还是主流型语言，注释函数的效果信息的能力可以释放编译器进行许多优化的能力，可以影响并发性，并且可以为各种程序分析和工具做出巨大贡献。但是，我个人不抱有太高的希望，因为我认为很多聪明的人已经在这方面工作了很长时间，但仍然没有什么实质性的成果。

- Brian