Idris, a general-purpose dependently typed programming language: Design and implementation
- 1 September 2013
- journal article
- research article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 23 (5), 552-593
- https://doi.org/10.1017/s095679681300018x
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 implementors. 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.Keywords
This publication has 16 references indexed in Scilit:
- A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive ConstructionsLogical Methods in Computer Science, 2012
- OutsideIn(X)Modular type inference with local assumptionsJournal of Functional Programming, 2011
- First-Class Type ClassesLecture Notes in Computer Science, 2008
- Applicative programming with effectsJournal of Functional Programming, 2007
- The view from the leftJournal of Functional Programming, 2004
- The size-change principle for program terminationACM SIGPLAN Notices, 2001
- The ZipperJournal of Functional Programming, 1997
- Inductive familiesFormal Aspects of Computing, 1994
- Unification under a mixed prefixJournal of Symbolic Computation, 1992
- Compiling pattern matchingLecture Notes in Computer Science, 1985