Filling out source locations in 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.