利用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数据类型,但我认为(从听到这个话题)可以在没有类型安全的情况下对这个FSM进行编码Either/Maybe.

什么是惯用的,Idris方式使用路径依赖类型编写上述函数,而不使用Maybe/Either？

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

在埃德温的讲话的情况比较复杂:门上的行动被视为副作用,打开门可能会失败(因此它也不一定是真的,我们有Open : DoorAction DClosed DOpen),但核心思想是相同的.

你可能想要看一篇有趣的文章是McBride的Kleisli箭头,这是一个令人发指的财富.在其中,他正在处理在Haskell中配备内部有限状态机的同类系统.