【问题标题】:What is a type and effect system?什么是类型和效果系统?
【发布时间】:2025-04-30 12:40:02
【问题描述】:

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

  • 除了类型系统之外,还有没有效果系统的语言?
  • 在您熟悉的主流语言中,什么样的可能(假设)表示法看起来像带有效果?

【问题讨论】:

标签: types effects type-systems type-theory effect-systems


【解决方案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 

如果您想了解更多信息,以下论文可能会很有趣(公平警告:这些论文非常理论化)。

【讨论】:

    【解决方案2】:

    (这不是一个权威的答案;只是想搜索一下我的记忆。)

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

    在一个非常手摇级别的类比是Java如何检查异常。您在类型系统中表达了有关某些效果的额外信息(出于类比的目的,您可以将异常视为“效果”),但这些“效果”通常会泄漏到您的程序中并且不能很好地组合练习(你最终会得到一百万个“抛出”子句,或者诉诸许多未经检查的运行时异常类型)。

    我认为在这一领域正在进行大量研究,无论是针对研究型语言还是主流型语言,因为使用效果信息注释函数的能力可以解锁编译器进行许多优化的能力,可以影响并发性,并且可以为各种程序分析和工具做很多事情。不过,我个人对它短期内并没有寄予厚望,因为我认为很多聪明人已经在这方面工作了很长时间,但仍然没有什么可展示的。

    【讨论】:

      最近更新 更多