Chapter 4. User-defined data types

Type-driven development involves not only giving precise types to functions, as you’ve seen so far, but also thinking about exactly how data is structured. In a sense, programming (pure functional programming, in particular) is about transforming data from one form to another. Types allow us to describe the form of that data, and the more precise we make these descriptions, the more guidance the language can give in implementing transformations on that data.

Several useful data types are distributed as part of the Idris libraries, many of which we’ve used so far, such as List, Bool, and Vect. Other than being defined directly in Idris, there’s nothing special about these data types. In any realistic program, you’ll need to define your own data types to capture the specific requirements of the problem you’re solving and the specific forms of data you’re working with. Not only that, but there’s a significant payoff to thinking carefully about the design of data types: the more precisely types capture the requirements of a problem, the more benefit you’ll get from interactive type-directed editing.

4.1. Defining data types

4.1.1. Enumerations

4.1.2. Union types

4.1.3. Recursive types

4.1.4. Generic data types

4.2. Defining dependent data types

4.2.1. A first example: classifying vehicles by power source

4.2.2. Defining vectors

4.2.3. Indexing vectors with bounded numbers using Fin

4.3. Type-driven implementation of an interactive data store

4.3.1. Representing the store

4.3.2. Interactively maintaining state in main

4.3.3. Commands: parsing user input

4.3.4. Processing commands

4.4. Summary