Filling out source locations in Idris

in Idris, DSLs, Programming

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.

New paper submission: “Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection”

in Idris, Quotation

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.

Implementing an Emacs programming language mode: beyond the basics

in Emacs

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!

Tutorials on my ITU page


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.

Using Scala libraries with new compiler versions

in Scala

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.

The first step is to understand the relationship between the various parts:
  • SBT is responsible for compiling your project, running tests, and generally performing the same role as make or ant. It also uses Ivy for retrieving library dependencies.

  • Apache Ivy provides an infrastructure for dependency management. Libraries exist in repositories, similar to Debian package repositories, and they are available in multiple versions.

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.

Make Ensime work with newer versions of SBT

in Scala

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: