List of Figures

 

Chapter 1. Overview

Figure 1.1. The top of a shape-sorter toy. The shapes correspond to the types of objects that will fit through the holes.

Figure 1.2. The states and valid operations on an ATM. Each operation is valid only in specific states and can change the state of the machine. CheckPIN changes the state only if the entered PIN is correct.

Figure 1.3. Two interacting concurrent processes, main and adder. The main process sends a request to adder, which then sends a response back to main.

Figure 1.4. A pure function, taking inputs and producing outputs with no observable side effects

Figure 1.5. Pure functions, in general, take only inputs and have no observable side effects.

Figure 1.6. A side-effecting program, reading inputs from a file, printing the result, and returning the result

Chapter 2. Getting started with Idris

Figure 2.1. The components of a function definition

Figure 2.2. A local variable definition: in the expression after the in keyword, x has the value 50.

Chapter 3. Interactive development with types

Figure 3.1. Matching the pattern (x :: xs) for inputs [1] and [2,3,4,5]

Figure 3.2. Calculating the lengths of words in a list. Notice that each input has a corresponding output, so the length of the output vector is always the same as the length of the input vector.

Figure 3.3. Representation of a matrix as two-dimensional vectors. On the left, the matrix is in mathematical notation. The same matrix is represented in Idris on the right.