Skip to content

Research at St Andrews

Elaborator reflection: extending Idris in Idris

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

Author(s)

David Christiansen, Edwin Charles Brady

School/Research organisations

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.
Close

Details

Original languageEnglish
Title of host publicationProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
Place of PublicationNew York
PublisherACM
Pages284-297
ISBN (Print)9781450342193
DOIs
Publication statusPublished - 4 Sep 2016
EventICFP 2016 - 21st ACM SIGPLAN International Conference on Functional Programming - Nara Kasugano International Forum, Nara, Japan
Duration: 18 Sep 201624 Sep 2016
http://conf.researchr.org/home/icfp-2016

Conference

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

    Research areas

  • Metaprogramming, Dependent types, Elaboration

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Value-dependent session design in a dependently typed language

    de Muijnck-Hughes, J., Brady, E. C. & Vanderbauwhede, W., 2 Apr 2019, Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software, Prague, Czech Republic, 7th April 2019. Martins, F. & Orchard, D. (eds.). Open Publishing Association, p. 47-59 (Electronic Proceedings in Theoretical Computer Science; vol. 291).

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

  2. Subtype polymorphism à la carte via machine learning on dependent types

    Swan, J., Johnson, C. G. & Brady, E. C., 16 Jul 2018, Companion Proceedings for the ISSTA/ECOOP 2018 Workshops. New York, NY: Association for Computing Machinery, Inc, p. 14-16 3 p.

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

  3. Type driven development of concurrent communicating systems

    Brady, E. C., 7 Jul 2017, In : Computer Science. 18, 3, 22 p., 1413.

    Research output: Contribution to journalArticle

  4. Sequential decision problems, dependent types and generic solutions

    Botta, N., Jansson, P., Ionescu, C., Christiansen, D. & Brady, E. C., 17 Mar 2017, In : Logical Methods in Computer Science. 13, 1, 23 p., 7.

    Research output: Contribution to journalArticle

  5. Type-driven development with Idris

    Brady, E. C., Mar 2017, Shelter Island: Manning Publications Co. 480 p.

    Research output: Book/ReportBook

ID: 243730122