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
Publication statusPublished - 2013

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., Vanderbauwhede, W. & Brady, E. C., 7 Apr 2019, Electronic Proceedings in Theoretical Computer Science. Open Publishing Association

    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

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