Archive for the ‘Dependent Types’ Category

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

Systems Programming with Dependent Types at DTP11

Slides from my invited talk at DTP 2011 are now available.

In this talk, I give a brief introduction to the Idris programming language, and show how it can be used to implement embedded domain specific languages (EDSLs) with strong correctness properties. I introduce a dsl construct which gives these EDSLs a usable (i.e. readable and writable) concrete syntax, and show how it can be used to tackle realistic resource management problems in systems programming.

Code for the resource management EDSL is on github, though I don’t promise much in the way of comments or documentation yet. There is a paper on the way soon which will explain the gory details.

(Usual disclaimer for publishing slides: you really need the talk as well as the slides to understand all of the details, so questions and comments are more than welcome.)

Posted August 27, 2011 by edwinb in Dependent Types, Idris, Talks

Idris, a language with dependent types

I was at the Dependently Typed Programming ’08 workshop a couple of weeks ago, and it was a lot of fun. Lots of interesting people were there talking variously about fun programs and implementation techniques.

One thing I thought was a little sad, though, is that we don’t yet have a real programming language (that is, a full one you can write programs in and actually run them, and interact with the outside world, read and write files, output HTML, etc, etc …, rather than proof assistants such as Coq and Agda) in which to try out the ideas for real. If you want to do that, the best you can do at the minute is Haskell with GADTs, or Tim Sheard’s Omega. These are interesting in themselves, but I want to know what we can do with full dependent types. Can we write the functional programs we know and love in the style we are used to, and add bits of dependency when we want some invariants checked, do we have to approach programming in a new way, or is some combination possible? It would be nice to have a system in which to try this out.

I’ve been working on file handling and concurrency recently, using the type system to manage state to prevent unauthorised access to resources and to ensure locks are managed correctly, even looking at how types can help prevent deadlock. I’ve been doing this in Ivor, but I think now is the time to give it a go in a real language. To this end…

…I’ve spent the last few weeks hacking on a fledgling dependently typed language called Idris.

It has full dependent types, pattern matching, and some basic IO with Haskell style do notation. I’ve tried a few simple examples, including the traditional well-typed interpreter. Types need to be given for pattern matching functions, but can often be omitted for constants – full type inference is of course impossible with full dependent types.

[Aside: An interesting thing about this is the fPlus function in the interpreter example:

fPlus : Term VNil (TyFun TyNat (TyFun TyNat TyNat));
fPlus = Lam (Lam (plusOp (Var fO) (Var (fS fO))));

This needs a type declaration because typed terms exist relative to an environement, so we have to tell the type checker the initial environment is empty. It turns out we can also just give the environment:

fPlus = Lam {G=VNil} (Lam (plusOp (Var fO) (Var (fS fO))));

So inference on terms in Idris gives type inference in the object language.]

There are a lot of theoretical issues still to sort out in dependently typed programming, such as how full dependent types interact with partial, general recursive functions, or how the universe hierarchy should be organised. I have decided (at least as far as this project goes) not to be interested in such things. I’d just like to get on with programming, and deal with such issues when the answers become more clear.

Early days yet, but I’m going to try using this for real work, and we’ll see how it goes. Any interesting updates, I’ll post them here.

Posted March 9, 2008 by edwinb in Dependent Types