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.

In each case, we implemented state by writing a recursive function that took the current state of the overall program as an argument.

12.1. Working with mutable state

12.1.1. The tree-traversal example

12.1.2. Representing mutable state using a pair

12.1.3. State, a type for describing stateful operations

12.1.4. Tree traversal with State

12.2. A custom implementation of State

12.2.1. Defining State and runState

12.2.2. Defining Functor, Applicative, and Monad implementations for State

12.3. A complete program with state: working with records

12.3.1. Interactive programs with state: the arithmetic quiz revisited

12.3.2. Complex state: defining nested records

12.3.3. Updating record field values

12.3.4. Updating record fields by applying functions

12.3.5. Implementing the quiz

12.3.6. Running interactive and stateful programs: executing the quiz

12.4. Summary