Idris, a general-purpose dependently typed programming language: Design and implementation
この論文をさがす
説明
<jats:title>Abstract</jats:title><jats:p>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<jats:sc>Idris</jats:sc>, a new dependently typed functional programming language.<jats:sc>Idris</jats:sc>is intended to be a<jats:italic>general-purpose</jats:italic>programming language and as such provides high-level concepts such as implicit syntax, type classes and<jats:monospace>do</jats:monospace>notation. I describe the high-level language and the underlying type theory, and present a tactic-based method for<jats:italic>elaborating</jats:italic>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.</jats:p>
収録刊行物
-
- Journal of Functional Programming
-
Journal of Functional Programming 23 (5), 552-593, 2013-09
Cambridge University Press (CUP)