Chapter 3. Interactive development with types

 

This chapter covers

  • Defining functions by pattern matching
  • Type-driven interactive editing in Atom
  • Adding precision to function types
  • Practical programming with vectors

You’ve now seen how to define simple functions, and how to structure these into complete programs. In this chapter, we’ll start a deeper exploration into type-driven development. First, we’ll look at how to write more-complex functions with existing types from the Prelude, such as lists. Then, we’ll look at using the Idris type system to give functions more-precise types.

In type-driven development, we follow the process of “type, define, refine.” You’ll see this process in action throughout this chapter as you first write the types and, as far as possible, always have a type-correct, if perhaps incomplete, definition of a function and refine it step by step until it’s complete. Each step will be broadly characterized as one of these three:

  • Type— Either write a type to begin the process, or inspect the type of a hole to decide how to continue the process.
  • Define— Create the structure of a function definition either by creating an outline of a definition or breaking it down into smaller components.
  • Refine— Improve an existing definition either by filling in a hole or making its type more precise.

3.1. Interactive editing in Atom

3.1.1. Interactive command summary

3.1.2. Defining functions by pattern matching

3.1.3. Data types and patterns

3.2. Adding precision to types: working with vectors

3.2.1. Refining the type of allLengths

3.2.2. Type-directed search: automatic refining

3.2.3. Type, define, refine: sorting a vector

3.3. Example: type-driven development of matrix functions

3.3.1. Matrix operations and their types

3.3.2. Transposing a matrix

3.4. Implicit arguments: type-level variables

3.4.1. The need for implicit arguments

3.4.2. Bound and unbound implicits

3.4.3. Using implicit arguments in functions

3.5. Summary