Review: Type-Driven Development with Idris

By Alex Beal
April 2, 2017

Type-Driven Development with Idris is out. I’ve been keeping an eye on it through Manning’s early access program, and it’s become one of my favorite books on programming. It’s special because it’s not just an Idris tutorial. Instead, it uses Idris as a medium for developing a vision of what programming could look like–a vision where developers embrace powerful type systems as a tool for improving the robustness of their programs. In this way, it’s similar to Functional Programming in Scala, where Scala is used as a medium for introducing a certain style of functional programming. Yes, FP in Scala will teach you Scala and TDD with Idris will teach you Idris, but the biggest insight is not the language itself. The magic is in seeing how leveraging dependent types can improve the development process. Best of all, Edwin Brady demonstrates this in a no nonsense way, explaining concepts clearly with realistic examples, and skipping the academic jargon.

So what are dependent types? I’ll let the book speak for itself1:

In Idris, types are a first-class language construct. Types can be manipulated, used, passed as arguments to functions and returned from functions just like any other value such as numbers, strings, or lists. This is a simple but powerful idea, which allows:

If you’re already familiar with Haskell, what you’ll find is a language with many of the same tools, but also a whole new realm of expressivity. What do I mean by that? Idris will let you express the same concepts (and more) at the type level without the acrobatics. Conor McBride said it best in his article Epigram: Practical Programming with Dependent Types. After a convoluted Haskell example, McBride writes2:

Programming with these ‘fake’ dependent types is an entertaining challenge, but let’s be clear: these techniques are cleverly dreadful, rather than dreadfully clever. Hideously complex dependent types certainly exist, but they express basic properties like size in a straightforward way—why should the length of a list be anything less ordinary than a number?

In other words, concepts that require contortions to express in Haskell melt away when types become first class. It’s much easier to express the length of a list at the type level, if types are allowed to contain natural numbers.

So who should read this book? Anyone with an interest in typed functional programming, but some experience with a language like Haskell is recommended. Despite Brady’s best efforts, I think those without some background in Haskell, ML, or Scala (using libraries like Cats or Scalaz) will find this book challenging. On the other hand, experienced Haskellers will find this book to be a breath of fresh air. It has certainly gotten me excited about the future of programming.

  1. Type-Driven Development with Idris by Edwin Brady. MEAP v12. p 2.↩︎

  2. Type-Driven Development with Idris by Conor McBride. p 3.↩︎