I heard a great podcast interview recently with Edwin Brady. He was discussing his upcoming book Type-driven development With Idris. After listening to the podcast, I immediately picked up a copy of his book. Having now completed the book (well it’s a MEAP, so what’s finished so far), I’m finding Idris the language really intriguing.
I’ve always had a preference toward statically-typed languages. I just like the ability to specify type constraints and have some level of confidence of correctness in my programs before I run them.
Why Idris?
Idris looks to be the most modern language designed for general purpose use. It is based on some of the very latest programming language research. What better way to stay ahead of the curve than that?
It has many of the things you expect from a language out the gate including:
- A REPL
- A packaging system
- Multiple back-ends (C, Javascript, Java, LLVM)
- It looks to have an interop story by design; It has FFI (foreign-function interface) to C and Javascript, and can support others. There is a Java one as well, but not sure its current maturity level.
- An active community of enthusiasts
More motivation: I’ve been meaning to learn Haskell for a while now. Idris is heavily influenced by Haskell, but takes the type system even further. It has two killer features:
1. Types are a first class language construct. This means you can take types as arguments, return a type from a function, and create them on the fly! Idris supports a concept called dependent types. This means types can be defined not just in terms of other types, but in terms of values. This is a really powerful idea. It allows you to create constraints like “Take a vector of size 5 as an argument.” (Incidentally, the `Vect` type in the Idris standard library has such a length property encoded directly in the type.)
2. Idris also has a cool language feature called holes. Here you can get a program to compile before you have completed it, essentially adding a placeholder before you’ve implemented a part of it. Even better, Idris will help you by being able to show you the type definition expected in the location of the hole, and even auto-generate code based on the surrounding context in many situations, where it can be inferred.
I love the idea that you can encode expression invariants directly into types and they will be checked by the type system!
Another thing I like about Idris is that it has eager evaluation, as opposed to non-strict (or lazy) evaluation, such as a language like Haskell. While powerful, laziness can lead to all kinds of unexpected gotchas and can make reasoning about the performance or runtime characteristics of your program more difficult.
The gooey center
In an effort to better understand Idris, I’m currently reading another excellent book called Haskell Programming from first Principles. It’s an awesome book which does an excellent and comprehensive job explaining the critical building blocks of Haskell’s type system (which languages like Idris are built on). There’s a venn diagram in the book that looks something like this:
The idea is that Haskell increases the overlapping area between the two circles, as compared to other programming languages.
One of the big draws of Idris to me is the idea of even further increasing this overlap:
The extent to which you can encode properties of your program in the code and have them type checked is quite tantalizing, and I’ve decided it’s well worth any leaning curve involved. Idris is also approaching 1.0. This would indicate the language spec will be finalized and the implementation will be considered stable.
Setup
Despite the language being relatively new, setting up Idris is actually really straight-forward. These steps assume you are on OSX. First, you’ll need to get the Idris language binary, which is available pre-built for OSX.
Once the installation is done, you can confirm everything worked by opening a terminal and typing:
idris --version
You should see something like this:
0.12.1
Idris has editor support in a number of popular editors including: Atom, Emacs, and Vim. In this post, we’ll do the setup in Atom.
First, you’ll need to get the language-idris plugin for Atom. Once installed, you’ll need to make sure the plugin has detected your local Idris installation. The default installation directory is `/usr/local/bin/idris` and this is the default location the plugin looks in. You can verify this is your install location by typing the following at the command line:
which idris
Now create a new file called `hello.idr`, and put paste the following in:
module Main where main : IO (); main = putStrLn "Hello Idris!";
Now let’s open a REPL. You can do this with the command Cmd+Alt+Enter. This will have loaded your current Idris file. You can compile it like so:
:c hello
This will create an executable in the same directory as the source file. You can now execute the file at the command line:
> ./hello Hello Idris!
Nice. Ok, so you might be asking why the heck use the REPL is you’re just going to have to switch to the command-line to run this? Well, this program produces side effects, so you’re not really going to have a meaningful result until you actually run it.
Let’s go back to our `hello.idr` file and add a regular pure function:
Here is an example from the idris-demos repo on github. It’s meant to give just a basic idea of what’s possible in the language.
append : Vect n a -> Vect m a -> Vect (n + m) a append [] ys = ys append (x :: xs) ys = x :: append xs ys
This is a recursive function implemented using pattern matching. If this syntax looks foreign to you, it comes from the ML-world and languages like Haskell. While not required, learning Haskell can really help you understand the world of dependent-typing, and is the path I’m taking to better learn and understand this stuff at the moment.
And now let’s reload the file again. You can do this with `:r` or `:reload`. This reloads the current file. At the REPL let’s try this out:
*hello> append [1, 2] [3] [1, 2, 3] : Vect 3 Integer
Cool!
OK, another example from that repo. Let’s try something slightly more interesting:
vZipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c vZipWith f [] [] = [] vZipWith f (x :: xs) (y :: ys) = f x y :: vZipWith f xs ys
You might already be familiar with the idea of a zip function. `vZipWith` will take a function and a pair of vectors, and create a single vector where each element is the result of applying the function to the pair of elements in each vector at each step.
But this function has the additional constraint that all the vectors must be the same length; this is encoded in the `n` variable in the type signature, which has to be the same for both vector arguments.
Ok, let’s take this for a spin:
*hello> vZipWith plus [2] [3] [5] : Vect 1 Nat
Great. This makes sense. How about something that violates the constraint?
*hello> vZipWith plus [1, 2] [3]
(input):1:23:When checking argument xs to constructor Data.Vect.:::
Type mismatch between
Vect 0 a (Type of [])
and
Vect 1 a (Expected type)
Specfically:
Type mismatch between
0
and
1
Whoa! So this will happen when I try to call this function. Let’s assign the result to a variable.
myVec : Vect 1 Nat myVec = (vZipWith plus [1] [1])
Now in a REPL, reload with:
*hello> :r Type checking ./hello.idr
OK. Now’s let’s change the `myVec` variable’s type to this:
myVec : Vect 2 Nat myVec = (vZipWith plus [1] [1])
Now back to the REPL, let’s reload again:
*hello> :r
Type checking ./hello.idr
hello.idr:17:25:When checking right hand side of myVec with expected type
Vect 2 Nat
When checking argument xs to constructor Data.Vect.:::
Type mismatch between
Vect 0 a (Type of [])
and
Vect 1 Nat (Expected type)
Specifically:
Type mismatch between
0
and
1
Holes: Main.myVec
This won’t even compile! We are trying to assign a 1-element vector to a 2 element vector.
Mind = blown.
Theorems for free!
Philip Wadler’s very accessible Theorems for free! paper discusses the idea of getting theorems (a scary math word which essentially means a property you can assert by reasoning about other known properties or observations) from programming language types.
As a very simple example, take the function `fst` from the Idris standard library:
fst : (a, b) -> a
Think about what this does. Remember the function is pure since it has no reference to `IO` or similar in the type signature. Also, notice that we aren’t saying anything about the type variables `a` or `b`; they could be anything and the function cannot really do anything specific with `a` or `b` since it doesn’t know anything about them. (As a side note, this is generally true in any pure functional language such as Haskell; for a nice discussion of this in Haskell, see Real world Haskell). So there’s literally nothing a function with this type signature could do other than return `a`, regardless of what `a` is.
Idris allows us to take this to it’s logical conclusion, for example:
fiveIsFive : 5 = (2 * 1 + 3) fiveIsFive = Refl
In this case, the type specifies everything so it essentially stands as a property. The `Refl` refers to the type being reflexive, meaning one side equals the other. Obviously this particular example is contrived, but it gives you a sense of what is possible in the language.
Summary
Idris is not a language ready for production use, yet. Much of Idris is still pretty over my head right now, but it’s a very interesting language that I would like to begin playing around with and tracking closely. The funny thing is that getting into this led me towards finally deciding to take the deep dive into Haskell! In contrast, Haskell is used in production in more and more places and continues to get more accessible and palatable (library availability, tutorials, etc.) with every passing year. Plus there’s all the new languages so heavily influenced by it (Purescript, Elm, etc.).
Dependently-typed languages are definitely an emerging area of programming language research that could mean big things, but they are still in their infancy in terms of general purpose use outside of academia. I’ve finally decided that in the meantime, I need to get myself to the next level of type safety and correctness and get some serious Haskell under my belt!
References
* Type-driven development With Idris
* Haskell Programming from first Principles
* idris-lang.org
* Real World Haskell