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

David Raymond Christiansen

    Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

    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 languageEnglish
    Title of host publicationPreproceedings of the 26nd Symposium on Implementation and Application of Functional Languages (IFL 2014)
    EditorsSam Tobin-Hochstadt
    Number of pages9
    PublisherAssociation for Computing Machinery
    Publication date2014
    ISBN (Print)978-1-4503-3284-2
    DOIs
    Publication statusPublished - 2014
    Event26nd Symposium on Implementation and Application of Functional Languages - Northeastern Universit, Boston, MA, United States
    Duration: 1 Oct 20143 Oct 2014
    http://www.wikicfp.com/cfp/servlet/event.showcfp?eventid=39053&copyownerid=48563

    Conference

    Conference26nd Symposium on Implementation and Application of Functional Languages
    LocationNortheastern Universit
    Country/TerritoryUnited States
    CityBoston, MA
    Period01/10/201403/10/2014
    Internet address

    Keywords

    • Quasiquotation
    • Proof automation
    • Metaprogramming

    Fingerprint

    Dive into the research topics of 'Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection'. Together they form a unique fingerprint.

    Cite this