Chapter 1. Overview


This chapter covers

  • Introducing type-driven development
  • The essence of pure functional programming
  • First steps with Idris

This book teaches a new approach to building robust software, type-driven development, using the Idris programming language. Traditionally, types are seen as a tool for checking for errors, with the programmer writing a complete program first and using either the compiler or the runtime system to detect type errors. In type-driven development, we use types as a tool for constructing programs. We put the type first, treating it as a plan for a program, and use the compiler and type checker as our assistant, guiding us to a complete and working program that satisfies the type. The more expressive the type is that we give up front, the more confidence we can have that the resulting program will be correct.

Types and tests

The name “type-driven development” suggests an analogy to test-driven development. There’s a similarity, in that writing tests first helps establish a program’s purpose and whether it satisfies some basic requirements. The difference is that, unlike tests, which can usually only be used to show the presence of errors, types (used appropriately) can show the absence of errors. But although types reduce the need for tests, they rarely eliminate it entirely.

1.1. What is a type?

1.2. Introducing type-driven development

1.2.1. Matrix arithmetic

1.2.2. An automated teller machine

1.2.3. Concurrent programming

1.2.4. Type, define, refine: the process of type-driven development

1.2.5. Dependent types

1.3. Pure functional programming

1.3.1. Purity and referential transparency

1.3.2. Side-effecting programs

1.3.3. Partial and total functions

1.4. A quick tour of Idris

1.4.1. The interactive environment

1.4.2. Checking types

1.4.3. Compiling and running Idris programs

1.4.4. Incomplete definitions: working with holes

1.4.5. First-class types

1.5. Summary