Type-Driven Development with Idris
Edwin Brady
  • MEAP began September 2015
  • Publication in March 2017 (estimated)
  • ISBN 9781617293023
  • 600 pages (estimated)
  • printed in black & white
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 from the very beginning to support type-driven development. In this book, you?ll learn how to manipulate types just like any other construct (numbers, strings, lists, etc.). You?ll see how to use type-driven development to build real-world software, as well as how to handle side-effects, state and concurrency, and interoperating with existing systems. By the end of this book, you will be able to develop robust and verified software in Idris and apply type-driven development methods to programming in other languages.
Table of Contents detailed table of contents

Part 1: Introduction

1. Overview

1.1. What is a Type?

1.2. A quick tour of Idris

1.2.1. The interactive environment

1.2.2. Checking Types

1.2.3. Compiling and Running Idris Programs

1.2.4. Incomplete Definitions: Working with Holes

1.2.5. Types as a First-class Construct

1.3. Introducing Type-driven Development

1.3.1. What is Type-driven Development?

1.3.2. Types and Precision

1.3.3. Dependent Types

1.3.4. Introductory Exercises

1.4. Pure Functional Programming

1.4.1. Purity and Referential Transparency

1.4.2. Side Effecting Programs

1.4.3. Partial and Total Functions

1.5. Dependent Types In Action: Modelling a Vending Machine

1.5.1. Vending machine description

1.5.2. A Type-driven Vending Machine

1.5.3. Type, Define, Refine: The Process of Type-driven Development

1.6. Summary

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

2.1.4. Booleans

2.2. Functions: The Building Blocks of Idris Programs

2.2.1. Function Types and Definitions

2.2.2. Partially Applying Functions

2.2.3. Writing Generic Functions: Variables in Types

2.2.4. Writing Generic Functions with Constrained Types

2.2.5. Higher Order Function Types

2.2.6. Anonymous Functions

2.2.7. Local definitions: let and where

2.3. Composite Types

2.3.1. Tuples

2.3.2. Lists

2.3.3. Functions with Lists

2.4. A Complete Idris Program

2.4.1. Whitespace Significance: The Layout Rule

2.4.2. Documentation Comments

2.4.3. Interactive Programs

2.5. Exercises

2.6. Summary

Part 2: Core Idris

3. Interactive Development with Types

3.1. Interactive Editing in Atom

3.1.1. Interactive Command Summary

3.1.2. Defining Functions by Pattern Matching

3.1.3. Data Types and Patterns

3.2. Adding Precision to Types: Working with Vectors

3.2.1. Refining the Type of word_lengths

3.2.2. Type Directed Search: Automatic Refining

3.2.3. Type, Define, Refine: Sorting a Vector

3.2.4. Exercises

3.3. Example: Type-driven Development of Matrix Functions

3.3.1. Matrix Operations and Their Types

3.3.2. Transposing a Matrix

3.3.3. Exercises

3.4. Implicit Arguments: Type Level Variables

3.4.1. The Need for Implicit Arguments

3.4.2. Bound and Unbound implicits

3.4.3. Using Implicit Arguments in Functions

3.5. Summary

4. User Defined Data Types

4.1. Defining Data Types

4.1.1. Enumerations

4.1.2. Union Types

4.1.3. Recursive Types

4.1.4. Generic Data Types

4.1.5. Exercises

4.2. Defining Dependent Data Types

4.2.1. A First Example: Classifying Vehicles by Power Source

4.2.2. Defining Vectors

4.2.3. Indexing Vectors with Bounded Numbers using Fin

4.2.4. Exercises

4.3. Type-driven Implementation of an Interactive Data Store

4.3.1. Representing the Store

4.3.2. Interactively Maintaining State in main

4.3.3. Commands: Parsing User Input

4.3.4. Processing Commands

4.3.5. Exercises

4.4. Summary

5. Interactive Programs: Input and Output Processing

5.1. Interactive Programming with IO

5.1.1. Evaluation and Execution of Interactive Programs

5.1.2. Actions and Sequencing: The >>= Operator

5.1.3. Syntactic Sugar for Sequencing with do Notation

5.1.4. Exercises

5.2. Interactive Programs and Control Flow

5.2.1. Producing Pure Values in Interactive Definitions

5.2.2. Pattern Matching Bindings

5.2.3. Writing Interactive Definitions with Loops

5.2.4. Exercises

5.3. Reading and Validating Dependent Types

5.3.1. Reading a Vect from the Console

5.3.2. Reading a Vect of Unknown Length

5.3.3. Dependent Pairs

5.3.4. Validating Vect Lengths

5.3.5. Exercises

5.4. Summary

6. Programming with First Class Types

6.1. Type Level Functions: Calculating Types

6.1.1. Type Synonyms: Giving Informative Names to Complex Types

6.1.2. Type Level Functions with Pattern Matching

6.1.3. Using case Expressions in Types

6.2. Defining Functions with Variable Numbers of Arguments

6.2.1. An Addition Function

6.2.2. Formatted Output: A Type Safe printf Function

6.2.3. Exercises

6.3. Enhancing the Interactive Data Store with Schemas

6.3.1. Refining the DataStore type

6.3.2. Using a Record for the DataStore

6.3.3. Correcting Compilation Errors using Holes

6.3.4. Displaying Entries in the Store

6.3.5. Parsing Entries According to the Schema

6.3.6. Updating the Schema

6.3.7. Sequencing Expressions with Maybe using do notation

6.3.8. Exercises

6.4. Summary

7. Interfaces: Using Constrained Generic Types

7.1. Generic Comparisons with Eq and Ord

7.1.1. Testing for Equality with Eq

7.1.2. Defining the Eq Constraint using Interfaces and Implementations

7.1.3. Default Method Definitions

7.1.4. Constrained Implementations

7.1.5. Constrained Interfaces: Defining Orderings with Ord

7.1.6. Exercises

7.2. Interfaces Defined in the Prelude

7.2.1. Converting to String with Show

7.2.2. Defining Numeric Types

7.2.3. Converting Between Types with Cast

7.2.4. Exercises

7.3. Interfaces Parameterised by Type -> Type

7.3.1. Applying a Function Across a Structure with Functor

7.3.2. Reducing a Structure using Foldable

7.3.3. Generic do notation using Monad and Applicative

7.3.4. Exercises

7.4. Summary

8. Equality: Expressing Relationships Between Data

8.1. Guaranteeing Equivalence of Data with Equality Types

8.1.1. Implementing exactLength, First Attempt

8.1.2. Expressing Equality of Nats as a Type

8.1.3. Testing for Equality of Nats

8.1.4. Functions as Proofs: Manipulating Equalities

8.1.5. Implementing exactLength, Second Attempt

8.1.6. Equality in General: The = Type

8.1.7. Exercises

8.2. Equality in Practice: Types and Reasoning

8.2.1. Reversing a Vector: First Attempt

8.2.2. Type Checking and Evaluation

8.2.3. The rewrite Construct: Rewriting a Type using Equality

8.2.4. Delegating Proofs and Rewriting to Holes

8.2.5. Appending Vectors, Revisited

8.2.6. Exercises

8.3. The Empty Type and Decidability

8.3.1. Void: a Type with No Values

8.3.2. Decidability: Checking Properties with Precision

8.3.3. DecEq: an Interface for Decidable Equality

8.3.4. Exercises

8.4. Summary

9. Predicates: Expressing Assumptions and Contracts in Types

9.1. Membership Tests: The Elem Predicate

9.1.1. Removing an Element from a Vect, First Attempt

9.1.2. The Elem Type: Guaranteeing a Value is in a Vector

9.1.3. Removing an Element from a Vect: Types as Contracts

9.1.4. auto-Implicit Arguments: Automatically Constructing Proofs

9.1.5. Decidable Predicates: Deciding Membership of a Vector

9.1.6. Exercises

9.2. Expressing Program State in Types: A Guessing Game

9.2.1. Representing the Game's State

9.2.2. A Top Level Game Function

9.2.3. A Predicate for Validating User Input: ValidInput

9.2.4. Processing a Guess

9.2.5. Deciding Input Validity: Checking ValidInput

9.2.6. Completing the Top Level Game Implementation

9.3. Summary

10. Views: Extending Pattern Matching

10.1. Defining and Using Views

10.1.1. Matching the Last Item in a List

10.1.2. Building Views: Covering Functions

10.1.3. with blocks: Syntax for Extended Pattern Matching

10.1.4. Example: Reversing a List using a View

10.1.5. Example: Merge Sort

10.1.6. Exercises

10.2. Recursive Views: Termination and Efficiency

10.2.1. "Snoc" Lists: Traversing a List in Reverse

10.2.2. Recursive Views and the with Construct

10.2.3. Traversing Multiple Arguments: Nested with Blocks

10.2.4. More Traversals: Data.List.Views

10.2.5. Exercises

10.3. Data Abstraction: Hiding the Structure of Data Using Views

10.3.1. Digression: Modules in Idris

10.3.2. The Data Store, Revisited

10.3.3. Traversing the Store’s Contents with a View

10.3.4. Exercises

10.4. Summary

11. Streams and Processes: Working with Infinite Data

11.1. Streams: Generating and Processing Infinite Lists

11.1.1. First Example: Tagging Elements in a List

11.1.2. Producing an Infinite List of Numbers

11.1.3. Digression: What Does it Mean for a Function to be Total?

11.1.4. Processing Infinite Lists

11.1.5. The Stream data type

11.1.6. An Arithmetic Quiz Using Streams of Random Numbers

11.1.7. Exercises

11.2. Infinite Processes: Writing Interactive Total Programs

11.2.1. Describing Infinite Processes

11.2.2. Executing Infinite Processes

11.2.3. Executing Infinite Processes as Total Functions

11.2.4. Generating Infinite Structures using Lazy Types

11.2.5. Extending do-notation for InfIO

11.2.6. A Total Arithmetic Quiz

11.2.7. Exercise

11.3. Refining the Types: Mixing Termination and Productivity

11.3.1. Interactive Programs with Termination

11.3.2. Domain Specific Commands

11.3.3. Sequencing Commands with do-notation

11.3.4. Exercises

11.4. Summary

Part 3: Idris and the Real World

12. Writing Programs with State

12.1. The Generic State Type: Writing Programs with State

12.1.1. Tree Labelling First Attempt: Using a Pair

12.1.2. State, a Type for Describing Stateful Operations

12.1.3. Managing Tree Labelling State

12.1.4. Exercises

12.2. A Custom Implementation of State

12.2.1. Defining State and runState

12.2.2. Defining Functor, Applicative and Monad Implementations for State

12.3. A Complete Program with State: Working with Records

12.3.1. Interactive Programs with State: The Arithmetic Quiz Revisited

12.3.2. Complex State: Defining Nested Records

12.3.3. Updating Record Field Values

12.3.4. Updating Record Fields by Applying Functions

12.3.5. Implementing the Quiz

12.3.6. Running Interactive and Stateful Programs: Executing the Quiz

12.3.7. Exercises

12.4. Summary

13. State Machines: Verifying Protocols in Types

13.1. State Machines: Tracking State in Types

13.1.1. Finite State Machines: Modelling a Door as a Type

13.1.2. Interactive Development of Sequences of Door Operations

13.1.3. Infinite States: Modelling a Vending Machine

13.1.4. A Verified Vending Machine Description

13.1.5. Exercises

13.2. Dependent Types in State: Implementing a Stack

13.2.1. Representing Stack Operations in a State Machine

13.2.2. Implementing the Stack using Vect

13.2.3. Using a Stack Interactively: A Stack-based Calculator

13.2.4. Exercises

13.3. Summary

14. Dependent State Machines: Handling Feedback and Errors

14.1. Dealing with Errors in State Transitions

14.1.1. Refining the Door Model: Representing Failure

14.1.2. A Verified, Error Checking, Door Protocol Description

14.2. Security Properties in Types: Modelling an ATM

14.2.1. Defining States for the ATM

14.2.2. Defining a Type for the ATM

14.2.3. Simulating an ATM at the Console: Executing ATMCmd

14.2.4. Refining Preconditions using auto-implicits

14.2.5. Exercises

14.3. A Verified Guessing Game: Describing Rules in Types

14.3.1. Defining an Abstract Game State and Operations

14.3.2. Defining a Type for the Game State

14.3.3. Implementing the Game

14.3.4. Defining a Concrete Game State

14.3.5. Running the Game: Executing GameLoop

14.4. Summary

15. Type-safe Concurrent Programming

15.1. Primitives for Concurrent Programming in Idris

15.1.1. Defining Concurrent Processes

15.1.2. The Channels Library: Primitive Message Passing

15.1.3. Problems with Channels: Type Errors and Blocking

15.2. Defining a Type for Safe Message Passing

15.2.1. Describing Message Passing Processes in a Type

15.2.2. Making Processes Total using Inf

15.2.3. Guaranteeing Responses using a State Machine and Inf

15.2.4. Generic Message Passing Processes

15.2.5. Defining a module for Process

15.2.6. Example 1: List Processing

15.2.7. Example 2: A Word Counting Process

15.3. Summary


Appendix A: Installing Idris and Editor Modes

==A.1 The Idris Compiler and Environment ==A.1.1 OS X ==A.1.2 Windows ==A.1.3 Unix-like platforms, installing from source ==A.2 Editor Modes ==A.2.1 Atom ==A.2.2 Other Editors

Appendix B: Interactive Editing Commands

Appendix C: REPL Commands

Appendix D: The Packaging System

About the Technology

Types are often seen as a tool for checking errors, with the programmer writing a complete program first and using the type checker to detect errors. And while tests are used to show presence of errors, they can only find errors that you explicitly test for. In type-driven development, types become your tools for constructing programs and, used appropriately, can show the absence of errors. And you can express precise relationships between data, your assumptions are explicit and checkable, and you can precisely state and verify properties. Type-driven development lets you write extensible code, create simple specifications very early in development, and easily create mock implementation for testing.

What's inside

  • Idris fundamentals
  • Understanding dependent types
  • Types as a first-class language construct
  • Using types to guide program construction
  • Expressing relationships between data

About the reader

Written for programmers with knowledge of basic functional programming concepts.

About the author

Edwin Brady leads the design and implementation of the Idris language. He is a Lecturer in Computer Science and regularly speaks at conferences.

Manning Early Access Program (MEAP) Read chapters as they are written, get the finished eBook as soon as it’s ready, and receive the pBook long before it's in bookstores.
  • MEAP combo $49.99 pBook + eBook
  • MEAP eBook $39.99 pdf + ePub + kindle

FREE domestic shipping on three or more pBooks