Elaborator reflection: extending Idris in Idris

David Christiansen, Edwin Charles Brady

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Many programming languages and proof assistants are defined by elaboration from a high-level language with a great deal of implicit information to a highly explicit core language. In many advanced languages, these elaboration facilities contain powerful tools for program construction, but these tools are rarely designed to be repurposed by users. We describe elaborator reflection, a paradigm for metaprogramming in which the elaboration machinery is made directly available to metaprograms, as well as a concrete realization of elaborator reflection in Idris, a functional language with full dependent types. We demonstrate the applicability of Idris’s reflected elaboration framework to a number of realistic problems, we discuss the motivation for the specific features of its design, and we explore the broader meaning of elaborator reflection as it can relate to other languages.
Original languageEnglish
Title of host publicationProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016)
Place of PublicationNew York
PublisherACM
Pages284-297
Number of pages14
ISBN (Print)9781450342193
DOIs
Publication statusPublished - 4 Sept 2016
EventICFP 2016 - 21st ACM SIGPLAN International Conference on Functional Programming - Nara Kasugano International Forum, Nara, Japan
Duration: 18 Sept 201624 Sept 2016
Conference number: 21
http://conf.researchr.org/home/icfp-2016

Publication series

NameACM SIGPLAN Notices
PublisherAssociation for Computing Machinery
Number9
Volume51
ISSN (Print)0362-1340
ISSN (Electronic)1558-1160

Conference

ConferenceICFP 2016 - 21st ACM SIGPLAN International Conference on Functional Programming
Abbreviated titleICFP 2016
Country/TerritoryJapan
CityNara
Period18/09/1624/09/16
Internet address

Keywords

  • Metaprogramming
  • Dependent types
  • Elaboration

Fingerprint

Dive into the research topics of 'Elaborator reflection: extending Idris in Idris'. Together they form a unique fingerprint.

Cite this