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.

5.1. Interactive programming with IO

 
 

5.1.1. Evaluating and executing interactive programs

 

5.1.2. Actions and sequencing: the >>= operator

 
 
 
 

5.1.3. Syntactic sugar for sequencing with do notation

 

5.2. Interactive programs and control flow

 

5.2.1. Producing pure values in interactive definitions

 
 
 

5.2.2. Pattern-matching bindings

 
 

5.2.3. Writing interactive definitions with loops

 
 

5.3. Reading and validating dependent types

 
 
 
 

5.3.1. Reading a Vect from the console

 
 

5.3.2. Reading a Vect of unknown length

 
 
 

5.3.3. Dependent pairs

 
 
 

5.3.4. Validating Vect lengths

 

5.4. Summary

 
 
sitemap

Unable to load book!

The book could not be loaded.

(try again in a couple of minutes)

manning.com homepage
test yourself with a liveTest