Using Idris to Model State Machine of Open-Close Door

Question

At ScalaWorld 2015, Edwin Brady gave an exciting talk on Idris - https://www.youtube.com/watch?v=X36ye-1x_HQ.

In one of the examples, I recall that he showed how to use Idris to write a program representing a Finite State Machine (FSM) - for opening and closing a door. His FSM may be a bit more complex, but, given the following states:

data DoorState = DOpen | DClosed

data DoorAction = Open | Close

I wrote a function that, given a DoorAction and DoorState, returns the new DoorState.

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

But, the above function is partial, example: runDoorOp Open DOpen would crash.

I thought of using an Either or Maybe data type, but I think (from hearing that talk) that it's possible to encode this FSM in a type-safe way without Either/Maybe.

What's the idiomatic, Idris way to write the above function using path-dependent types, not using Maybe/Either?

Answer 1

A common strategy to represent these finite state machines is to define the states as an enumeration (which is precisely what your DoorState does!)

data DoorState = DOpen | DClosed

And then describe the valid transitions by defining a relation (think: DoorAction a b means that from a I'm allowed to go to b). As you can see the indices of the constructor Open are enforcing that you may only open a door if it's currently Dclosed and it'll become DOpen.

data DoorAction : DoorState -> DoorState -> Type where
  Open  : DoorAction DClosed DOpen
  Close : DoorAction DOpen   DClosed

From there on you can describe well-formed sequences of interactions with a door by making sure that whenever you try to apply an action, it is allowed by the state the system is in:

data Interaction : DoorState -> DoorState -> Type where
  Nil  : Interaction a a
  Cons : DoorAction a b -> Interaction b c -> Interaction a c

In Edwin's talk the situation is more complex: the actions on the door are seen as side effects, opening the door may fail (and so it's not necessarily true that we have Open : DoorAction DClosed DOpen) but the core ideas are the same.

An interesting article you may want to have a look at is McBride's Kleisli arrows of outrageous fortune. In it, he is dealing with the same sort of systems equipped with an internal finite state machine in Haskell.