Chapter 5. Interactive programs: input and output processing
This chapter covers
- Writing interactive console programs
- Distinguishing evaluation and execution
- Validating user inputs to dependently typed functions
Idris is a pure language, meaning that functions don’t have side effects, such as updating global variables, throwing exceptions, or performing console input or output. Realistically, though, when we put functions together to make complete programs, we’ll need to interact with users somehow.
In the preceding chapters, we used the repl and replWith functions to write simple, looping interactive programs that we can compile and execute without worrying too much about how they work. For all but the simplest programs, however, this approach is very limiting. In this chapter, you’ll see how interactive programs work in Idris more generally. You’ll see how to process and validate user input, and how you can write interactive programs that work with dependent types.
The key idea that allows us to write interactive programs in Idris, despite it being a pure language, is that we distinguish between evaluation and execution. We write interactive programs using a generic type IO, which describes sequences of actions that are then executed by the Idris runtime system.