Anybody recommend this?
I’ve spent some time learning a bit of Idris for fun. To set expectations, if you do learn it, learn it for fun not for profit. I don’t mean that it’s a small, new language, but rather that the cool features it has I have struggled a bit to find great uses for them. Maybe it just takes a big mind shift, I don’t know. To compare, a type system that Haskell or Ocaml or SML has, has much clearer wins for my day-to-day life. I want to use these languages at work and argue for it. The type system of Idris on the other hand has powerful features but I haven’t really figured out how to apply them to the use-cases I have. But, that means when I use it, it’s purely for the joy of doing so, and that is its own reward.
As for the book, I don’t know, but I’ll probably grab it to hopefully help with what I said above.
the cool features it has I have struggled a bit to find great uses for them. Maybe it just takes a big mind shift
There are plenty of good uses for dependent types. Here’s what I believe to be an important example. We generally want parallelism in our language to be deterministic. Nondeterminism leads to annoying heisenbugs, security concerns via side channel attacks, and can also break language guarantees like referential transparency or type safety. There are a number of approaches to ensuring determinacy, such as Determinator (which modifies the OS communication primitives), CoreDet (which modifies the scheduler), or DPJ, which uses a type and effect system.
More recently there is LVish which allows threads to communicate only with data types that form a lattice. This is an expressive approach but it is difficult to extend with new data types, because we must trust the programmer that what they provided indeed forms a lattice. With dependent types you can enforce these properties through the type system.
That being said, adding dependent types to a language involves a lot of tradeoffs that I think are simply unacceptable for general purpose programming. Recursion must be limited if you want the types to mean anything (and in the parallel example we do), type inference is weakened, and writing proof terms is a huge pain in the ass. I don’t think dependent types are useful enough to make these tradeoffs, and would rather use them in a special purpose language like Coq.
Yeah… I tried to learn it for fun and got stuck. I intend to go back.
On my most recent try, somehow I wound up doing a “fun, easy, simple” project for which I needed to implement row types. Which I don’t even understand in any other language either.
I advise learning it with simpler things first. :)
I’ll first say I don’t do functional programming or formal work. Ive read on a ton of it to track capabilities of field. I also read debates by veterans on places like Lambda the Ultimate. The point they all say of it is verification of properties of your programs instead of say productivity like some language features. Dependeng types supposedly are easier than theorem provers to do this.
The arguments by each side boiled down to one of two positions: (a) general purpose languages with dependent types are easier to point it might increase adoption of formal-like methods; (b) verifying serious programs and properties with dependent types is about as hard as other methods like Coq so might as well avoid them in favor of stuff like Coq.
My barely-informed opinion leans toward the latter as both ATS and Idris code + proofs of anything complex looks like as much gibberish to me as similar stuff I see in Coq papers. The guides had a lot of similar material in them, too. So, I was leaning on it being better just to learn the real stuff.
If you do want to learn dependent types, Chlipala has a book on it and has done lots of useful verifications.
Far as what cmm is saying, Brady et al have a nice paper on checking resource use:
(a) general purpose languages with dependent types are easier to point it might increase adoption of formal-like methods; (b) verifying serious programs and properties with dependent types is about as hard as other methods like Coq so might as well avoid them in favor of stuff like Coq.
Coq isn’t a different method than Dependent types, it’s a different underlying formalisation to Idris', but they are both dependently-typed programming languages, and proving something in Idris produces something exactly the same as proving something in Coq.
They do, however, differ in two main ways.
I’ve not used Idris in anger but I have used ATS. I find having the ability to prove things in the language itself more useful than using an external system like Coq. When debugging an ATS program I’ll often start with adding dependent types and some proofs to narrow things down. These then stay within the program and the additional checks ensure safety if anyone changes it in the future. With an external checker like Coq I could write proofs in that, translate to my actual language but then if people make changes they must know to re-check assumptions in Coq. Maybe they will, probably they won’t.
I’d say it’s just as useful to learn the capabilities within ATS and Idris to learn how such things help in development of production code and then followup with Coq, etc to get a deeper dive in systems that are oriented solely around proofs and dependant types. You can then apply what you learn there to the programs being written in ATS, Idris, etc.
One could turn your argument around that “Real World” applications Coq tend to be full of complex stuff that looks like nothing to do with the application being written. Might as well program in ATS or Idris where you can have your program structured like you’d write code normally and add the complex gibberish looking stuff later as needed.
That said, if you learn Coq first, or ATS or Idris first, it doesn’t really matter - it’s still an interesting field to learn and whatever one gets you interested enough to stick with it is really what matters.
Yes, I think it’s a great book. Not only is it a good resource for learning Idris but it also goes through how to interactively write programs guided by types and the Idris REPL.
This approach to development reminds me of “Programming in the Debugger” approaches used in Smalltalk and Self. In those languages you define a function but leave parts unimplemented, When you run and test it the debugger will appear for the unimplemented portions. You then implement that functionality while in the debugger and resume the program execution where it was. In this way you interactively build your program while it runs.
An approach demonstrated in the book for Idris is to define your types and let the compiler help you interactively build the implementation as it typechecks. You can leave ‘holes’ in your program that the type checker identifies and helps you determine what should go in there. You can also leave ‘holes’ in your type definitions and be guided towards what the correct types should be. For this alone I found the book worth reading.
This book has good coverage of dependant types for programming with Idris and a useful resources for practical examples of dependent type usage. The authors writing style is clear and easy to follow with lots of examples.
I can’t view Twitter where I am. But I’m a huge fan of Idris' design and I think he’s the language author? Which doesn’t always lead to the best language books, but one can hope; in any case this is probably the first proper Idris book.
Yes, Edwin Brady is the author of Idris itself, and this is the first book on Idris (though there have been books on dependent types before).