Autres vendeurs sur Amazon
+ EUR 0,01 (livraison)
+ EUR 2,99 (livraison)
+ EUR 2,99 (livraison)
Type-driven Development with Idris (Anglais) Broché – 3 mai 2017
|Neuf à partir de||Occasion à partir de|
- Choisissez parmi 17 000 points de collecte en France
- Les membres du programme Amazon Prime bénéficient de livraison gratuites illimitées
- Trouvez votre point de collecte et ajoutez-le à votre carnet d’adresses
- Sélectionnez cette adresse lors de votre commande
Les clients ayant acheté cet article ont également acheté
Description du produit
Présentation de l'éditeur
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 typedriven
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.
KEY FEATURES• Written by the creator of Idris• Improve performance and accuracy of programs• Teaches Idris, a new type-driven development language• Hands-on code examples• Build real-world software
Written for programmers with knowledge of basic functional programming
ABOUT THE TECHNOLOGY
Type-driven development lets you write extensible code, create simple
specifications very early in development, and easily create mock
implementation for testing. In type-driven development, types become your
tools for constructing programs and, used appropriately, can show the
absence of errors.
Biographie de l'auteur
He is a Lecturer in Computer Science and regularly speaks at conferences.
Aucun appareil Kindle n'est requis. Téléchargez l'une des applis Kindle gratuites et commencez à lire les livres Kindle sur votre smartphone, tablette ou ordinateur.
Pour obtenir l'appli gratuite, saisissez votre numéro de téléphone mobile.
Détails sur le produit
Si vous vendez ce produit, souhaitez-vous suggérer des mises à jour par l'intermédiaire du support vendeur ?
|5 étoiles (0%)|
|4 étoiles (0%)|
|3 étoiles (0%)|
|2 étoiles (0%)|
|1 étoile (0%)|
Commentaires client les plus utiles sur Amazon.com
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.
Until I got the book I hadn't heard of IDRIS. As someone who spent 15 years using Object Oriented Programming and sworn it off, Clojure is my language of choice for most projects. I got this book, downloaded the tools and just started at it. I'll let you infer what you will.
Night one I came back from the gym around 10:00 PM. The next thing I knew the sun was coming up and I realized I was going to be late for work. I was so preoccupied with it that I took it to work to play with at lunch.
Note that it is a derivative of Haskell, which is a good or bad thing depending on one's perspective but I absolutely love this language. Love it isn't strong enough of a way to say it.
There's not much about it. If it's your 2nd language and you're really looking for work, it's probably too early for a demand to have developed. But is there any doubt in my mind that this language is well done and will make a big splash? None. Do I love it enough to give up Clojure? No. But I never thought I'd even consider another functional language and I've had a good 12 nights that I've stayed up all night learning it.
And let me point out, that's not b/c its hard. If you are a functional programmer, it's a very straightforward language and the book covers it very well. I've been through it a few times wishing there was more too it but that's not to say the author left anything out, it's just that exciting of a language and I want to learn it as well as I can. So much so that I have made a point of using it for several ad hoc projects at work (luckily I'm a Director so I can do that and everyone on the data science team believes in Functional Programming when we're not using R).
I'll leave you with a parting thought. When Agile first came out, the thought of writing code without unit tests seemed lazy and pathetic. That war was had and won in favor of writing unit tests. As functional programming became popular , serious discussions and arguments were had about the necessity of unit tests, were they worth the time or could you count on the language to produce 0 defect software or as close to it as possible without writing unit tests? It still feels weird not writing them but at this point I've found them to largely be a waste of time. That's b/c at first I wrote unit tests and in the entirety of the code base I've written (upwards of 30k lines) I've yet to write a test that would have caught anything.
There's a special feeling you get when your app compiles and you feel a tremendous sense of victory. If this language turns out to flop and is never embraced, I still feel like I grew tremendously as a developer from having spent the time i have with it and I can not imagine that it won't pick up speed and become very popular. Then again, Functional Programming still faces and uphill battle just b/c OOP is so engrained in the minds of many and people don't like change. Even if they do, giving up Unit Tests is a different subject but that's not the subject of this review or something the author really gets into so that's just my two cents