Copyright
Brief Table of Contents
Table of Contents
Preface
Acknowledgments
About this Book
About the Author
About the Cover Illustration
1. Introduction
Chapter 1. Overview
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
Chapter 2. Getting started with Idris
2.1. Basic types
2.1.1. Numeric types and values
2.1.2. Type conversions using cast
2.1.3. Characters and strings