Type-driven Development with Idris
Summary 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. Purchase of the print book includes a free eBook in PDF, Kindle, and ePub formats from Manning Publications. 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.
Stats for nerds
30recommend
47mentions
36people
2016–2026years
81% recommend19% neutral
Mentions per year
What Hacker News says
- One option is dependent pairs, where one value of the pair (in this example) would be the length of the array and the other value is a type which depends on that same value (such as Vector n T instead of List T).
Type-Driven Development with Idris[1] is a great introduction for dependently typed languages and covers methods such as these if you're interested (and Edwin Brady is a great teacher).
[1] https://www.manning.com/books/type-driven-development-with-i...
- Books. Some books on my shelf covering these topics:
"Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search)
First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers
For some early stuff on dependent types (also covered in the above), check out "Intuitionistic Type Theory" by Per Martin-Lof
"Computation and Reasoning: A Type Theory for Computer Science" by Zhaouhui Luo
"Type-Driven Development with Idris" by Edwin Brady
"Gentle Introduction to Dependent Types with Idris" by Boro Sitnikovski
"Types and Programming Languages" by Pierce
"Practical Foundations for Programming Languages" by Robert Harper (or any of his YouTube videos re/Type Theory)
"The Little Typer" by Friedman and Christiansen
"Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy" by David Corfield (just took this one to OBX North Carolina to enjoy on my beach vacation last week! Got some salt water in those pages. Also speaks to Category Theory.)
For Category Theory:
"The Joy of Abstraction" (2023) by Euginia Cheng
"Basic Category Theory for Computer Scientists" by Benjamin C. Pierce
"Conceptual Mathematics: A first introduction to categories" by Lawvere and Schanuel
"Categories for the Working Philosopher" by Landry
- PS: Type Driven Development with Idris is mentioned in the final notes. OP, I could not recommend it more!
- The book itself Type Driven Development with Idris is great too, it is the principal way I write code these days, by writing my types upfront then filling out the logic, and in some languages, the logic itself can be produced automatically via the filling of type holes. In other words, simply based on the types you provide, the compiler can guess the implementation of the function, somewhat like Copilot but guaranteed to be correct on a type level, even if not necessarily on a business logic level.
https://www.manning.com/books/type-driven-development-with-i...
- What's the state of Idris2 at this point? I really enjoyed Type Driven Development with Idris a few years ago.
- For dependent types? I'm really fond of Type Driven Development With Idris.
Related
2018–2025
Gentle Introduction to Dependent Types with Idris
1 recommend · 2
Types and Programming Languages
132 recommend · 321
Type theory and functional programming
2 recommend · 6
2011–2026
Software Foundations
58 recommend · 77
Domain-Driven Design
104 recommend · 252
The annotated C++ reference manual
2 recommend · 13
