What do you think?
Rate this book
Type-Driven Development with Idris
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 from the very beginning to support type-driven development. In this book, you’ll learn how to manipulate types just like any other construct (numbers, strings, lists, etc.). You’ll see how to use type-driven development to build real-world software, as well as how to handle side-effects, state and concurrency, and interoperating with existing systems. By the end of this book, you will be able to develop robust and verified software in Idris and apply type-driven development methods to programming in other languages.
453 pages, Paperback
First published March 22, 2017
55 people are currently reading
384 people want to read
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 - 8 of 8 reviews
June 5, 2017
"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.
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.
November 28, 2017
Wow. This book has opened my eyes to the power of dependent types: types that can have values associated with them, such as a `Vect 5`, a list of 5 elements.
Edwin Brady has done a great job here explaining what Idris can do and how it can be used to help you write correct programs. (He's the creator of Idris, so that's not too surprising.) This requires a shift in thinking, which is what Brady means by type-driven development. In Idris, you can first write the types of your functions, leaving holes that the compiler can help you fill in by providing types.
This is well worth a read, even if you'll never use Idris, because it'll expand your view of what's possible in a type system. The only downside is that it may increase your dissatisfaction with whatever language you use.
Edwin Brady has done a great job here explaining what Idris can do and how it can be used to help you write correct programs. (He's the creator of Idris, so that's not too surprising.) This requires a shift in thinking, which is what Brady means by type-driven development. In Idris, you can first write the types of your functions, leaving holes that the compiler can help you fill in by providing types.
This is well worth a read, even if you'll never use Idris, because it'll expand your view of what's possible in a type system. The only downside is that it may increase your dissatisfaction with whatever language you use.
November 30, 2017
I've finally decided to take a plunge into dependent typing and Edwin Brady's Type-Driven Development in Idris seemed like a perfect start.
First of all, let me say what the book is not. It's not a book on on dependent type theory or a hardcore book on software verification. The book is an introduction to Idris with elements of functional programming patterns, dependent typing, and type theory. The major goal seems to be tackling practical and error prone programming problems: working with i/o, potentially infinite data, concurrent and parallel programming, verifying state transitions in state machines.
Pedagogically, the author makes some interesting choices: the book stats of with an introduction the language: defining types, data and functions then goes to working with i/o, typeclasses and working with proofs. The book concludes with several practical applications in part 3: Idris and the Real World. The author spends almost no time defining Monads, Functors or other functional design patters, yet they are used extensively. Similarly, the theory behind dependent types is almost totally omitted.
For me, the difficultly ramped up in the chapters concentrating on proving properties in types and was pretty much constant everywhere else. I have a hard time telling who's the target reader of the book, though. People experienced with functional programming might find the book boring (or at least not challenging), while people with no exposure to it might be lost. Except for the proofs, the exercises were quite easy - more "repetition" than any real problem.
The "Type-Driven Development" in the title alludes to the other TDD: Test Driven Development. Instead of the "write a test, check that it fails, and code until tests pass" loop the author proposes a "type, define, refine" one. When you're first learning about Idris's interactive features, this seems fine but becomes gimmicky very fast. I've caught myself several times just skipping over sections of "type, define, refine" to just get it over with. In many places the whole process seemed very trivial.
I had some other minor peeves when reading the book: I didn't quite like how the author conflated parallelism and concurrency, or how IO and State are called "side-effecting". The book also had a few typographical errors but all in all it seems very solid.
I usually reserve 5 stars for books that are mind-expanding, but sadly, Type Driven Development in Idris isn't one of them. It is still a very good book, though! Highly recommended.
First of all, let me say what the book is not. It's not a book on on dependent type theory or a hardcore book on software verification. The book is an introduction to Idris with elements of functional programming patterns, dependent typing, and type theory. The major goal seems to be tackling practical and error prone programming problems: working with i/o, potentially infinite data, concurrent and parallel programming, verifying state transitions in state machines.
Pedagogically, the author makes some interesting choices: the book stats of with an introduction the language: defining types, data and functions then goes to working with i/o, typeclasses and working with proofs. The book concludes with several practical applications in part 3: Idris and the Real World. The author spends almost no time defining Monads, Functors or other functional design patters, yet they are used extensively. Similarly, the theory behind dependent types is almost totally omitted.
For me, the difficultly ramped up in the chapters concentrating on proving properties in types and was pretty much constant everywhere else. I have a hard time telling who's the target reader of the book, though. People experienced with functional programming might find the book boring (or at least not challenging), while people with no exposure to it might be lost. Except for the proofs, the exercises were quite easy - more "repetition" than any real problem.
The "Type-Driven Development" in the title alludes to the other TDD: Test Driven Development. Instead of the "write a test, check that it fails, and code until tests pass" loop the author proposes a "type, define, refine" one. When you're first learning about Idris's interactive features, this seems fine but becomes gimmicky very fast. I've caught myself several times just skipping over sections of "type, define, refine" to just get it over with. In many places the whole process seemed very trivial.
I had some other minor peeves when reading the book: I didn't quite like how the author conflated parallelism and concurrency, or how IO and State are called "side-effecting". The book also had a few typographical errors but all in all it seems very solid.
I usually reserve 5 stars for books that are mind-expanding, but sadly, Type Driven Development in Idris isn't one of them. It is still a very good book, though! Highly recommended.
October 23, 2021
Gateway drug to Haskell and a new take on programming. As some one who loves duck types languages I expected to hate it. Glad to be proven wrong.
June 23, 2020
This book was a very good read.
The author, none other than Idris's creator himself, has a remarkably neat writing style, and a great sense of when to fill in exercises which are quite reasonable and most surely add to the chapters.
Probably this book's biggest selling point is how down-to-earth it is, in which pretty much there aren't any non-real-world examples given, which make it very accessible, a quite surprising statement since dependent typing and type theory aren't really the most obvious topics out there.
The author, none other than Idris's creator himself, has a remarkably neat writing style, and a great sense of when to fill in exercises which are quite reasonable and most surely add to the chapters.
Probably this book's biggest selling point is how down-to-earth it is, in which pretty much there aren't any non-real-world examples given, which make it very accessible, a quite surprising statement since dependent typing and type theory aren't really the most obvious topics out there.
June 25, 2018
Perhaps the best introduction both to Idris and to dependently-typed programming in general. It's not too hardcore to explicitly include notions of math stuff like the Curry-Howard isomorphism or other aspects of type theory and logic, but this book will surely get you up to speed with writing dependently typed, statically verified code.
July 3, 2017
The book itself was well written, but there are numerous errors in the example code in the book that causes type-check errors, and this made it very frustrating to follow along as the book suggests.
May 19, 2021
A dependent types book with a very practical focus. It doesn't enter into great detail on the mathematics but it's a good intro to the topic.
Displaying 1 - 8 of 8 reviews