Abstract
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.
Original language | English |
---|---|
Title of host publication | Preproceedings of the 26nd Symposium on Implementation and Application of Functional Languages (IFL 2014) |
Editors | Sam Tobin-Hochstadt |
Number of pages | 9 |
Publisher | Association for Computing Machinery |
Publication date | 2014 |
ISBN (Print) | 978-1-4503-3284-2 |
DOIs | |
Publication status | Published - 2014 |
Event | 26nd Symposium on Implementation and Application of Functional Languages - Northeastern Universit, Boston, MA, United States Duration: 1 Oct 2014 → 3 Oct 2014 http://www.wikicfp.com/cfp/servlet/event.showcfp?eventid=39053©ownerid=48563 |
Conference
Conference | 26nd Symposium on Implementation and Application of Functional Languages |
---|---|
Location | Northeastern Universit |
Country/Territory | United States |
City | Boston, MA |
Period | 01/10/2014 → 03/10/2014 |
Internet address |
Keywords
- Quasiquotation
- Proof automation
- Metaprogramming