This week on #PLTalk, @jeanqasaur invited Edwin Brady to speak about his work on the Idris programming language. As always, a recording of the stream is available for the next few days.

Idris is a functional programming language with dependent types. This means that types are first-class objects, and can depend on values. The canonical example is of a vector type that specifies its size. A function can specify that it takes two such vectors, requiring that they share the same length: a fact that will be proven to hold at compile-time.

An online REPL is available if you'd like to give the language a try.

Quantitative Type Theory

A lot of Edwin's recent work has been on Idris 2, a "mostly backwards compatible" rework of the language, built on Quantitative Type Theory. This means that every variable in Idris 2 also has a quantity associated with it: either 0, 1, or unrestricted.

If the quantity is 0, that variable is erased at runtime. If it is 1, that variable is used exactly once. Lastly, if the quantity is unrestricted, the variable behaviors like you would expect in most other languages, and it can be used as many or as few times as needed.

If this reminds you of the way Rust's borrow-check works, you wouldn't be wrong in drawing a connection! Rust's type system implements what's known as affine types: a close relative of linear types where a resource can either be discarded, or used exactly once.

Idris' use of QTT allows for type erasure, linearity, and more traditional programming models to all coexist in a single language. This flexibility gives Idris a lot of expressive power, by enabling complex use cases like modeling resource usage protocols. We ran out of time for the full demo, but Edwin briefly showed off how session types can be used in Idris, so that protocol specifications can be used during type-checking to verify that an implementation conforms to a given specification.

The official docs can do a better job than me of demonstrating what QTT brings to Idris. And as a bonus, here's Edwin teaching QTT using a can of beer.

Type-Driven Development

Another big theme of the stream was demonstrating what Edwin calls type-driven development. In Edwin's words, this is "an approach to coding that embraces types as the foundation of your code - essentially as built-in documentation your compiler can use to check data relationships and other assumptions."

In particular, Edwin discussed the use of holes to facilitate both exploring a program, and automatically synthesizing functions and parts of functions. The general idea is that you're able to write a partial program, with a "hole" in the missing piece. You can then query the compiler for the type of the hole, along with the types of the variables in scope.

Combined with the quantities from QTT, this can often reduce the possible number of implementations for that hole to the point where they can either be manually enumerated through, or automatically inferred through program synthesis. It was a very similar idea to the research Nadia Polikarpova shared with us a few weeks ago.

The most exciting of these demonstrations was the automatic synthesis of a function for uncompressing run-length encoded lists. It sounded like this was an active area of research for Edwin, and he expressed interest in using these capabilities, alongside session types, to synthesis clients and servers for the sorts of resource protocols I mentioned earlier.

Overall it was a very exciting stream, and I'm thankful to Edwin for taking the time to walk us through everything in as much detail as he did! I've always been a fan of Idris, but I didn't realize just much it was advancing the state of the art in programming languages, beyond just broadening the appeal of dependent types.

Join next week at 3pm PDT for a conversation with Jeff Bezanson, the creator of Julia.

- Quinn

Miscellaneous Links

Epigram - An earlier dependently typed language that heavily influenced Idris.

Language Strangeness Budget - The idea that a programming language needs to be weird enough to offer something new over other languages, but not so weird that it scares people away from learning it.

The Future of Mathematics? - A talk on using the dependently typed Lean Theorem Prover to formalize mathematics.

Hazel: A Live Functional Programming Environment with Typed Holes - A talk on another language built around the idea of using holes to drive the exploration and development of a program.

Elba - The incredibly named Idris package manager.

Idris Quine Generator - A quine generator in Idris.

Idris Politeness Monad - An INTERCAL inspired monad that requires politeness -- but not too much politeness -- from the programmer.