This week I’ve been giving a course on Dependently Typed Functional Programming in Idris at IT University, Copenhagen. Various course materials are available:

## Idris course at ITU, slides and video

## On Partial Functions in Idris

I had an email from a student asking why Idris supported partial functions, saying that it was surprising that a dependently typed language supported partial functions, because types are supposed to be precise specifications and you can’t be sure you have a precise implementation if your functions aren’t total. This is a very good question, and my answer was quite long, so following these academic blogging tips, I’ll reproduce my answer here. The tl;dr version is that, while I agree totality is important and I aim to make all of my programs total (I don’t think I’ve ever wanted to write a function with neither terminates nor produces results occasionally, after all) it’s a bit more complicated than that in practice.

I’m going to use “total” in a fairly informal sense here. By “total function” I mean either:

- A function which terminates for possible inputs, or
- A function which is guaranteed to produce some output before making a recursive call

In particular, this means you can still write an interpreter or operating system, for example. That is, you can write programs which run forever, but at least they achieve something while doing so.

It is a good idea to aim to make all of your functions total, as David Turner argues – when functions are total, you really can believe that “well-typed programs don’t go wrong” because you know you’re going to get an answer eventually (or in the case of coinductive functions, you know you’re going to keep making progress). And, indeed, dependent types can help you achieve that goal because you can use the extra structure the types give you as additional evidence for the termination checker. Here is a nice example.

Then, of course, some programs are really proofs, that you never actually run but which do demonstrate some properties of other functions. In this case, it’s vitally important that they are total, to guarantee that you haven’t missed any cases, or relied on circular reasoning, and so every possible input leads to a proof object.

Having said all that, Idris still supports partial functions, for two main reasons.

Firstly, you can divide programs in general into two categories:

- Programs you haven’t finished writing yet
- Programs which are complete

The first category is significantly larger than the second. Even more so if you replace “Programs” with “Applications”.

In the case that your program isn’t finished yet, you don’t want your type checker shouting at you that it’s not finished, because you already know, but you still might want to test it (sometimes we like to run our programs, as well as read and write them, after all). You might want to try running a program even with an incomplete proof, to help you develop an intuition for how the proof might work, or even to see if there are test cases which might invalidate your hypothesis. Alternatively, you might have a nice natural recursive algorithm which is not obviously structurally recursive (the functional version of quicksort is an obvious example of this) and not want to hold up the development of the rest of your application while you develop the termination proof.

The fact that programs spend most of their lives in an unfinished state is one reason people are interested in gradual types, and why a recent GHC extension allows you to run programs with type errors. You don’t want to release software with type errors (or, in the case of an Idris program with an associated correctness proof, release software with an incomplete proof) but it might be convenient during development.

Secondly, I don’t believe it’s a language’s job to tell a program what level of precision their programs’ types should have. Rather, a language and its features are there to help a programmer do their job. If I want the language to help me write a totally correct program with a precise specification, then I certainly want a totality checker, but if I’m just writing a quick script to do a simple task, maybe I’d rather just get the job done. I would like the library code the script invokes to be total, but I might not be so bothered about the script itself, at first.

Related to this, remember that there’s more you can do with dependent types than prove functional correctness. Just being able to give types to more programs is already a benefit which doesn’t require programs to be total. Dependent types can help you write generic libraries – the Eff library is a developing example of this, as are embedded domain specific languages in general – where the library user is making use of dependent types without necessarily being aware of it.

Idris aims to be a general purpose programming language, rather than a theorem prover, so aims to support all uses of dependent types, or even to support programming with conventional types if that’s all you need, so the default is to support partial functions. If the goal was primarily to be a theorem prover, I think the opposite choice would have been appropriate. Whatever happens, though, functions are always checked for totality, and you can make partial functions a compile-time error by default with the “–total” flag.

If you want complete safety, you certainly have to work for it, and depending on your application that may be important. Sometimes, though, you just want to get things done. In that case, Idris will let you – but at least the type system and totality checker make it clear what assumptions you have made to do so.

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

## PLPV 2013 Slides

I have put slides from my PLPV 2013 invited talk online here. You can also find the example code.

Of course, the slides won’t make as much sense as with the accompanying commentary, but at least you’ll see what I talked about, and maybe you’ll get something from them anyway. In them, you’ll find:

- An introduction to Idris
- Some examples: verified binary arithmetic, lightweight verification of a virtual machine, and

my plan to never have to write a monad transformer again. - Some notes on compilation issues

## Whitespace in Idris

As a weekend hack, I’ve been implementing the Whitespace programming language, in Idris. You can find it on github. Whitespace, behind the syntax, is a stack based language with unbounded integers and a single global heap, and control flow implemented using labels, conditional jumps, and subroutine calls. There’s no types (just integers for everything) So what do we gain by implementing it in a language with dependent types? It turns out there’s some interesting things we can do, and problems we have to solve:

- Various operations are only valid if the stack is in the right form (e.g. arithmetic requires at least two items at the top of the stack, and leaves at least one item). We can often statically check that the stack is in the right form before executing such instructions, and at least statically check that the necessary dynamic checks are carried out.
- We need to consider how to represent the stack – a
`Stack n`

is the type of stacks with*at least*elements.`n`

- There’s a lot of bounds checking of stack references, and as much of this as possible is made static.
- A jump is only valid if the given label is defined. We can statically check this, too, and guarantee that a program we execute has well-defined labels.
- Although whitespace is Turing complete, we can still use the totality checker to verify that executing individual instructions terminates.

If nothing else, we get to see how to use dependent types to make *assumptions* and *invariants* explicit in the code. Even if those invariants aren’t used to guarantee total correctness, we at least get the type checker to tell us where we’ve violated them. In fact, I avoided a few errors this way and found a couple of missing or badly specified parts of the whitespace tutorial… Perhaps I’ll write more on this at some point…

## 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!

## Elaborating Idris – STP slides

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…

## Type Classes in Idris

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…

## Idris, Mk II

About a month ago, I started working on a complete reimplementation of Idris, because there are a number of things about the current implementation that have been bothering me for a while. It’s now got to a point where it’s beginning to work (in particular, the standard well-typed interpreter is up and running). You can start playing with it now, and follow progress at the github repository.

I’m usually very reluctant to start something again – especially so with Idris since I’ve been working on it for a few years now. But there’s quite a few problems with the current design. In fact, “design” is too strong a word – I didn’t really know when I started what I wanted the language to do and which features I’d need. Moreover, it’s evolved out of a theorem proving system Ivor that was originally meant to do something else, and it’s getting harder and harder to add the new features I want (e.g. mod cons like `where`

clauses, destructuring `let`

, `case`

, and essential gadgets for developing large systems like separate compilation and a decent module system) without having to jump through hoops.

Pleasingly, the new version is not far off catching up with where the old version was. Basic syntax, type checking with implicit syntax and evaluation are all working (mostly better than before…) There is no `with`

rule yet, but it won’t be long. There’ll be a compiler not long after I’ve decided how to handle IO (I want to keep the IO primitives as primitive as I can so that it will be possible to experiment with different high level representations).

The main, significant, distinction between the previous implementation and this is the type checker. In the new version, the type checker is kept extremely simple – no implicit syntax, no unification, no generating proof obligations or coercions. Instead, we have a core type theory with metavariables, and an EDSL (that is, an embedded domain specific language) called `Elab`

which constructs programs using Coq-style tactics, directed by the high level source text, and filling in metavriables by unification where it can. This idea will be unsurprising to anyone who is following the progress of Epigram.

Making `Elab`

an EDSL has several advantages. Adding a new language construct (e.g. pattern matching, now, or maybe coercions, or type classes, some day…) is simply a matter of writing a sequence of tactics to build that construct in the core type theory. To check a pattern match clause, for example, we elaborate the left hand side inferring types for the pattern variables as we go, and use this information to elaborate the right hand side. Another advantage is that it will be easy to expose the EDSL to an Idris programmer for building domain specific decision procedures (e.g. a Ring Solver would be nice). Finally, making the elaborator do all of the work and keeping the type checker simple means that we can be far more confident that only well-typed programs are accepted.

I’ll go back into my hacking shed now, and I’m staying there until all the programs that worked with the previous version compile. Hopefully this won’t take long :). In the meantime, if you have a go, please let me know what you come up with. In particular, if anything behaves badly, please shout – I want this version to work well!

## 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!