Type-Driven Development with Idris

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