Type-Driven Development with Idris (英語) ペーパーバック – 2017/4/7
Kindle 端末は必要ありません。無料 Kindle アプリのいずれかをダウンロードすると、スマートフォン、タブレットPCで Kindle 本をお読みいただけます。
Types are often seen as a tool for checking errors, with the programmer writing a complete program first and using the type checker to detect errors. And while tests are used to show presence of errors, they can only find errors that you explicitly test for. In type-driven development, types become your tools for constructing programs and, used appropriately, can show the absence of errors. And you can express precise relationships between data, your assumptions are explicit and checkable, and you can precisely state and verify properties. Type-driven development lets users write extensible code, create simple specifications very early in development, and easily create mock implementation for testing.
Type-Driven Development with Idris, written by the creator of Idris, teaches programmers how to improve the performance and accuracy of programs by taking advantage of a state-of-the-art type system. This book teaches readers using Idris, a language designed from the very beginning to support type-driven development. Readers learn how to manipulate types just like any other construct (numbers, strings, lists, etc.). This book teaches 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, readers will be able to develop robust and verified software in Idris and apply type-driven development methods to programming in other languages.
Purchase of the print book includes a free eBook in PDF, Kindle, and ePub formats from Manning Publications.
Edwin Brady leads the design and implementation of the Idris language. He is a Lecturer in Computer Science and regularly speaks at conferences.
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.