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

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.