zilinc (4) [Avatar] Offline
I had an urge to see and buy this book, and I did. As a definite resource for learning and using Idris, I wanted to see more about how Idris works, rather than the very superficial introduction on functional programming. Thus things like what purity is, how (>>=) works etc. are really not what I wanted to spend money on. I don't think people use Idris as their first fp language anyway, so I'd imagine the readers of this book are all with at least intermediate level of knowledge of how fp works. So more constructively (as Idris), it'd great if the following are covered (I only searched the book for what I needed to know, e.g. syntax, etc. so not sure if they already appear in the book. apologies):
* limitations of Idris
* comparisons with other languages (Agda, Coq, LiquidHaskell, "Dependent" Haskell)
* how the compiler works (of course intro level should suffice for this book, as it's not a dev's book)
* more advanced/difficult examples and features, of a similar level to the "language extensions" section of Haskell users guide, Isabelle's Concrete semantics book
Maybe I'm after an improved version of the Idris reference from the very beginning, but I thought as a book it should be more complete, easier-to-follow, more accurate and trustworthy than online materials.

Thanks for your work on this great book. Please keep it going.
Edwin Brady (65) [Avatar] Offline
Thanks for the comments. I very much hope it's accurate and trustworthy, we've worked quite hard to make it so! Much of the things you're looking for, though, are discussed at some length elsewhere in academic papers about Idris and in various parts of the documentation. The book is more about the process of development, and showing how to go about writing programs with dependent types (hence the title being "Type-driven development with Idris" rather than, say, "Idris in Action".)

Also, a lot of the things that are described (e.g. (>>=) and purity) may be true of Haskell but are not necessarily true of other functional languages, and even then I think it's good to explain the Idris approach. Even when we talk of purity, for example, we mean something more in Idris than we do in Haskell.

Our experience has been that many people come to Idris from Scala, ML, F#, and various other backgrounds, so a lot of the earlier chapters are about making sure everyone is up to speed on the basics. If you have a Haskell background, you can probably work through them quite quickly then really start seeing what you can do with dependent types from Chapter 8 onwards, but if you don't, there should be enough there to get you going.
443179 (1) [Avatar] Offline
I'm not new to functional programming and I don't know what (>>=) is. I heard about Idris from a fellow Elm programmer.