Type-driven Development with Idris
by Edwin Brady · first published 2017
83% recommend17% neutral
Why HN recommends it
A practical introduction to dependent types: write the types first, then fill in the logic with compiler help. Suits programmers new to dependent typing, even without Haskell, and offers ideas for other languages.
Summarised by Claude from recommending comments
Affiliate links. As an Amazon Associate I earn from qualifying purchases.
Mentions per year
What Hacker News says
Related books
2008–2025Basic category theory for computer scientists
Benjamin C. Pierce
Recommended by 12 · mentioned by 1412 recommend · 14 mention12 recommend · 1412 recommend
Software Foundations
Benjamin C. Pierce
Recommended by 58 · mentioned by 6058 recommend · 60 mention58 recommend · 6058 recommend
2008–2021Network Algorithmics,
George Varghese
Recommended by 8 · mentioned by 98 recommend · 9 mention8 recommend · 98 recommend
2013–2026Practical Foundations for Programming Languages
Robert Harper
Recommended by 17 · mentioned by 2717 recommend · 27 mention17 recommend · 2717 recommend
2016–2026Computer Age Statistical Inference
Bradley Efron, Trevor Hastie
Recommended by 14 · mentioned by 1714 recommend · 17 mention14 recommend · 1714 recommend
2016–2023Hands-On Machine Learning with Scikit-Learn and TensorFlow
Aurélien Géron
Recommended by 16 · mentioned by 1816 recommend · 18 mention16 recommend · 1816 recommend
2008–2025More programming pearls
Jon Louis Bentley
Recommended by 12 · mentioned by 1512 recommend · 15 mention12 recommend · 1512 recommend
The effective engineer
Edmond Lau
Recommended by 19 · mentioned by 2519 recommend · 25 mention19 recommend · 2519 recommend
Type-Driven Development with Idris: https://www.manning.com/books/type-driven-development-with-i...
on “Ask HN: CS and programming books of 2017” ↗I always thought this kind of thing was abstruse and impractical until I read Type-Driven Development with Idris[0], which made basic dependent type examples--like those demonstrated in the posted article--completely straightforward. Turns out that this kind of thing isn't actually that hard with the right language…
on “Basic Type-Level Programming in Haskell” ↗On the contrary, I’d recommend to start with Idris instead. The design of the language is globally better and way more coherent. It fixes a lot of Haskell “mistakes”. Check out “Type-Driven Development with Idris” by Edwin Brady himself. The book is truly amazing.
on “A game in a pure language (part 1): introduction and problems with Idris” ↗…[1] Lectures on the Curry-Howard Isomorphism[2] is my favorite (graduate-level) introduction to type theory and the lambda calculus, including the “lambda cube” and pure type systems. Finally, while Type-Driven Development With Idris[3] is not at all “theoretical,” it is still an excellent introduction to dependent types and the idea of proof-as-program. It’s also the only book about a specific programming language I’ve ever read…
on “Homotopy Type Theory (2012) [pdf]” ↗Type-driven development with Idris (https://www.manning.com/books/type-driven-development-with-i...). It was a real eye-opener of what types can do.
on “Ask HN: What's the best computer science book you've read recently?” ↗what if that something must be between zero and one? A type can't tell you that. Actually, it can, using dependent types :) I'm a Python fan, but Type-Driven Development with Idris has been a very interesting read.
on “Yes, Python is Slow, and I Don’t Care” ↗I suggest reading Type-Driven Development with Idris by Edwin Brady. I don't think you have enough experience writing Haskell to understand the outcome of type driven development. In Haskell you start by defining your domain as types, and constrain those…
on “Why I love Common Lisp and hate Java (2012)” ↗Definitely give Idris a go. I'm working through the book Type-Driven Development with Idris [1] by Edwin Brady, the author of Idris, and I'm having a ton of fun with it. Idris is a lot more practical than I thought. It fixes some annoyances I had with Haskell, such as record naming (Idris lets…
on “Dependent Haskell Is the Future (2018)” ↗…that in a book. Enjoyable to read. Parallel and Concurrent Programming in Haskell by Simon Marlow Probably a must-read if you're into Haskell; probably too esoteric if you're not... Well written. Type-Driven Development with Idris by Edwin Brady Describes a programming language similar to Haskell, but strict by default and with dependent types designed-in from the start. Also describes techniques for leveraging the type system…
on “Most tech content is bullshit” ↗Dependently typed languages may fit what you're asking for. See Idris and the book Type-Driven Development with Idris for an example of encoding critical information into the type system. Beyond that, see SPARK where you're limited to a provable subset of the Ada language (the subset has been extended with each version)…
on “How Did Software Get So Reliable Without Proof? (1996) [pdf]” ↗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…
on “Idris: A Language for Type-Driven Development” ↗I have found Type-Driven Development with Idris [1] is a nice introduction into verifiable programming. The book starts with basic functional programming (Idris is how a strict Haskell could look) and gradually adds dependent types and working with…
on “A formalization of category theory in Coq” ↗Check Idris (https://www.idris-lang.org/) and if you have a chance, work through the Idris book, Type Driven Development with Idris (https://www.manning.com/books/type-driven-development-with-i...).
on ““What next?”” ↗…space of possibilities to a more manageable level to ensure that your testing can be more targeted. To see this pushed to the extreme, and to have a glimpse of the future, check out Edwin Brady's book "Type Driven Development with Idris": https://www.manning.com/books/type-driven-development-with-i... - I don't expect this style of programming to become the norm until at least another several years, but it essentially allows you to push…
on “Sick of Ruby, dynamic typing, side effects, and object-orientation (2014)” ↗…(http://adam.chlipala.net/cpdt/). If you are more interested in programming, consider trying Idris (http://idris-lang.org/). Edwin Brady, the language designer, wrote a great book that I would recommend called Type-Driven Development with Idris (https://www.manning.com/books/type-driven-development-with-i...).
on “Finding bugs in Haskell code by proving it” ↗