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.

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.

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 Idris for Practical Programming end, you’ll be able to develop robust and verified software in Idris and apply type-driven development methods to other languages.

Prerequisites for Idris

1. Basic Programming Knowledge: Familiarity with programming concepts such as variables, functions, and control structures.
2. Understanding of Functional Programming: Grasp of functional programming principles, including recursion and higher-order functions.
3. Familiarity with Haskell: Prior experience with Haskell can be beneficial, given the similarities between the two languages.
4. Mathematical Foundations: Basic understanding of type theory and logic will help in grasping dependent types.
5. Development Environment Setup: Knowledge of installing Idris and setting up a suitable development environment.

TABLE OF CONTENT

1. Introduction to Idris
   1.1 What is Idris?
   1.2 Features of Idris
   1.3 Setting Up Your Idris Environment
   1.4 Your First Idris Program
2. Core Idris
   2.1 Interactive Development with Types
   2.2 User Defined Data Types
   2.3 Interactive Programs: Input and Output Processing
   2.4 Programming with First Class Types
   2.5 Interfaces: Using Constrained Generic Types
   2.6 Equality: Expressing Relationships Between Data
   2.7 Predicates: Expressing Assumptions and Contracts in Types
   2.8 Views: Extending Pattern Matching
3. Idris and the Real World
   3.1 Streams and Processes: Working with Infinite Data
   3.2 Writing Programs with State
   3.3 State Machines: Verifying Protocols in Types
   3.4 Dependent State Machines: Handling Feedback and Errors
   3.5 Type-safe Concurrent Programming