Part 3. Idris and the real world

In part 2, you gained experience in developing programs interactively, guided by types, and you learned about all of the core features of Idris. Now, it’s time to apply what you’ve learned to some more practical examples.

First, in chapter 11, you’ll learn about writing programs that deal with potentially infinite structures such as streams. You’ve learned about the importance of writing total functions, but in chapter 11 you’ll see that totality is about more than termination. A function is also total if it produces some portion of a potentially infinite result, which means you can write interactive systems such as servers and read-eval-print loops that run forever, but which are nevertheless total.

Chapters 12–14 deal with state. Real-world programs usually need to deal with global state somehow, and you’ll see both how to represent state and how to describe properties of state in such a way that you can guarantee that programs follow protocols accurately. If you’re implementing a system with important security properties, such as an ATM for a bank, you can use type-driven development to ensure that those properties are satisfied.