The book is fantastic. If you think this model is interesting, please consider trying Idris and reading the Idris book:<p><a href="https://www.manning.com/books/type-driven-development-with-idris" rel="nofollow">https://www.manning.com/books/type-driven-development-with-i...</a>
This book is a real joy to read. I got to peek at a draft at OPLSS 2017 and have been waiting impatiently for it to come out. The detailed, carefully worked examples one after another that this style of book is famous for is adapted beautifully to dependent type theory. Check it out! The code implementing the language in the book is here: <a href="https://github.com/the-little-typer/pie" rel="nofollow">https://github.com/the-little-typer/pie</a>
I'm going to order it right now. I highly recommend the little schemer and the seasoned schemer too! I have read all the titles (MLer and Java too) in the series and those are my favorites. The only one I have not finished is the reasoned schemer although I hope to try again in the future.
Several comments elaborate on the big gap between normal programming practice (e.g. structurally recursive algorithms) and the great difficulty of dependent typing those practices. Some of these comment on how dependent types are "just out of the lab".<p>This brings into focus a question I've had for a long time: Why this gap, and especially in this direction? E.g. in aerodynamics we had Bernoulli's principle for a couple of hundred years before we could build airplanes, which depend on it. In formal language theory we had lambda calculus, Turing's universality results, etc. decades before we had Lisp and Fortran.<p>We often see the difficulty of building a practice to exploit theory.<p>So it seems very strange to me that we are able to write / plug together literally world-spanning software systems -- which do have bugs but fact work correctly nearly all the time. But we can't easily well-type even simple algorithms with extremely well understood properties.<p>Why this huge gap, in this direction?
I can't tell if my question is off-topic or not, but..<p>Can anyone recommend a book (or whatever) that introduces the aspects of type theory relevant to a would-be language designer?
Source code of pie (used in the book) at <a href="https://github.com/the-little-typer/pie" rel="nofollow">https://github.com/the-little-typer/pie</a>
> An introduction to dependent types, demonstrating the most beautiful aspects, one step at a time.<p>Is there a companion book detailing the ugly downsides of dependent types and how to avoid them, one step at a time?
See related HN thread <<a href="https://news.ycombinator.com/item?id=18050706>" rel="nofollow">https://news.ycombinator.com/item?id=18050706></a>
Sad to say the book isn't on Library Genesis, so you'll have to drop $40 if you want the knowledge. <a href="http://libgen.io/search.php?req=little+typer" rel="nofollow">http://libgen.io/search.php?req=little+typer</a><p>Also Library Genesis is amazing: <a href="http://libgen.io/search.php?req=knuth" rel="nofollow">http://libgen.io/search.php?req=knuth</a><p>It's everything I dreamed of when I was a kid. I used to spend hours at the local library scouring through crummy "Learn C++ in 24 hours" type books.<p><a href="http://custodians.online/" rel="nofollow">http://custodians.online/</a> is worth a read too.