TypeState 在语言设计方面指的是什么?我在一些关于 mozilla 的新语言 Rust 的讨论中看到了它。
3 回答
注意: Typestate 从 Rust 中删除,只剩下一个有限的版本(跟踪未初始化和从变量中移动)。最后看我的笔记。
TypeState背后的动机是类型是不可变的,但是它们的一些属性是动态的,基于每个变量。
因此,我们的想法是创建关于类型的简单谓词,并使用编译器出于许多其他原因执行的控制流分析来用这些谓词静态修饰类型。
这些谓词实际上并没有由编译器本身检查,它可能过于繁琐,编译器只会根据图形进行推理。
作为一个简单的示例,您创建一个 predicate even
,true
如果一个数字是偶数则返回。
现在,您创建两个函数:
halve
,它只作用于even
数字double
,它接受任何数字,并返回一个even
数字。
请注意,类型number
不会更改,您不会创建evennumber
类型并复制之前执行的所有功能number
。您只需number
使用名为even
.
现在,让我们构建一些图表:
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`
\___________________________________/
这表明您根据谓词集进行推理:
- 当连接两条路径时,新的谓词集是这两条路径给出的谓词集的交集
这可以通过函数的通用规则来增强:
- 要调用函数,必须满足它所需的谓词集
- 调用函数后,仅满足它建立的谓词集(注意:按值获取的参数不受影响)
因此, Rust中TypeState的构建块:
check
:检查谓词是否成立,如果不成立,则将fail
谓词添加到谓词集中
请注意,由于Rust要求谓词是纯函数,因此check
如果它可以证明谓词在这一点上已经成立,它可以消除冗余调用。
Typestate 缺乏的东西很简单:可组合性。
如果你仔细阅读描述,你会注意到:
- 调用函数后,仅满足它建立的谓词集(注意:按值获取的参数不受影响)
这意味着类型的谓词本身是无用的,实用程序来自注释函数。因此,在现有代码库中引入新谓词是很无聊的,因为需要审查和调整现有函数以解释它们是否需要/保留不变量。
当新的谓词弹出时,这可能会导致函数以指数速度重复:不幸的是,谓词不是可组合的。他们本来要解决的设计问题(类型的增加,因此功能的增加)似乎没有得到解决。
它基本上是类型的扩展,您不仅要检查一般情况下是否允许某些操作,还要检查特定上下文中的操作。所有这些都在编译时。
原始论文实际上是非常可读的。
有一个为 Java 编写的类型状态检查器,Adam Warski 的解释页面提供了一些有用的信息。我只是自己弄清楚这些材料,但是如果您熟悉 Haskell 的 QuickCheck,那么 QuickCheck 对一元状态的应用似乎是相似的:对状态进行分类并解释当它们通过接口发生突变时它们如何变化。