Type-Driven Development with Idris

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 ...