什么是typestate?

注: Typestate已从Rust中删除,只剩下有限的版本(跟踪未初始化的和从变量中移动的)。请看我最后的便条。

背后的动机 类型状态

因此,我们的想法是创建简单的

这些谓词实际上并不是由编译器本身检查的,它可能过于繁重,相反,编译器只会根据图形进行推理。

even true 如果一个数是偶数。

• halve ,它只作用于
• double ,它接受任意数字,并返回 即使 号码。

请注意,类型 number 如果不更改,则不创建 evennumber 键入并复制以前执行的所有函数 . 你只要作曲 用一个叫做 即使

现在,让我们构建一些图表:

a: number -> halve(a)  #! error: `a` is not `even`

a: number, even -> halve(a)  # ok

a: number -> b = double(a) -> b: number, even

当然,当你有几种可能的路径时,情况会变得更复杂一些:

a: number -> a = double(a) -> a: number, even -> halve(a) #! error: `a` is not `even`
          \___________________________________/

这表明您可以根据谓词集进行推理:

• 当连接两条路径时,新的谓词集是这两条路径给定的谓词集的交集

这可以通过函数的一般规则来补充:

• 要调用函数,必须满足它所需的谓词集
• 调用函数后,只满足它所建立的谓词集(注意:按值获取的参数不受影响)

因此是 类型状态 在里面 铁锈 :

• check :检查谓词是否成立(如果不成立) fail

注意,自从 铁锈 检查

Typestate缺少的很简单:可组合性。

这意味着类型的谓词本身是无用的,实用程序来自注释函数。因此,在现有的代码库中引入一个新的谓词是一件令人厌烦的事情,因为需要对现有函数进行检查和调整,以解释它们是否需要/保留不变量。

它基本上是类型的一个扩展,在这里,您不仅仅检查某些操作是否在一般情况下被允许,而是在这个特定的上下文中。所有这些都是在编译时完成的。

这个 original paper 实际上相当可读。

有一个为Java编写的typestate检查器 Adam Warski's explanatory page