Type-Driven Development with Idris

Edwin Brady

• Publisher: Manning Publications
• Year: 2017
• ISBN:
  9781617293023
• Topic: Informatique
• Subtopic: Développement de logiciels

Type-Driven Development with Idris, written by the creator of Idris, teaches you how to improve the performance and accuracy of your programs by taking advantage of a state-of-the-art type system. This book teaches you with Idris, a language designed to support type-driven development.

Part 1. Introduction

In this first part, you’ll get started with Idris and learn about the ideas behind type-driven development. I’ll take you on a brief tour of the Idris environment, and you’ll write some simple but complete programs.

In the first chapter, I’ll explain more about what I mean by type-driven development. Most importantly, I’ll define what I mean by “type” and give several examples of how you can use expressive types to describe the intended purpose of your programs more precisely. I’ll also introduce the two most distinctive features of the Idris language: holes, which stand for parts of programs that are yet to be written, and the use of types as a first-class language construct.

Before you get too deeply into type-driven development in Idris, it’s important to have a solid grasp of the fundamentals of the language. Therefore, in chapter 2, I’ll discuss some of the primitive language constructs, many of which will be familiar to you from other languages, and show how to construct complete programs in Idris.

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.

---

Idris is a relatively young programming language, designed from the beginning to support type-driven development. A prototype implementation first appeared in 2008, with development of the current implementation beginning in 2011. It builds on decades of research into the theoretical and practical foundations of programming languages and type systems.

In Idris, types are a first-class language construct. Types can be manipulated, used, passed as arguments to functions, and returned from functions just like any other value, such as numbers, strings, or lists. This is a simple but powerful idea:

• It allows relationships to be expressed between values; for example, that two lists have the same length.
• It allows assumptions to be made explicit and checkable by the compiler. For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run.
• If desired, it allows program behavior to be formally stated and proven correct.

In this chapter, I’ll introduce the Idris programming language and give a brief tour of its features and environment. I’ll also provide an overview of type-driven development, discussing why types matter in programming languages and how they can be used to guide software development. But first, it’s important to understand exactly what we mean when we talk about “types.”

1.1. What is a type?

We’re taught from an early age to recognize and distinguish types of objects. As a young child, you may have had a shape-sorter toy. This consists of a box with variously shaped holes in the top (see figure 1.1) and some shapes that fit through the holes. Sometimes they’re equipped with a small plastic hammer. The idea is to fit each shape (think of this as a “value”) into the appropriate hole (think of this as a “type”), possibly with coercion from the hammer.

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

In programming, types are a means of classifying values. For example, the values 94, "thing", and [1,2,3,4,5] could respectively be classified as an integer, a string, and a list of integers. Just as you can’t put a square shape in a round hole in the shape sorter, you can’t use a string like "thing" in a part of a program where you need an integer.

All modern programming languages classify values by type, although they differ enormously in when and how they do so (for example, whether they’re checked statically at compile time or dynamically at runtime, whether conversions between types are automatic or not, and so on).

Types serve several important roles:

• For a machine, types describe how bit patterns in memory are to be interpreted.
• For a compiler or interpreter, types help ensure that bit patterns are interpreted consistently when a program runs.
• For a programmer, types help name and organize concepts, aiding documentation and supporting interactive editing environments.

From our point of view in this book, the most important purpose of types is the third. Types help programmers in several ways:

• By allowing for the naming and organization of concepts (such as Square, Circle, Triangle, and Hexagon)
• By providing explicit documentation of the purposes of variables, functions, and programs
• By driving code completion in an interactive editing environment

As you’ll see, type-driven development makes extensive use of code completion in particular. Although all modern, statically typed languages support code completion to some extent, the expressivity of the Idris type system leads to powerful automatic code generation.

1.2. Introducing type-driven development

Type-driven development is a style of programming in which we write types first and use those types to guide the definition of functions. The overall process is to write the necessary data types, and then, for each function, do the following:

1. Write the input and output types.
2. Define the function, using the structure of the input types to guide the implementation.
3. Refine and edit the type and function definition as necessary.

---

Types as models

When you write a program, you’ll often have a conceptual model in your head (or, if you’re disciplined, even on paper) of how it’s supposed to work, how the components interact, and how the data is organized. This model is likely to be quite vague at first and will become more precise as the program evolves and your understanding of the concept develops.

Types allow you to make these models explicit in code and ensure that your implementation of a program matches the model in your head. Idris has an expressive type system that allows you to describe a model as precisely as you need, and to refine the model at the same time as developing the implementation.

---

In type-driven development, instead of thinking of types in terms of checking, with the type checker criticizing you when you make a mistake, you can think of types as being a plan, with the type checker acting as your guide, leading you to a working, robust program. Starting with a type and an empty function body, you gradually add details to the definition until it’s complete, regularly using the compiler to check that the program so far satisfies the type. Idris, as you’ll soon see, strongly encourages this style of programming by allowing incomplete function definitions to be checked, and by providing an expressive language for describing type...