Type-Driven Development with Idris

Chapter 15. Type-safe concurrent programming

This chapter covers

• Using concurrency primitives
• Defining a type for describing concurrent processes
• Using types to ensure concurrent processes communicate consistently

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