使用 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，returns 新的 DoorState.

runDoorOp : DoorAction -> DoorState -> DoorState
runDoorOp Close DOpen  = DClosed
runDoorOp Open DClosed = DOpen

但是，上面的功能是部分的，例如：runDoorOp Open DOpen会崩溃。

我想过使用 Either 或 Maybe 数据类型，但我认为（从听到那个谈话）可以在没有 [=18 的情况下以类型安全的方式编码这个 FSM =].

使用路径相关类型而不是使用 Maybe/Either 来编写上述函数的惯用 Idris 方法是什么？

Answer 1

表示这些有限状态机的常用策略是将状态定义为枚举（这正是您的 DoorState 所做的！）

data DoorState = DOpen | DClosed

然后通过定义一个关系来描述有效的转换（想想：DoorAction a b 意味着我可以从 a 转到 b）。如您所见，构造函数 Open 的 indices 强制要求您只能打开当前为 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 的演讲中，情况更复杂：门上的动作被视为副作用，开门可能会失败（因此我们不一定有 Open : DoorAction DClosed DOpen）但核心思想都一样。

McBride 的 Kleisli arrows of outrageous fortune 是您可能想看的一篇有趣的文章。在其中，他正在处理在 Haskell.

中配备内部有限状态机的同类系统

Using Idris to Model State Machine of Open-Close Door