Type-Driven Development with Idris

Type-Driven Development with Idris

by Edwin Brady
Released March 2017
Publisher(s): Manning Publications
ISBN: 9781617293023

Read it now on the O’Reilly learning platform with a 10-day free trial.

O’Reilly members get unlimited access to books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.

Start your free trial

Book description

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.



About the Technology

Stop fighting type errors! Type-driven development is an approach to coding that embraces types as the foundation of your code - essentially as built-in documentation your compiler can use to check data relationships and other assumptions. With this approach, you can define specifications early in development and write code that's easy to maintain, test, and extend. Idris is a Haskell-like language with first-class, dependent types that's perfect for learning type-driven programming techniques you can apply in any codebase.



About the Book

Type-Driven Development with Idris teaches you how to improve the performance and accuracy of your code by taking advantage of a state-of-the-art type system. In this book, you'll learn type-driven development of real-world software, as well as how to handle side effects, interaction, state, and concurrency. By the end, you'll be able to develop robust and verified software in Idris and apply type-driven development methods to other languages.



What's Inside

  • Understanding dependent types
  • Types as first-class language constructs
  • Types as a guide to program construction
  • Expressing relationships between data


About the Reader

Written for programmers with knowledge of functional programming concepts.



About the Author

Edwin Brady leads the design and implementation of the Idris language.



Quotes
This book will turn your approach to software upside-down, in the best way.
- Ian Dees, New Relic

Highly recommended for anyone developing software with serious safety requirements.
- Arnaud Bailly, GorillaSpace

After reading this book, TDD took on a new meaning for me.
- Giovanni Ruggiero, Eligotech

A clear and complete view of type-driven development that reveals the power of dependent types.
- Nicolas Biri, Luxembourg Institute of Science and Technology

Publisher resources

View/Submit Errata

Table of contents

  1. Type-Driven Development with Idris
    1. Edwin Brady
  2. Copyright
  3. Brief Table of Contents
  4. Table of Contents
  5. Preface
  6. Acknowledgments
  7. About this Book
    1. Who should read this book
    2. Roadmap
    3. Code conventions and downloads
    4. Author Online
    5. Other online resources
  8. About the Author
  9. About the Cover Illustration
  10. Part 1. Introduction
  11. Chapter 1. Overview
    1. 1.1. What is a type?
    2. 1.2. Introducing type-driven development
      1. 1.2.1. Matrix arithmetic
      2. 1.2.2. An automated teller machine
      3. 1.2.3. Concurrent programming
      4. 1.2.4. Type, define, refine: the process of type-driven development
      5. 1.2.5. Dependent types
    3. 1.3. Pure functional programming
      1. 1.3.1. Purity and referential transparency
      2. 1.3.2. Side-effecting programs
      3. 1.3.3. Partial and total functions
    4. 1.4. A quick tour of Idris
      1. 1.4.1. The interactive environment
      2. 1.4.2. Checking types
      3. 1.4.3. Compiling and running Idris programs
      4. 1.4.4. Incomplete definitions: working with holes
      5. 1.4.5. First-class types
    5. 1.5. Summary
  12. Chapter 2. Getting started with Idris
    1. 2.1. Basic types
      1. 2.1.1. Numeric types and values
      2. 2.1.2. Type conversions using cast
      3. 2.1.3. Characters and strings
      4. 2.1.4. Booleans
    2. 2.2. Functions: the building blocks of Idris programs
      1. 2.2.1. Function types and definitions
      2. 2.2.2. Partially applying functions
      3. 2.2.3. Writing generic functions: variables in types
      4. 2.2.4. Writing generic functions with constrained types
      5. 2.2.5. Higher-order function types
      6. 2.2.6. Anonymous functions
      7. 2.2.7. Local definitions: let and where
    3. 2.3. Composite types
      1. 2.3.1. Tuples
      2. 2.3.2. Lists
      3. 2.3.3. Functions with lists
    4. 2.4. A complete Idris program
      1. 2.4.1. Whitespace significance: the layout rule
      2. 2.4.2. Documentation comments
      3. 2.4.3. Interactive programs
    5. 2.5. Summary
  13. Part 2. Core Idris
  14. Chapter 3. Interactive development with types
    1. 3.1. Interactive editing in Atom
      1. 3.1.1. Interactive command summary
      2. 3.1.2. Defining functions by pattern matching
      3. 3.1.3. Data types and patterns
    2. 3.2. Adding precision to types: working with vectors
      1. 3.2.1. Refining the type of allLengths
      2. 3.2.2. Type-directed search: automatic refining
      3. 3.2.3. Type, define, refine: sorting a vector
    3. 3.3. Example: type-driven development of matrix functions
      1. 3.3.1. Matrix operations and their types
      2. 3.3.2. Transposing a matrix
    4. 3.4. Implicit arguments: type-level variables
      1. 3.4.1. The need for implicit arguments
      2. 3.4.2. Bound and unbound implicits
      3. 3.4.3. Using implicit arguments in functions
    5. 3.5. Summary
  15. Chapter 4. User-defined data types
    1. 4.1. Defining data types
      1. 4.1.1. Enumerations
      2. 4.1.2. Union types
      3. 4.1.3. Recursive types
      4. 4.1.4. Generic data types
    2. 4.2. Defining dependent data types
      1. 4.2.1. A first example: classifying vehicles by power source
      2. 4.2.2. Defining vectors
      3. 4.2.3. Indexing vectors with bounded numbers using Fin
    3. 4.3. Type-driven implementation of an interactive data store
      1. 4.3.1. Representing the store
      2. 4.3.2. Interactively maintaining state in main
      3. 4.3.3. Commands: parsing user input
      4. 4.3.4. Processing commands
    4. 4.4. Summary
  16. Chapter 5. Interactive programs: input and output processing
    1. 5.1. Interactive programming with IO
      1. 5.1.1. Evaluating and executing interactive programs
      2. 5.1.2. Actions and sequencing: the >>= operator
      3. 5.1.3. Syntactic sugar for sequencing with do notation
    2. 5.2. Interactive programs and control flow
      1. 5.2.1. Producing pure values in interactive definitions
      2. 5.2.2. Pattern-matching bindings
      3. 5.2.3. Writing interactive definitions with loops
    3. 5.3. Reading and validating dependent types
      1. 5.3.1. Reading a Vect from the console
      2. 5.3.2. Reading a Vect of unknown length
      3. 5.3.3. Dependent pairs
      4. 5.3.4. Validating Vect lengths
    4. 5.4. Summary
  17. Chapter 6. Programming with first-class types
    1. 6.1. Type-level functions: calculating types
      1. 6.1.1. Type synonyms: giving informative names to complex types
      2. 6.1.2. Type-level functions with pattern matching
      3. 6.1.3. Using case expressions in types
    2. 6.2. Defining functions with variable numbers of arguments
      1. 6.2.1. An addition function
      2. 6.2.2. Formatted output: a type-safe printf function
    3. 6.3. Enhancing the interactive data store with schemas
      1. 6.3.1. Refining the DataStore type
      2. 6.3.2. Using a record for the DataStore
      3. 6.3.3. Correcting compilation errors using holes
      4. 6.3.4. Displaying entries in the store
      5. 6.3.5. Parsing entries according to the schema
      6. 6.3.6. Updating the schema
      7. 6.3.7. Sequencing expressions with Maybe using do notation
    4. 6.4. Summary
  18. Chapter 7. Interfaces: using constrained generic types
    1. 7.1. Generic comparisons with Eq and Ord
      1. 7.1.1. Testing for equality with Eq
      2. 7.1.2. Defining the Eq constraint using interfaces and implementations
      3. 7.1.3. Default method definitions
      4. 7.1.4. Constrained implementations
      5. 7.1.5. Constrained interfaces: defining orderings with Ord
    2. 7.2. Interfaces defined in the Prelude
      1. 7.2.1. Converting to String with Show
      2. 7.2.2. Defining numeric types
      3. 7.2.3. Converting between types with Cast
    3. 7.3. Interfaces parameterized by Type -> Type
      1. 7.3.1. Applying a function across a structure with Functor
      2. 7.3.2. Reducing a structure using Foldable
      3. 7.3.3. Generic do notation using Monad and Applicative
    4. 7.4. Summary
  19. Chapter 8. Equality: expressing relationships between data
    1. 8.1. Guaranteeing equivalence of data with equality types
      1. 8.1.1. Implementing exactLength, first attempt
      2. 8.1.2. Expressing equality of Nats as a type
      3. 8.1.3. Testing for equality of Nats
      4. 8.1.4. Functions as proofs: manipulating equalities
      5. 8.1.5. Implementing exactLength, second attempt
      6. 8.1.6. Equality in general: the = type
    2. 8.2. Equality in practice: types and reasoning
      1. 8.2.1. Reversing a vector
      2. 8.2.2. Type checking and evaluation
      3. 8.2.3. The rewrite construct: rewriting a type using equality
      4. 8.2.4. Delegating proofs and rewriting to holes
      5. 8.2.5. Appending vectors, revisited
    3. 8.3. The empty type and decidability
      1. 8.3.1. Void: a type with no values
      2. 8.3.2. Decidability: checking properties with precision
      3. 8.3.3. DecEq: an interface for decidable equality
    4. 8.4. Summary
  20. Chapter 9. Predicates: expressing assumptions and contracts in types
    1. 9.1. Membership tests: the Elem predicate
      1. 9.1.1. Removing an element from a Vect
      2. 9.1.2. The Elem type: guaranteeing a value is in a vector
      3. 9.1.3. Removing an element from a Vect: types as contracts
      4. 9.1.4. auto-implicit arguments: automatically constructing proofs
      5. 9.1.5. Decidable predicates: deciding membership of a vector
    2. 9.2. Expressing program state in types: a guessing game
      1. 9.2.1. Representing the game’s state
      2. 9.2.2. A top-level game function
      3. 9.2.3. A predicate for validating user input: ValidInput
      4. 9.2.4. Processing a guess
      5. 9.2.5. Deciding input validity: checking ValidInput
      6. 9.2.6. Completing the top-level game implementation
    3. 9.3. Summary
  21. Chapter 10. Views: extending pattern matching
    1. 10.1. Defining and using views
      1. 10.1.1. Matching the last item in a list
      2. 10.1.2. Building views: covering functions
      3. 10.1.3. with blocks: syntax for extended pattern matching
      4. 10.1.4. Example: reversing a list using a view
      5. 10.1.5. Example: merge sort
    2. 10.2. Recursive views: termination and efficiency
      1. 10.2.1. “Snoc” lists: traversing a list in reverse
      2. 10.2.2. Recursive views and the with construct
      3. 10.2.3. Traversing multiple arguments: nested with blocks
      4. 10.2.4. More traversals: Data.List.Views
    3. 10.3. Data abstraction: hiding the structure of data using views
      1. 10.3.1. Digression: modules in Idris
      2. 10.3.2. The data store, revisited
      3. 10.3.3. Traversing the store’s contents with a view
    4. 10.4. Summary
  22. Part 3. Idris and the real world
  23. Chapter 11. Streams and processes: working with infinite data
    1. 11.1. Streams: generating and processing infinite lists
      1. 11.1.1. Labeling elements in a List
      2. 11.1.2. Producing an infinite list of numbers
      3. 11.1.3. Digression: what does it mean for a function to be total?
      4. 11.1.4. Processing infinite lists
      5. 11.1.5. The Stream data type
      6. 11.1.6. An arithmetic quiz using streams of random numbers
    2. 11.2. Infinite processes: writing interactive total programs
      1. 11.2.1. Describing infinite processes
      2. 11.2.2. Executing infinite processes
      3. 11.2.3. Executing infinite processes as total functions
      4. 11.2.4. Generating infinite structures using Lazy types
      5. 11.2.5. Extending do notation for InfIO
      6. 11.2.6. A total arithmetic quiz
    3. 11.3. Interactive programs with termination
      1. 11.3.1. Refining InfIO: introducing termination
      2. 11.3.2. Domain-specific commands
      3. 11.3.3. Sequencing Commands with do notation
    4. 11.4. Summary
  24. Chapter 12. Writing programs with state
    1. 12.1. Working with mutable state
      1. 12.1.1. The tree-traversal example
      2. 12.1.2. Representing mutable state using a pair
      3. 12.1.3. State, a type for describing stateful operations
      4. 12.1.4. Tree traversal with State
    2. 12.2. A custom implementation of State
      1. 12.2.1. Defining State and runState
      2. 12.2.2. Defining Functor, Applicative, and Monad implementations for State
    3. 12.3. A complete program with state: working with records
      1. 12.3.1. Interactive programs with state: the arithmetic quiz revisited
      2. 12.3.2. Complex state: defining nested records
      3. 12.3.3. Updating record field values
      4. 12.3.4. Updating record fields by applying functions
      5. 12.3.5. Implementing the quiz
      6. 12.3.6. Running interactive and stateful programs: executing the quiz
    4. 12.4. Summary
  25. Chapter 13. State machines: verifying protocols in types
    1. 13.1. State machines: tracking state in types
      1. 13.1.1. Finite state machines: modeling a door as a type
      2. 13.1.2. Interactive development of sequences of door operations
      3. 13.1.3. Infinite states: modeling a vending machine
      4. 13.1.4. A verified vending machine description
    2. 13.2. Dependent types in state: implementing a stack
      1. 13.2.1. Representing stack operations in a state machine
      2. 13.2.2. Implementing the stack using Vect
      3. 13.2.3. Using a stack interactively: a stack-based calculator
    3. 13.3. Summary
  26. Chapter 14. Dependent state machines: handling feedback and errors
    1. 14.1. Dealing with errors in state transitions
      1. 14.1.1. Refining the door model: representing failure
      2. 14.1.2. A verified, error-checking, door-protocol description
    2. 14.2. Security properties in types: modeling an ATM
      1. 14.2.1. Defining states for the ATM
      2. 14.2.2. Defining a type for the ATM
      3. 14.2.3. Simulating an ATM at the console: executing ATMCmd
      4. 14.2.4. Refining preconditions using auto-implicits
    3. 14.3. A verified guessing game: describing rules in types
      1. 14.3.1. Defining an abstract game state and operations
      2. 14.3.2. Defining a type for the game state
      3. 14.3.3. Implementing the game
      4. 14.3.4. Defining a concrete game state
      5. 14.3.5. Running the game: executing GameLoop
    4. 14.4. Summary
  27. Chapter 15. Type-safe concurrent programming
    1. 15.1. Primitives for concurrent programming in Idris
      1. 15.1.1. Defining concurrent processes
      2. 15.1.2. The Channels library: primitive message passing
      3. 15.1.3. Problems with channels: type errors and blocking
    2. 15.2. Defining a type for safe message passing
      1. 15.2.1. Describing message-passing processes in a type
      2. 15.2.2. Making processes total using Inf
      3. 15.2.3. Guaranteeing responses using a state machine and Inf
      4. 15.2.4. Generic message-passing processes
      5. 15.2.5. Defining a module for Process
      6. 15.2.6. Example 1: List processing
      7. 15.2.7. Example 2: A word-counting process
    3. 15.3. Summary
  28. Appendix A. Installing Idris and editor modes
    1. The Idris compiler and environment
    2. Mac OS
    3. Windows
    4. Unix-like platforms, installing from source
    5. Editor modes
    6. Atom
    7. Other editors
  29. Appendix B. Interactive editing commands
  30. Appendix C. REPL commands
  31. Appendix D. Further reading
    1. Functional programming in Haskell
    2. Other languages and tools with expressive type systems
    3. Theoretical foundations
    4. Total functional programming
    5. Types for concurrency
  32. Appendix E.
  33. Appendix F.
  34. Index
  35. List of Figures
  36. List of Tables
  37. List of Listings

Product information

  • Title: Type-Driven Development with Idris
  • Author(s): Edwin Brady
  • Release date: March 2017
  • Publisher(s): Manning Publications
  • ISBN: 9781617293023