Finite-state machines? Your compiler wants in!

When modeling problem domains, we collect different possible states, legal transitions between states, and relevant data for each state. Finite-state machines emerge. To verify that programs are constructed correctly, and to have a living machine-verified documentation, we should let the compiler in on our trade secrets.

In this talk we will look at motivations and examples of encoding finite-state machines, using the expressive type systems of Haskell and PureScript.

Talk objectives

• Show common ways of handling state, using examples from real-world projects.
• Motivate type-checking of state machines as a valuable tool for the working programmer.
• Show techniques of gradually increasing complexity, weighing some of the trade-offs, and showing how far the safety goes.

Target audience

While this talk is aimed at showing the benefits of encoding state machines in type systems, the examples use advanced type system features to accomplish that goal. Being comfortable with monads, monad transformers, type classes, and associated types, as well as Haskell or PureScript syntax, will definitely help in following along.

If you are interested in absorbing the rich harmony of state machines and type systems intertwined, and you are not afraid of the occasional compile-time error, then this talk is for you.