It’s a new year, so I figured that it’s time to dip my toes in a new language. This time, I’ve decided to start poking at Idris a bit to see what I can learn from it. While I doubt I will be focusing on the language, I still feel that there is a lot that I can learn from it that might become useful if const generics land in stable Rust. Besides, learning how to write compiler-verified programs seemed like fun.
In order to learn more about the language, I needed a good place to start, so I poked around the Idris subreddit and found the book Type-Driven Development with Idris. Thus, this post will primarily be about my experience with the book. Apologies if this seems a bit rambly, but I guess it’s a bit of a brain dump.
About the book
The book is laid out in 3 major sections, where the first two sections introduce you to Idris and its features and the last section talks about Idris’ applications in “Real-world” scenarios. All of the chapters up to the final two contain multiple exercises for readers to try as well. As one might guess, there is heavy emphasis on the usage of dependent types to design precise data and function types. One of the major themes of the book is “Type, Define, Refine”, which is prevalent in every chapter of the book. The idea is that programmers should start by writing out type signatures for their functions (Type). Next they should define their function, using the type signature to guide them (Define). At this point, the programmer should edit their type signature and function definition as needed (Refine). Interestingly, there is very little mention of testing in the book, likely because precise data types can help guarantee that certain properties of the program will hold. I imagine that this likely obsoletes property-based testing, but I’m still a bit leery about not writing unit tests in general. After all, designing precise data types only covers the cases that you manage to come up with while working on the design. Random testing could still help bring attention to other cases you might miss, so I’m hesitant about putting all of my eggs in the verification basket.
The book also emphasizes using the Idris interactive development tools in the Atom text editor. These tools can be used to save time writing out boilerplate, such as when pattern matching or creating a function definition from the type signature, and also help with debugging. Idris features typed holes, which can be used to denote code that has not yet been implemented yet. Using the interactive tools, you can inspect a hole and see what type of value it is expecting, as well as which variables are in scope along with their types. Using the proof search shortcut, you can even automatically implement certain function bodies if the types are precise enough.
The earlier chapters of the book cover basic language features, like algebraic data types, monadic do notation, and typeclasses (interfaces in Idris). If you are already familiar with other statically typed functional languages, such as Haskell, most of this content is old hat, but I think that it is still worth briefly covering just so that you can familiarize yourself with the syntax differences. Interfaces also work slightly differently in Idris than typeclasses do in Haskell.
Some of the more Idris specific features covered by the book include the termination checker and views. While determining if an arbitrary program will terminate is undecidable, Idris will try to make a conservative guess about which programs will terminate. For example, Idris recognizes that structurally recursive programs are guaranteed to terminate. This is important for guaranteeing that functions return a value of the correct type and will not infinitely loop. Views in Idris are used to enable different formats when pattern matching. For example, case splitting on a List usually results in [] and x :: xs as the two cases. However, using views, you can change the case splitting behaviour to produce [] and xs ++ [x] as the two cases instead, allowing you to traverse the list in reverse order.
Since Idris supports dependent types, like many other dependently typed languages, it also supports equality types. For example, the type 2 == 2 is inhabited by the value Refl while types like 2 == 3 are not inhabited at all. Thus, you cannot construct a proof that 2 is equal to 3, but you can construct a proof that 2 is equal to 2. This turns out to be pretty useful for working with Dec, which is a wrapper for indicating that a property is decidable. Similar to the GDP technique I talked about in my November post, you can use this to prove that certain properties hold so that you don’t have to return a Maybe (Maybe in Idris/Haskell is the same as Option in Rust). Later in the book, Idris’ dependent types are also used to create type-level state machines, which allow us to specify pre-conditions and post-conditions on functions to describe valid state transitions, similar to the typestate pattern used in Rust.
One of the more interesting examples presented at the end of the book is creating a Process API that allows one to write concurrent programs that are guaranteed not to deadlock or encounter race conditions. Writing the API to begin with requires careful planning and implementation to ensure that API users can’t use the API to create deadlocks or race conditions. This isn’t too different how most APIs prevent users from misusing them, but it’s still pretty interesting to see how it’s done using dependent types. While many APIs written in other languages would probably throw exceptions to signal that you’ve done something bad at runtime, Idris has the power to prevent these same issues at compile time.
Overall thoughts
I was pleasantly surprised by how well written this book is. It answered a lot of questions I had about dependent types and also gave me a much better understanding of why termination is such a desirable property for Idris programs. One thing I noticed is that the end of the book kind of felt a little rushed, since there were no exercises to do and the last example printed the wrong result. The mistake was simply caused by the order of two parameters being swapped, which was pretty easy to fix, but it also did not account for Windows users, since the example prints the wrong results for files that contain carriage returns. That being said, it’s still a very good introduction to FP and also dependent types and I would highly recommend it to anyone interested in writing compiler verified programs.
As for Idris itself, I think that the language is quite pleasant to write code in. I like being able to precisely define my data types and the interactive tools make programming feel very quick. The compiler error messages can leave something to be desired, especially compared to Rust’s error messages, which usually leads to me deleting code and adding holes in various locations just to try and figure out where the type mismatch is occurring. I’ve also noticed that Idris can fairly slow in some scenarios. I tried writing a little permutation searching algorithm in both Idris and Haskell and the Haskell version ended up being 8.5x faster than the Idris code, even after marking the return type as Lazy in Idris. I’m not sure why exactly this is, but it certainly makes me a bit uneasy about picking up Idris. Idris’ ecosystem is also severely under-developed at the moment, though that is to be expected with a new and experimental language. For now, I think I will be sticking to Rust for general development and using Idris for those problems where I could use the extra power of its type system.