Edwin Brady

"I don't care how easy it is to write correct programs in a language, I care about how hard it is to write wrong ones." -- Nicoλas (@BeRewt as seen on Twitter))

If you are professional software developer in 2017, you're most probably developing systems using programming languages such as Java, C#, Python, Ruby, Objective-C, C, C++, PHP, and/or JavaScript. If you belong to a minority of professional software developers, you might be programming in Scala that has a much more advanced typing system and yields itself more easily to sophisticated functional programming idioms. And if you're a minority within minority, that belong to 1%, you might be even doing professional development using an advanced language such as Haskell. And in that case, you are already used to your compiler being a good friend, showing you errors before run-time, and guiding your design based on your types. For those people, "Type-Driven Development with Idris" is the next step. Not professionally of course, because you know, you're already a minority within a minority, so there's nothing beyond that. But in terms of seeing how advanced concepts such as dependently typed programming can even a small chance of being practical, this book is the perfect introduction. And the only one.

Why should you care? I can think of two broad answers to that question:

1- You already know the benefits of static and strong typing, and you are curious whether it is possible to go much beyond that. You have heard about Haskell, and you've even seen someone mentioning obscure languages such as Agda, or Coq, describing how it is possible to prove properties about functions and data, and automatically derive verified programs from those proofs, and you wonder whether you have the slightest chance of seeing such things in concrete action, rather than academic exercises confined to peer-reviewed journals.

2- Or, you've already playing with Haskell, even developed some complex software with Haskell (or did similar things in Scala with advanced type-level libraries), and seen its power, as well as some slightly verbose examples in Haskell where by using some language extensions it was possible to prove some properties at compile-time. You wonder if there's an easier way of doing these, and maybe even go beyond the simplest type-level computations without getting more convoluted code.

In both cases, the implicit assumption is that a) the more you can easily fix / prove at the compile time, the better, and b) the more the compiler can guide you refine things at type-level, therefore guiding you in the 'right' direction, the easier it'll be for you as a software developer. And that's because, another implicit assumption, you think that the only ethical way to go with building software-intensive solutions is by eliminate errors that can be eliminated before the system runs, that is, at design-time (probably because you're old enough to remember so much money, energy, and even lives lost because of software errors).

For the curious minds to delve into the depths of dependently-typed and type-drive programming, this book, written by the creator of Idris language, will be a gentle guide to the future of programming. The author starts with the basics, e.g. showing how to write functions that are guaranteed to return values such as vectors of a given length and type, and move forward to more complex examples such as how to create data types and functions so that they don't compile unless they comply with some protocols you have defined, and how to avoid to some difficult concurrency problems by using types.

In a sense, this is indeed a practical book, not only because many of the terms that might be unfamiliar for the reader is described in plain language, but also because getting started with Idris, and creating useful programs whose executables you can easily share with others is as straightforward as it can be, given the scarcity of resources dedicated to this brand new programming language. Even though the book is a gentle introduction, if you've been slightly exposed to exposed to Haskell, it'll be easier for you (and if you're not, in the recent years, very nice books for learning Haskell started to come out!). But I think any serious developer who've used a statically, strongly typed language professionally for a few years, can try and understand most of the examples in a few months of study.

Another nice aspect is that, the tooling for the language is not very bad, making playing with code examples easier: It is possible to interact with Idris compiler and interactive environment (REPL) via Vim, Emacs, and Atom. The author prefers the Atom editor, and if you accept to use that it'll be a more pleasant reading and studying experience for you, because throughout the text you'll always be presented with Atom editor's keyboard shortcuts for interacting with Idris, and refine your code, fill in the "holes" with the help of compiler, etc.

As a conclusion, I recommend this book to professional software developers who want to have good, solid taste of dependently-typed programming and the qualitative feel it leads to when trying type-driven programming, in no other practical book that I know, those things are demonstrated so explicitly. But of course, with all the praise, do not expect to put Idris into action immediately or even next year. Funny thing is, the author himself shows that most of the core ideas and even some implementations aren't new, some academic papers are more than 10 year old. But at least 10 years passed from them being written until such a book published by a popular programming book publisher, and it is only the first and minimum step until advanced languages such as Idris and advanced ideas such as dependently-typed programming become even an acceptable minority in the world of mainstream software development. Until then, you have your food for thought and enough material to dig in and experience for yourself the future of strongly, statically type-driven functional programming today.… (más)