Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection

Idris's reflection features allow Idris metaprograms to manipulate a representation of Idris's core language as a datatype, but these reflected terms were designed for ease of type checking and are therefore exceedingly verbose and tedious to work with. A simpler notation would make these programs both easier to read and easier to write. We describe a variation of quasiquotation that uses the language's compiler to translate high-level programs with holes into their corresponding reflected representation, both in pattern-matching and expression contexts. This provides a notation for reflected language that matches the notation used to write programs, allowing readable metaprograms.