A new paper by David Christiansen and myself, to appear in ICFP 2016. Abstract:
Many programming languages and proof assistants are defined by elaboration from a high-level language with a great deal of implicit information to a highly explicit core language. In many advanced languages, these elaboration facilities contain powerful tools for program construction, but these tools are rarely designed to be repurposed by users. We describe elaborator reflection, a paradigm for metaprogramming in which the elaboration machinery is made directly available to metaprograms, as well as a concrete realization of elaborator reflection in Idris, a functional language with full dependent types. We demonstrate the applicability of Idris’s reflected elaboration framework to a number of realistic problems, we discuss the motivation for the specific features of its design, and we explore the broader meaning of elaborator reflection as it can relate to other languages.
You can get the PDF here.
I’ve just submitted a new draft, Cross-platform Compilers for Functional Languages. Abstract:
Constructive comments and suggestions are welcome, particularly if you’ve tried implementing a code generator for Idris.
I’ve written a draft paper describing the implementation of Idris,
Implementation of a General Purpose Programming Language with Dependent Types, abstract as follows:
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 succesive 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.
There’s still some polishing to do, but comments on the content, form, and so on, would be most welcome. Enjoy!
A new draft, Resource-safe Systems Programming with Embedded Domain Specific Languages, by Edwin Brady and Kevin Hammond, submitted September 2011.
We introduce a new overloading notation that facilitates programming, modularity and reuse in Embedded Domain Specific Languages (EDSLs), and use it to reason about safe resource usage and state management. We separate the structural language constructs from our primitive operations, and show how precisely-typed functions can be lifted into the EDSL. In this way, we implement a generic framework for constructing state-aware EDSLs for systems programming.
As usual, comments and questions are most welcome!