The mainline branch of Idris now has support for source location reflection. This means that Idris code can be informed about which line and column of which file it occurs on. In this post, I’ll walk you through how this can be used for implementing programmer tools, such as a facility similar to Haskell’s error function. Then, I’ll briefly discuss how the feature is implemented and the implications for referential transparency and claims of purity.

Note that I’m not claiming any major innovation here – this blog post exists only to explain a feature that I took from scala-virtualized and implemented in Idris.

Idris supports semantic highlighting of compiler output. In this post, I’ll sketch what the feature brings users, why it’s interesting, what inspired it, and how it’s implemented in the Idris compiler. Rather than spending a bunch of time describing a series of screenshots, here’s a quick video of it in action, inside of idris-mode for Emacs:

I just finished a submission to IFL 2014. It’s a paper about Idris’s quasiquotations mechanism, which allow the use of high-level Idris syntax to describe low-level reflected terms, with the ability to escape from quotation in chosen areas and intentionally control the details of the representation. This is very much inspired by Lisp quasiquotation.

I’m a cohost of a new pocast on type theory, The Type Theory Podcast. We just posted our first episode: an interview with Peter Dybjer on types and testing.

As one of the two primary authors of idris-mode, I’ve had to learn a fair bit about implementing Emacs modes. While I’m far from an expert on the subject, I do think that I’ve picked up a few ideas that are useful. There are already a number of good tutorials about the very basics, such as define-derived-mode, font-lock, and Emacs packages. What I haven’t been able to find is an answer to the question “what’s next?”. You can view this post as a kind of checklist for useful things to add to your mode.

I won’t go into great detail about how to do all of these things, because the documentation is typically quite good. The real problem is learning that there is documentation to be read!

I’ve just written a new tutorial on bidirectional typing rules. It’s available from my tutorials page. The PDF can also be downloaded directly.

In case you’re interested in programming languages and you’re working from Peter Sestoft’s book Programming Language Concepts, I’ve just posted some supplementary materials to my ITU page. It consists of a tutorial for converting from regular expressions to discrete finite automata via NFAs and a tutorial on constructing typing derivations in the particular miniature ML-like language used in the book.

You can find them on my tutorials page.

I recently needed to use Scalacheck with a milestone release of the compiler, and it took me a little while to wrap my head around the infrastructure. To preserve the steps for prosperity, I’m documenting them here, as I couldn’t find it described anywhere.

When you add library dependencies in your project’s SBT configuration, it will find the code by first looking in your local Ivy repository, then in any remote repositories that are configured. In other words, even if you don’t have access to the remote repositories, you can still put libraries in your local repository to be found by SBT.

Libraries such as Scalacheck that are intended to be used with multiple versions of Scala will typically use the crossScalaVersions setting to build against multiple compiler versions. The workflow to get a library working is, then:

1. Get ahold of the source code to the library

2. In build.sbt, find the crossScalaVersions setting. Add the desired version of Scala.

3. Run sbt. At the command line, type + test. This will compile the project for each configured version of Scala and run the tests.

4. Assuming the project passes, run + publish-local to push the compiled version

Now, the library will be available in your other projects.

If you try to use Ensime with newer versions of SBT, you’ll find that SBT grows to fill available memory and then crashes. This is because the latest released version of Ensime assumes the project format of an old version of SBT. To fix this, just add the following to your .emacs after you require Ensime: