在 ScalaWorld 2015 上,Edwin Brady 发表了关于 Idris 的精彩演讲 - https://www.youtube.com/watch?v=X36ye-1x_HQ .
在其中一个示例中,我记得他展示了如何使用 Idris 编写一个表示有限状态机 (FSM) 的程序 - 用于打开和关闭门。他的
FSM 可能有点复杂,但是,鉴于以下状态:
data DoorState = DOpen | DClosed
data DoorAction = Open | Close
我写了一个函数,给出一个
DoorAction
和 DoorState
, 返回新的 DoorState
.runDoorOp : DoorAction -> DoorState -> DoorState
runDoorOp Close DOpen = DClosed
runDoorOp Open DClosed = DOpen
但是,上面的函数是局部的,例如:
runDoorOp Open DOpen
会崩溃。我想过使用
Either
或 Maybe
数据类型,但我认为(从听那个谈话中)可以在没有 Either/Maybe
的情况下以类型安全的方式对这个 FSM 进行编码。 .使用依赖于路径的类型而不是使用
Maybe/Either
编写上述函数的惯用方法是什么 Idris ?
最佳答案
表示这些有限状态机的常见策略是将状态定义为枚举(这正是您的 DoorState
所做的!)
data DoorState = DOpen | DClosed
然后通过定义一个关系来描述有效的转换(想想:
DoorAction a b
意味着从 a
我被允许去 b
)。如您所见,构造函数的索引 Open
正在强制您只能打开当前 Dclosed
的门它会变成 DOpen
.data DoorAction : DoorState -> DoorState -> Type where
Open : DoorAction DClosed DOpen
Close : DoorAction DOpen DClosed
从那时起,您可以通过确保每当您尝试应用某个操作时,系统所处的状态都允许它来描述与门交互的结构良好的序列:
data Interaction : DoorState -> DoorState -> Type where
Nil : Interaction a a
Cons : DoorAction a b -> Interaction b c -> Interaction a c
在 Edwin 的演讲中,情况更为复杂:门上的 Action 被视为副作用,开门可能会失败(因此我们有
Open : DoorAction DClosed DOpen
不一定正确)但核心思想是相同的。您可能想看的一篇有趣的文章是 McBride 的 Kleisli arrows of outrageous fortune .在其中,他正在处理配备 Haskell 内部有限状态机的同类系统。
关于state-machine - 使用 Idris 对开闭门状态机建模,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/33851598/