Chapter 13. State machines: verifying protocols in types
This chapter covers
- Specifying protocols in types
- Describing preconditions and postconditions of operations
- Using dependent types in state
In the previous chapter, you saw how to manage mutable state by defining a type for representing sequences of commands in a system, and a function for running those commands. This follows a common pattern: the data type describes a sequence of operations, and the function interprets that sequence in a particular context. For example, State describes sequences of stateful operations, and runState interprets those operations with a specific initial state.
In this chapter, we’ll look at one of the advantages of using a type for describing sequences of operations and keeping the execution function separate. It allows you to make the descriptions more precise, so that certain operations can only be run when the state has a specific form. For example, some operations require access to a resource, such as a file handle or database connection, before they’re executed: