state-machine - 使用 Idris 对开闭门状态机建模

Question

在 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 ?

Answer 1

表示这些有限状态机的常见策略是将状态定义为枚举(这正是您的 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 内部有限状态机的同类系统。