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

I’m busy revising the “How Idris works” paper, and you can find the latest draft here. Any further comments on how to improve it would be most welcome! 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 implementations. In this paper, I describe the implementation of a new dependently typed functional programming language, IDRIS. 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 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, based on a domain specific language embedded in Haskell, facilitates the implementation of new high level language constructs.

Posted February 10, 2013 by edwinb in Dependent Types, Idris

%d bloggers like this: