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.
%0 Journal Article
%1 Brady2013Idris
%A Brady, Edwin
%D 2013
%J Journal of Functional Programming
%K 03b15-higher-order-logic-type-theory 68n15-programming-languages 68n18-functional-programming-and-lambda-calculus idris
%N 05
%P 552--593
%R 10.1017/s095679681300018x
%T Idris, A General-Purpose Dependently Typed Programming Language: Design and Implementation
%U http://dx.doi.org/10.1017/s095679681300018x
%V 23
%X 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.
@article{Brady2013Idris,
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.}},
added-at = {2019-03-01T00:11:50.000+0100},
author = {Brady, Edwin},
biburl = {https://www.bibsonomy.org/bibtex/280e821b2ea13b429ce6e4a08d9c83cbe/gdmcbain},
citeulike-article-id = {13112547},
citeulike-linkout-0 = {http://journals.cambridge.org/action/displayAbstract?fromPage=online\&aid=9060502},
citeulike-linkout-1 = {http://dx.doi.org/10.1017/s095679681300018x},
day = 18,
doi = {10.1017/s095679681300018x},
interhash = {983d373264f18b9421f1b2a497dd779e},
intrahash = {80e821b2ea13b429ce6e4a08d9c83cbe},
issn = {0956-7968},
journal = {Journal of Functional Programming},
keywords = {03b15-higher-order-logic-type-theory 68n15-programming-languages 68n18-functional-programming-and-lambda-calculus idris},
month = oct,
number = 05,
pages = {552--593},
posted-at = {2017-10-24 23:16:03},
priority = {4},
timestamp = {2019-03-01T00:11:50.000+0100},
title = {{Idris, A General-Purpose Dependently Typed Programming Language: Design and Implementation}},
url = {http://dx.doi.org/10.1017/s095679681300018x},
volume = 23,
year = 2013
}