Chapter 12. Writing programs with state
This chapter covers
- Using the State type to describe mutable state
- Implementing custom types for state management
- Defining and using records for global system state
Idris is a pure language, so variables are immutable. Once a variable is defined with a value, nothing can update it. This might suggest that writing programs that manipulate state is difficult, or even impossible, or that Idris programmers in general aren’t interested in state. In practice, the opposite is true.
In type-driven development, a function’s type tells you exactly what a function can do in terms of its allowed inputs and outputs. So, if you want to write a function that manipulates state, you can do that, but you need to be explicit about it in the function’s type. In fact, we’ve already done this in earlier chapters:
- In chapter 4, we implemented an interactive data store using global state.
- In chapter 9, we implemented a word-guessing game using global state to hold the target word, the letters guessed, and the number of guesses still available.
- In chapter 11, we implemented an arithmetic game using global state to hold the user’s current score.