book

Type-Driven Development with Idris

Name: Type-Driven Development with Idris
Author: Edwin Brady
ISBN: 9781617293023

by Edwin Brady

March 2017

Intermediate to advanced

480 pages

12h 52m

English

Manning Publications

Read now

Unlock full access

Type-Driven Development with Idris
Edwin Brady
Copyright
Brief Table of Contents
Table of Contents
Preface
Acknowledgments
About this Book
Who should read this bookRoadmapCode conventions and downloadsAuthor OnlineOther online resources
About the Author
About the Cover Illustration
Part 1. Introduction

Chapter 1. Overview
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
Chapter 2. Getting started with Idris
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
Part 2. Core Idris
Chapter 3. Interactive development with types
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
Chapter 4. User-defined data types
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
Chapter 5. Interactive programs: input and output processing
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
Chapter 6. Programming with first-class types
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
Chapter 7. Interfaces: using constrained generic types
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
Chapter 8. Equality: expressing relationships between data
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
Chapter 9. Predicates: expressing assumptions and contracts in types
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
Chapter 10. Views: extending pattern matching
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
Part 3. Idris and the real world
Chapter 11. Streams and processes: working with infinite data
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
Chapter 12. Writing programs with state
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
Chapter 13. State machines: verifying protocols in types
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
Chapter 14. Dependent state machines: handling feedback and errors
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
Chapter 15. Type-safe concurrent programming
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
Appendix A. Installing Idris and editor modes
The Idris compiler and environmentMac OSWindowsUnix-like platforms, installing from sourceEditor modesAtomOther editors
Appendix B. Interactive editing commands
Appendix C. REPL commands
Appendix D. Further reading
Functional programming in HaskellOther languages and tools with expressive type systemsTheoretical foundationsTotal functional programmingTypes for concurrency
Appendix E.
Appendix F.
Index
List of Figures
List of Tables
List of Listings

Content preview from Type-Driven Development with Idris

Chapter 9. Predicates: expressing assumptions and contracts in types

This chapter covers

Describing and checking membership of a vector using a predicate
Using predicates to describe contracts for function inputs and outputs
Reasoning about system state in types

Dependent types like EqNat and =, which you saw in the previous chapter, are used entirely for describing relationships between data. These types are often referred to as predicates, which are data types that exist entirely to describe a property of some data. If you can construct a value for a predicate, then you know the property described by that predicate must be true.

In this chapter, you’ll see how to express more-complex relationships between data using predicates. By expressing ...

Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.

Read now

Unlock full access

More than 5,000 organizations count on O’Reilly

O’Reilly covers everything we've got, with content to help us build a world-class technology community, upgrade the capabilities and competencies of our teams, and improve overall team performance as well as their engagement.

Julian F.

Head of Cybersecurity

I wanted to learn C and C++, but it didn't click for me until I picked up an O'Reilly book. When I went on the O’Reilly platform, I was astonished to find all the books there, plus live events and sandboxes so you could play around with the technology.

Addison B.

Field Engineer

I’ve been on the O’Reilly platform for more than eight years. I use a couple of learning platforms, but I'm on O'Reilly more than anybody else. When you're there, you start learning. I'm never disappointed.

Amir M.

Data Platform Tech Lead

I'm always learning. So when I got on to O'Reilly, I was like a kid in a candy store. There are playlists. There are answers. There's on-demand training. It's worth its weight in gold, in terms of what it allows me to do.

Mark W.

Embedded Software Engineer

Publisher Resources

ISBN: 9781617293023Publisher Support Publisher Website Errata Page

Cloud Computing

Data Engineering

Data Science

AI & ML

Programming Languages

Software Architecture

IT/Ops

Security

Design

Business

Soft Skills

Type-Driven Development with Idris

by Edwin Brady

Chapter 9. Predicates: expressing assumptions and contracts in types

Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.