Chapter 15. Type-safe concurrent programming

In Idris, a value of type IO () describes a sequence of actions for interacting with the user and operating system, which the runtime system executes sequentially. That is, it only executes one action at a time. You can refer to a sequence of interactive actions as a process.

As well as executing actions in sequence in a single process, it’s often useful to be able to execute multiple processes at the same time, concurrently, and to allow those processes to communicate with each other. In this chapter, I’ll introduce concurrent programming in Idris.

Message passing

Concurrent programming is a large topic, and there are several approaches to it that would fill books of their own. We’ll look at some small examples of message-passing concurrency, where processes interact by sending messages to each other. Message passing is supported as a primitive by the Idris runtime system. In effect, sending a message to a process and receiving a reply corresponds to calling a method that returns a result in an object-oriented language.

Concurrent programming has several advantages:

15.1. Primitives for concurrent programming in Idris

15.1.1. Defining concurrent processes

15.1.2. The Channels library: primitive message passing

15.1.3. Problems with channels: type errors and blocking

15.2. Defining a type for safe message passing

15.2.1. Describing message-passing processes in a type

15.2.2. Making processes total using Inf

15.2.3. Guaranteeing responses using a state machine and Inf

15.2.4. Generic message-passing processes

15.2.5. Defining a module for Process

15.2.6. Example 1: List processing

15.2.7. Example 2: A word-counting process

15.3. Summary