types - 什么是类型和效果系统？

Question

Wikipedia article on Effect system目前只是一个短 stub ，我一直想知道什么是效果系统。

除了类型系统之外，是否还有其他语言具有效果系统？

中可能的(假设的)符号是什么？主流语言，你熟悉的，看起来像效果？

Answer 1

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

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

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

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 .弗拉纳根、弗洛因德、利普申和卡迪尔。

Enforcing High-Level Protocols in Low-Level Software .罗伯特·德莱恩和曼努埃尔·范德里奇。

Type and Effect Systems .尼尔森和尼尔森。