List of Tables

Chapter 1. Overview

Table 1.1. Input and output types for matrix operations. The names x, y, and z describe, in general, how the dimensions of the inputs and outputs are related.

Table 1.2. Appending specific typed lists. Unlike simple types, where there’s no difference between the input and output list types, dependent types allow the length to be encoded in the type.

Table 1.3. Appending typed lists, in general. Type variables describe the relationships between the inputs and outputs, even though the exact inputs and outputs are unknown.

Chapter 3. Interactive development with types

Table 3.1. Interactive editing commands in Atom

Chapter 7. Interfaces: using constrained generic types

Table 7.1. Summary of numeric interfaces and their implementations

Chapter 13. State machines: verifying protocols in types

Table 13.1. Vending machine operations, with input and output states represented as Nat

Table 13.2. Stack operations, with input and output stack sizes represented as Nat

Chapter 15. Type-safe concurrent programming

Table 15.1. Value of var for each sequence of operations in figure 15.1, given an initial value of 1 for var

Appendix B. Interactive editing commands

Table 1. Interactive editing commands in Atom

Appendix C. REPL commands

Table 1. Idris REPL commands