Chapter 11. Streams and processes: working with infinite data

 

This chapter covers

  • Generating and processing streams of data
  • Distinguishing terminating from productive total functions
  • Defining total interactive processes using infinite streams

The functions we’ve written in this book so far have worked in batch mode, processing all of their inputs and then returning an output. In the previous chapter, we also spent some time discussing why termination is important, and you learned how to use views to help you write programs that are guaranteed to terminate.

But input data doesn’t always arrive in a batch, and you’ll often want to write programs that don’t terminate, running indefinitely. For example, it can be convenient to think of input data to an interactive program (such as keypresses, mouse movements, and so on) as a continuous stream of data, processed one element at a time, leading to a stream of output data. In reality, many programs are, in effect, stream processors:

  • A read-eval-print loop, such as the Idris environment, processes a potentially infinite stream of user commands, giving an output stream of responses.
  • A web server processes a potentially infinite stream of HTTP requests, giving an output stream of responses to be sent over the network.
  • A real-time game processes a potentially infinite stream of commands from a controller, giving an output stream of audiovisual actions.

11.1. Streams: generating and processing infinite lists

11.1.1. Labeling elements in a List

11.1.2. Producing an infinite list of numbers

11.1.3. Digression: what does it mean for a function to be total?

11.1.4. Processing infinite lists

11.1.5. The Stream data type

11.1.6. An arithmetic quiz using streams of random numbers

11.2. Infinite processes: writing interactive total programs

11.2.1. Describing infinite processes

11.2.2. Executing infinite processes

11.2.3. Executing infinite processes as total functions

11.2.4. Generating infinite structures using Lazy types

11.2.5. Extending do notation for InfIO

11.2.6. A total arithmetic quiz

11.3. Interactive programs with termination

11.3.1. Refining InfIO: introducing termination

11.3.2. Domain-specific commands

11.3.3. Sequencing Commands with do notation

11.4. Summary