Type-Driven Development with Idris

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