Archive for the ‘Papers’ Category

New draft: Implementation of a General Purpose Programming Language with Dependent Types

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!

Posted April 8, 2012 by edwinb in Dependent Types, Idris, Papers

Resource-safe Systems Programming with Embedded Domain Specific Languages

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!

Posted September 16, 2011 by edwinb in Dependent Types, Domain Specific Languages, Idris, Papers


Get every new post delivered to your Inbox.