Type-Driven Development with Idris

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 ...