## Archive for the ‘**Dependent Types**’ Category

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!

Last Friday I gave a talk at Scottish Theorem Proving in which I sketched how Idris worked.

Here are the slides. There’ll be a paper explaining in more detail at some point fairly soon…

My goal for Idris is to make it a *practical* dependently typed programming language – suitable for general purpose, systems programming, with precise types when you need them for increasing confidence in correctness of your program. One thing that a modern, practical language really needs, however, is a sane, safe, general way of overloading functions. Haskell‘s solution to this, type classes, is by far the neatest I’ve seen, so in the new implementation of Idris, that’s what I’ve done. They work much as you’d expect if you’re used to Haskell. For example, the `Show`

class could look a bit like this:

class Show a where {
show : a -> String;
}

This generates a function `show : Show a => a -> String`

, i.e. a function which will display any `a`

under the constraint that `a`

is an instance of `Show`

. We can declare instances…

instance Show Nat where {
show O = "O";
show (S k) = "s" ++ show k;
}

…and instances can themselves have constraints (and, indeed, be instances for dependent types):

instance Show a => Show (Vect a n) where {
show xs = "[" ++ show' xs ++ "]" where {
show' : Show a => Vect a n -> String;
show' VNil = "";
show' (x :: VNil) = show x;
show' (x :: xs) = show x ++ ", " ++ show' xs;
}
}

As you’d expect, classes can have constraints too:

class Monad (m : Set -> Set) where {
return : a -> m a;
(>>=) : m a -> (a -> m b) -> m b;
}
class Monad m => MonadPlus (m : Set -> Set) where {
mplus : m a -> m a -> m a;
mzero : m a;
}

Note that, in this case, we have to give an explicit kind for the parameter `m`

. If you don’t give this, Idris will assume that the parameter is of kind `Set`

.

The prelude and builtins modules now have a couple of the more obviously useful type classes. However, I’m not going to rush into extending this – we should probably think carefully about what classes we need and how they relate to each other, rather than do things “just because Haskell did it that way”!

### How it works

Type classes classify types according to which operations can be overloaded for them. Internally, therefore, we can represent type classes as a record of functions. For example, for show:

data Show : Set -> Set where
instanceShow : (show : a -> String) -> Show a;
show : Show a -> a -> String;
show (instanceShow s) x = s x;

An instance for a type `a`

is then a value of type `Show a`

; for example for `Nat`

:

showNat : Show Nat;
showNat = instanceShow show' where {
show' O = "O";
show' (S k) = "s" ++ show' k;
}

All the elaborator has to do on seeing a `class`

declaration is to generate the appropriate data type, and on seeing an `instance`

declaration generate the appropriate instance function.

Class constraints are a special kind of implicit argument (much like Agda’s instance arguments). On seeing a function call `show x`

, the elaborator will attempt to resolve the implicit argument first by looking in the local context, then attempting to refine by any global class instances which match, recursively.

### Still to do…

Default definitions of class methods will be very useful, as will a deriving mechanism. The former is easy, and so likely to happen soon. The latter is hard, and so isn’t.

Note also that this mechanism is intended entirely for a safe general overloading mechanism, and many of the type class tricks which are possible in Haskell are unlikely to work (though, at least, Idris classes can have more than one parameter). Such tricks, I believe, ought to be unnecessary anyway since the dependent type system is very flexible. It will, however, be interesting to see what *can* be done that I haven’t thought of…

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!

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.)

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.