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 ...
Get Type-Driven Development with Idris now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
