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 implementors. In this paper, I describe the implementation of Idris , a new dependently typed functional programming language. Idris is...