Posts tagged Idris

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.