Posts tagged Idris

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.