什么是types状态?

TypeState在语言devise方面提到什么? 我在一些讨论中看到了Mozilla提到的一个叫做Rust的新语言。

注意: Typestate是从Rust中删除的,只剩下一个有限的版本(跟踪未初始化并从variables中移出)。 看到我的笔记在最后。

TypeState背后的动机是types是不可变的,但是它们的一些属性是dynamic的,每个variables都是不变的。

因此,这个想法是创build一个关于types的简单谓词 ,并使用Control-Flow分析,编译器执行其他许多原因来静态修饰这些谓词的types。

这些谓词实际上并没有被编译器本身检查,它可能太繁重,而编译器会简单地以图表为理由。

作为一个简单的例子,你even可以创build一个谓词,如果一个数是偶数,则返回true

现在,你创build两个函数:

  • halve ,只对even起作用
  • double ,取任何数字,并返回一个even

请注意,typesnumber不会更改,您不会创build一个evennumbertypes并复制所有以前在number上作用的函数。 你只是用一个称为even的谓词来编写number

现在,我们来构build一些图表:

 a: number -> halve(a) #! error: `a` is not `even` a: number, even -> halve(a) # ok a: number -> b = double(a) -> b: number, even 

简单,不是吗?

当然,如果你有几个可能的path,它会变得更复杂一些:

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

这表明你用一系列的谓词来推理:

  • 当连接两条path时,新的谓词集是这两条path给出的谓词集合的交集

这可以通过函数的通用规则来增强:

  • 要调用一个函数,必须满足它所需的一组谓词
  • 在调用一个函数之后,只有它所build立的谓词集被满足(注意:由值所取的参数不受影响)

因此, TypeStateRust中的构build块:

  • check :检查谓词是否成立,如果没有fail ,则将谓词添加到谓词集合中

请注意,由于Rust要求谓词是纯函数,因此如果它能certificate谓词已经成立,则可以消除多余的check调用。


Typestate缺乏的是简单的:可组合性。

如果仔细阅读说明,您会注意到这一点:

  • 在调用一个函数之后,只有它所build立的谓词集被满足(注意:由值所取的参数不受影响)

这意味着一个types的谓词本身是无用的,这个效用来自于注释函数。 因此,在现有的代码库中引入一个新的谓词是一件很麻烦的事情,因为现有的函数需要审查和调整,以便解释他们是否需要/保留不variables。

当新的谓词popup时,这可能导致以指数速度复制函数:不幸的是,谓词不可组合。 他们要解决的devise问题(types的扩散,因此function)似乎没有得到解决。

它基本上是types的扩展,你不只是检查是否允许一些操作,而是在这个特定的上下文中。 所有在编译时。

原文实际上很可读。

有一个为Java编写的types状态检查器, Adam Warski的解释性页面提供了一些有用的信息。 我只是简单地把这些材料自己搞清楚,但是如果你熟悉Haskell的QuickCheck,QuickCheck对monadic状态的应用看起来很相似:对状态进行分类并解释当它们通过接口发生变化时它们是如何改变的。