Type-Driven Development with Idris
eBook - ePub

Type-Driven Development with Idris

Edwin Brady

  1. English
  2. ePUB (mobile friendly)
  3. Available on iOS & Android
eBook - ePub

Type-Driven Development with Idris

Edwin Brady

Book details
Book preview
Table of contents

About This Book

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.

Frequently asked questions

How do I cancel my subscription?
Simply head over to the account section in settings and click on “Cancel Subscription” - it’s as simple as that. After you cancel, your membership will stay active for the remainder of the time you’ve paid for. Learn more here.
Can/how do I download books?
At the moment all of our mobile-responsive ePub books are available to download via the app. Most of our PDFs are also available to download and we're working on making the final remaining ones downloadable now. Learn more here.
What is the difference between the pricing plans?
Both plans give you full access to the library and all of Perlego’s features. The only differences are the price and subscription period: With the annual plan you’ll save around 30% compared to 12 months on the monthly plan.
What is Perlego?
We are an online textbook subscription service, where you can get access to an entire online library for less than the price of a single book per month. With over 1 million books across 1000+ topics, we’ve got you covered! Learn more here.
Do you support text-to-speech?
Look out for the read-aloud symbol on your next book to see if you can listen to it. The read-aloud tool reads text aloud for you, highlighting the text as it is being read. You can pause it, speed it up and slow it down. Learn more here.
Is Type-Driven Development with Idris an online PDF/ePUB?
Yes, you can access Type-Driven Development with Idris by Edwin Brady in PDF and/or ePUB format, as well as other popular books in Computer Science & Software Development. We have over one million books available in our catalogue for you to explore.


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

Table of contents

  1. Type-Driven Development with Idris
  2. Copyright
  3. Brief Table of Contents
  4. Table of Contents
  5. Preface
  6. Acknowledgments
  7. About this Book
  8. About the Author
  9. About the Cover Illustration
  10. Part 1. Introduction
  11. Chapter 1. Overview
  12. Chapter 2. Getting started with Idris
  13. Part 2. Core Idris
  14. Chapter 3. Interactive development with types
  15. Chapter 4. User-defined data types
  16. Chapter 5. Interactive programs: input and output processing
  17. Chapter 6. Programming with first-class types
  18. Chapter 7. Interfaces: using constrained generic types
  19. Chapter 8. Equality: expressing relationships between data
  20. Chapter 9. Predicates: expressing assumptions and contracts in types
  21. Chapter 10. Views: extending pattern matching
  22. Part 3. Idris and the real world
  23. Chapter 11. Streams and processes: working with infinite data
  24. Chapter 12. Writing programs with state
  25. Chapter 13. State machines: verifying protocols in types
  26. Chapter 14. Dependent state machines: handling feedback and errors
  27. Chapter 15. Type-safe concurrent programming
  28. Appendix A. Installing Idris and editor modes
  29. Appendix B. Interactive editing commands
  30. Appendix C. REPL commands
  31. Appendix D. Further reading
  32. Appendix E.
  33. Appendix F.
  34. Index
  35. List of Figures
  36. List of Tables
  37. List of Listings