- Paperback: 480 pages
- Publisher: Manning Publications; 1 edition (March 31, 2017)
- Language: English
- ISBN-10: 1617293024
- ISBN-13: 978-1617293023
- Product Dimensions: 7.3 x 0.9 x 9.2 inches
- Shipping Weight: 1.8 pounds (View shipping rates and policies)
- Average Customer Review: 7 customer reviews
- Amazon Best Sellers Rank: #266,677 in Books (See Top 100 in Books)
Enter your mobile number or email address below and we'll send you a link to download the free Kindle App. Then you can start reading Kindle books on your smartphone, tablet, or computer - no Kindle device required.
To get the free app, enter your mobile phone number.
Type-driven Development with Idris 1st Edition
Use the Amazon App to scan ISBNs and compare prices.
Garth Brooks: The Anthology Part 1 | Limited Edition
A great gift for country music fans, The Anthology Part 1 includes CDs containing the music of Garth's first five years, and behind-the-scenes photographs and stories never before made public. Learn more
Frequently bought together
Customers who bought this item also bought
From the Publisher
About this Book
Type-Driven Development with Idris is about making types work for you. Types are often seen as a tool for checking for errors, with the programmer writing a complete program first and using the type checker to detect errors. In type-driven development, you use types as a tool for constructing programs, and the type checker as your assistant to guide you to a complete and working program.
This book begins by describing what you can express with types; then, it introduces the core features of the Idris programming language. Finally, it describes some more-practical applications of type-driven development.
Who Should Read This Book
This book is aimed at developers who want to learn about the state of the art in using sophisticated type systems to help develop robust software. It aims to provide an accessible introduction to dependent types, and to show how modern type-based techniques can be applied to real-world problems.
Readers will ideally already be familiar with functional programming concepts such as closures and higher-order functions, although the book introduces these and other concepts as necessary. Knowledge of another functional programming language such as Haskell, OCaml, or Scala will be particularly helpful, though none is assumed.
About the Author
Edwin Brady leads the design and implementation of the Idris language. He is a Lecturer in Computer Science and regularly speaks at conferences.
Top customer reviews
There was a problem filtering reviews right now. Please try again later.
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.
This book is written by the author - well yes, all books are, but by the author of the programming language itself. And its a warm and friendly book!
Reviewing technical books is often very hard for me, I dont want to rewrite the book as a review, and filling a decent length review is rather tricky. This, the work is keeping the review short! I want to talk about so much, but honestly, you need to buy this book. Its worth it.
Very simple overview - Type driven means that certain types of code only have certain permissions - so the code that manages a users name and address could not corrupt or release their social security number, because it is simply the wrong type.
So security is less of an issue, because the entire platform is the security. Assuming that the code has been properly written, there cannot be security issues. Whereas with traditional languages, assuming the code is properly written, and well tested there probably wont be any security issues. unless someone sneaks something through that contact form, or through the comments block, or...
From a different perspective, you have an office full of chests of drawers. Each draw has a lock. Traditional programing will put a lock on the front door, but you may be able to sneak in through the window - once inside, each draw has a bolt, you can slide that to the side, and get in.
With Idris, if you get in through the door, and find the drawer you want to open, you need a key to open it. You cannot slide the contents down the back of the draw into the draw below, you cannot take a quick peek into the draw next to it, you can only look in your draw, and when you turn away, the draw will close and lock.
Oh, and if you try to break the window, you will find a brick wall behind it.
I find the authors method of writing very easy to read, nice friendly text, but the book accelerates quickly! You will be moving back and forth a lot to keep up unless you are very intelligent in these matters - which I like. I like a good book that makes me work! This is worth the work.
What the book doesn't really say, but is said through every line is we are looking at the future of programming here. Think of all the viruses, all the recent hacks, data locking, theft and fraud. With the adaptation of Idris, and its peers, these issues will be gone.
When you look at computer powered cars, security and more, this is becoming more important than ever.
Most recent customer reviews
Until I got the book I hadn't heard of IDRIS.Read more