book

Type-Driven Development with Idris

by Edwin Brady

March 2017

Intermediate to advanced

480 pages

12h 52m

English

Manning Publications

Read now

Unlock full access

Edwin Brady
Who should read this bookRoadmapCode conventions and downloadsAuthor OnlineOther online resources

1.1. What is a type?1.2. Introducing type-driven development1.2.1. Matrix arithmetic1.2.2. An automated teller machine1.2.3. Concurrent programming1.2.4. Type, define, refine: the process of type-driven development1.2.5. Dependent types1.3. Pure functional programming1.3.1. Purity and referential transparency1.3.2. Side-effecting programs1.3.3. Partial and total functions1.4. A quick tour of Idris1.4.1. The interactive environment1.4.2. Checking types1.4.3. Compiling and running Idris programs1.4.4. Incomplete definitions: working with holes1.4.5. First-class types1.5. Summary
2.1. Basic types2.1.1. Numeric types and values2.1.2. Type conversions using cast2.1.3. Characters and strings2.1.4. Booleans2.2. Functions: the building blocks of Idris programs2.2.1. Function types and definitions2.2.2. Partially applying functions2.2.3. Writing generic functions: variables in types2.2.4. Writing generic functions with constrained types2.2.5. Higher-order function types2.2.6. Anonymous functions2.2.7. Local definitions: let and where2.3. Composite types2.3.1. Tuples2.3.2. Lists2.3.3. Functions with lists2.4. A complete Idris program2.4.1. Whitespace significance: the layout rule2.4.2. Documentation comments2.4.3. Interactive programs2.5. Summary
3.1. Interactive editing in Atom3.1.1. Interactive command summary3.1.2. Defining functions by pattern matching3.1.3. Data types and patterns3.2. Adding precision to types: working with vectors3.2.1. Refining the type of allLengths3.2.2. Type-directed search: automatic refining3.2.3. Type, define, refine: sorting a vector3.3. Example: type-driven development of matrix functions3.3.1. Matrix operations and their types3.3.2. Transposing a matrix3.4. Implicit arguments: type-level variables3.4.1. The need for implicit arguments3.4.2. Bound and unbound implicits3.4.3. Using implicit arguments in functions3.5. Summary
4.1. Defining data types4.1.1. Enumerations4.1.2. Union types4.1.3. Recursive types4.1.4. Generic data types4.2. Defining dependent data types4.2.1. A first example: classifying vehicles by power source4.2.2. Defining vectors4.2.3. Indexing vectors with bounded numbers using Fin4.3. Type-driven implementation of an interactive data store4.3.1. Representing the store4.3.2. Interactively maintaining state in main4.3.3. Commands: parsing user input4.3.4. Processing commands4.4. Summary
5.1. Interactive programming with IO5.1.1. Evaluating and executing interactive programs5.1.2. Actions and sequencing: the >>= operator5.1.3. Syntactic sugar for sequencing with do notation5.2. Interactive programs and control flow5.2.1. Producing pure values in interactive definitions5.2.2. Pattern-matching bindings5.2.3. Writing interactive definitions with loops5.3. Reading and validating dependent types5.3.1. Reading a Vect from the console5.3.2. Reading a Vect of unknown length5.3.3. Dependent pairs5.3.4. Validating Vect lengths5.4. Summary
6.1. Type-level functions: calculating types6.1.1. Type synonyms: giving informative names to complex types6.1.2. Type-level functions with pattern matching6.1.3. Using case expressions in types6.2. Defining functions with variable numbers of arguments6.2.1. An addition function6.2.2. Formatted output: a type-safe printf function6.3. Enhancing the interactive data store with schemas6.3.1. Refining the DataStore type6.3.2. Using a record for the DataStore6.3.3. Correcting compilation errors using holes6.3.4. Displaying entries in the store6.3.5. Parsing entries according to the schema6.3.6. Updating the schema6.3.7. Sequencing expressions with Maybe using do notation6.4. Summary
7.1. Generic comparisons with Eq and Ord7.1.1. Testing for equality with Eq7.1.2. Defining the Eq constraint using interfaces and implementations7.1.3. Default method definitions7.1.4. Constrained implementations7.1.5. Constrained interfaces: defining orderings with Ord7.2. Interfaces defined in the Prelude7.2.1. Converting to String with Show7.2.2. Defining numeric types7.2.3. Converting between types with Cast7.3. Interfaces parameterized by Type -> Type7.3.1. Applying a function across a structure with Functor7.3.2. Reducing a structure using Foldable7.3.3. Generic do notation using Monad and Applicative7.4. Summary
8.1. Guaranteeing equivalence of data with equality types8.1.1. Implementing exactLength, first attempt8.1.2. Expressing equality of Nats as a type8.1.3. Testing for equality of Nats8.1.4. Functions as proofs: manipulating equalities8.1.5. Implementing exactLength, second attempt8.1.6. Equality in general: the = type8.2. Equality in practice: types and reasoning8.2.1. Reversing a vector8.2.2. Type checking and evaluation8.2.3. The rewrite construct: rewriting a type using equality8.2.4. Delegating proofs and rewriting to holes8.2.5. Appending vectors, revisited8.3. The empty type and decidability8.3.1. Void: a type with no values8.3.2. Decidability: checking properties with precision8.3.3. DecEq: an interface for decidable equality8.4. Summary
9.1. Membership tests: the Elem predicate9.1.1. Removing an element from a Vect9.1.2. The Elem type: guaranteeing a value is in a vector9.1.3. Removing an element from a Vect: types as contracts9.1.4. auto-implicit arguments: automatically constructing proofs9.1.5. Decidable predicates: deciding membership of a vector9.2. Expressing program state in types: a guessing game9.2.1. Representing the game’s state9.2.2. A top-level game function9.2.3. A predicate for validating user input: ValidInput9.2.4. Processing a guess9.2.5. Deciding input validity: checking ValidInput9.2.6. Completing the top-level game implementation9.3. Summary
10.1. Defining and using views10.1.1. Matching the last item in a list10.1.2. Building views: covering functions10.1.3. with blocks: syntax for extended pattern matching10.1.4. Example: reversing a list using a view10.1.5. Example: merge sort10.2. Recursive views: termination and efficiency10.2.1. “Snoc” lists: traversing a list in reverse10.2.2. Recursive views and the with construct10.2.3. Traversing multiple arguments: nested with blocks10.2.4. More traversals: Data.List.Views10.3. Data abstraction: hiding the structure of data using views10.3.1. Digression: modules in Idris10.3.2. The data store, revisited10.3.3. Traversing the store’s contents with a view10.4. Summary
11.1. Streams: generating and processing infinite lists11.1.1. Labeling elements in a List11.1.2. Producing an infinite list of numbers11.1.3. Digression: what does it mean for a function to be total?11.1.4. Processing infinite lists11.1.5. The Stream data type11.1.6. An arithmetic quiz using streams of random numbers11.2. Infinite processes: writing interactive total programs11.2.1. Describing infinite processes11.2.2. Executing infinite processes11.2.3. Executing infinite processes as total functions11.2.4. Generating infinite structures using Lazy types11.2.5. Extending do notation for InfIO11.2.6. A total arithmetic quiz11.3. Interactive programs with termination11.3.1. Refining InfIO: introducing termination11.3.2. Domain-specific commands11.3.3. Sequencing Commands with do notation11.4. Summary
12.1. Working with mutable state12.1.1. The tree-traversal example12.1.2. Representing mutable state using a pair12.1.3. State, a type for describing stateful operations12.1.4. Tree traversal with State12.2. A custom implementation of State12.2.1. Defining State and runState12.2.2. Defining Functor, Applicative, and Monad implementations for State12.3. A complete program with state: working with records12.3.1. Interactive programs with state: the arithmetic quiz revisited12.3.2. Complex state: defining nested records12.3.3. Updating record field values12.3.4. Updating record fields by applying functions12.3.5. Implementing the quiz12.3.6. Running interactive and stateful programs: executing the quiz12.4. Summary
13.1. State machines: tracking state in types13.1.1. Finite state machines: modeling a door as a type13.1.2. Interactive development of sequences of door operations13.1.3. Infinite states: modeling a vending machine13.1.4. A verified vending machine description13.2. Dependent types in state: implementing a stack13.2.1. Representing stack operations in a state machine13.2.2. Implementing the stack using Vect13.2.3. Using a stack interactively: a stack-based calculator13.3. Summary
14.1. Dealing with errors in state transitions14.1.1. Refining the door model: representing failure14.1.2. A verified, error-checking, door-protocol description14.2. Security properties in types: modeling an ATM14.2.1. Defining states for the ATM14.2.2. Defining a type for the ATM14.2.3. Simulating an ATM at the console: executing ATMCmd14.2.4. Refining preconditions using auto-implicits14.3. A verified guessing game: describing rules in types14.3.1. Defining an abstract game state and operations14.3.2. Defining a type for the game state14.3.3. Implementing the game14.3.4. Defining a concrete game state14.3.5. Running the game: executing GameLoop14.4. Summary
15.1. Primitives for concurrent programming in Idris15.1.1. Defining concurrent processes15.1.2. The Channels library: primitive message passing15.1.3. Problems with channels: type errors and blocking15.2. Defining a type for safe message passing15.2.1. Describing message-passing processes in a type15.2.2. Making processes total using Inf15.2.3. Guaranteeing responses using a state machine and Inf15.2.4. Generic message-passing processes15.2.5. Defining a module for Process15.2.6. Example 1: List processing15.2.7. Example 2: A word-counting process15.3. Summary
The Idris compiler and environmentMac OSWindowsUnix-like platforms, installing from sourceEditor modesAtomOther editors
Functional programming in HaskellOther languages and tools with expressive type systemsTheoretical foundationsTotal functional programmingTypes for concurrency

Content preview from Type-Driven Development with 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 ...