Skip to content

Research at St Andrews

Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation

Research output: Contribution to journalArticle

Author(s)

School/Research organisations

Abstract

Many components of a dependently typed programming language are by now well understood, for example the underlying type theory, type checking, unification and evaluation. How to combine these components into a realistic and usable high level language is, however, folklore, discovered anew by successive language implementations. In this paper, I describe the implementation of Idris, a new dependently typed functional programming language. Idris is intended to be a general purpose programming language
and as such provides high level concepts such as implicit syntax,
type classes and do notation. I describe the high level language and the underlying type theory, and present a tactic based method for elaborating concrete high level syntax with implicit arguments and type classes into a fully explicit type theory. Furthermore, I show how this method facilitates the implementation of new high level language constructs.
Close

Details

Original languageEnglish
Pages (from-to)552-593
Number of pages42
JournalJournal of Functional Programming
Volume23
Issue number05
Early online date18 Oct 2013
DOIs
StatePublished - 2013

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

View graph of relations

Related by author

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

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

  3. Type-driven development with Idris

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

    Research output: Book/ReportBook

  4. Automatically proving equivalence by type-safe reflection

    Slama, F. & Brady, E. C. 2017 Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Geuvers, H., England, M., Hasan, O., Rabe, F. & Teschke, O. (eds.). Cham: Springer, p. 40-55 (Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence); vol. 10383)

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

  5. Elaborator reflection: extending Idris in Idris

    Christiansen, D. & Brady, E. C. 4 Sep 2016 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. New York: ACM, p. 284-297

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

Related by journal

  1. PAEAN: portable and scalable runtime support for parallel Haskell dialects

    Berthold, J., Loidl, H-W. & Hammond, K. 2016 In : Journal of Functional Programming. 26, 39 p., e10

    Research output: Contribution to journalArticle

  2. Ott: Effective tool support for the working semanticist

    Sewell, P., Nardelli, F. Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S. & Strnisa, R. Jan 2010 In : Journal of Functional Programming. 20, 01, p. 71-122 52 p.

    Research output: Contribution to journalArticle

  3. The View from the Left

    McBride, C. & McKinna, J. H. Jan 2004 In : Journal of Functional Programming. 14, 1, p. 69-111 43 p.

    Research output: Contribution to journalArticle

ID: 64756474