什么是类型和效果系统？

Question

这 维基百科文章关于 效果系统 目前只是一个简短的存根，我有一段时间想知道什么是效果系统。

• 除了类型系统之外，是否还有其他语言还具有效果系统？
• 可能的（假设的）符号是什么 主流 您熟悉的语言、外观和效果吗？

Answer 1

“类型和效果系统”不仅描述了程序中值的种类，还描述了这些值的变化。“Typestate”检查是一个相关的想法。

一个示例可能是跟踪文件句柄的类型系统：而不是有一个函数 close 带返回类型 void, ，类型系统会记录 影响 的 close 作为文件资源的处置——调用后任何读取或写入文件的尝试 close 将成为类型错误。

我不知道主流编程语言中出现过任何类型和效果系统。它们已用于定义静态分析（例如，根据效果定义正确锁定/解锁的分析是很自然的）。因此，效果系统通常是使用推理方案而不是具体语法来定义的。你可以想象语法看起来像

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

如果您想了解更多信息，以下论文可能会很有趣（公平警告：这些论文非常理论化）。

• 原子性的类型：Java 的静态检查和推理. 。弗拉纳根、弗洛因德、利普辛和卡德尔。
• 在低级软件中实施高级协议. 。罗伯特·德莱恩和曼努埃尔·范德里奇。
• 类型和效果系统. 。尼尔森和尼尔森。

Answer 2

（这不是权威答案；只是想搜寻我的记忆。）

从某种意义上说，任何时候你用一种语言编写“状态单子”，你都在使用类型系统作为潜在的效果系统。因此，Haskell 中的“状态”或“IO”捕获了这个概念（IO 也捕获了很多其他效果）。我依稀记得读过有关使用高级类型系统的各种语言的论文，包括“依赖类型”之类的东西来控制效果的更细粒度管理，例如，类型/效果系统可以捕获有关哪些内存位置将在给定的数据类型。这很有用，因为它提供了使两个修改互斥状态位的函数允许“通勤”的方法（monad 通常不会通勤，并且不同的 monad 并不总是能够很好地相互组合，这通常使得很难打字（阅读：为“合理”程序分配静态类型）...

打个比方 非常 hand-wavy level 是 Java 检查异常的方式。您在类型系统中表达了有关某些效果的额外信息（出于类比的目的，您可以将异常视为“效果”），但这些“效果”通常会泄漏到整个程序中，并且不能很好地组合在一起实践（您最终会得到一百万个“抛出”子句，或者诉诸许多未经检查的运行时异常类型）。

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

Answer 3

你可以看看 http://www.haskell.org/haskellwiki/DDC

它是 Haskell 实现效果系统的一个版本。