Silence, and adding things up

Well, so much for new year resolutions . I’d like to claim I haven’t posted anything for a while because I’ve been being super-productive, but I think it’s more due to teaching and not paying much attention to blogland. Perhaps there will be more brain dumps when the students have gone…

Anyway. We’ve just submitted a paper on the carry ripple adder for binary numbers, using dependent types, to TFP 2007.

Correctness by Construction – a Carry-Ripple Adder

I dedided to to try out Ivor’s new pattern matching gadgetry by implementing a program I’ve been wanting to write for ages. This is a carry-ripple adder for binary numbers, where the representation of binary numbers is indexed over its meaning (i.e. the natural number it represents). Doing this has the advantage that any program written over the binary numbers must satisfy the appropriate invariant properties; a carry-ripple adder really must implement addition corresponding to addition of the natural numbers.

Dependent Pattern Matching in Ivor

I’m working on Ivor, a theorem proving library for Haskell. It’s an implementation of dependent type theory which is embeddable in Haskell applications and easily extensible with domain specific tactics. You can read a paper explaining the motivation and design in more detail.

I’ve been using it for research into using dependent types for proving resource bounds of functional programs, and more generally for experiments with multi-stage programming with dependent types. However, I’ve found it frustratingly hard to implement interesting dependently typed programs, because of the lack of pattern matching, or an Epigram-like elimination with a motive tactic. Doing the latter by hand is, er, an interesting challenge up to a point, but gets tedious very quickly.

And so, over the last couple of days I’ve been adding dependent pattern matching. You can now do such things as bounds safe vector lookup functions as follows:

Data Nat:* = O:Nat | S:(k:Nat)Nat; -- Natural numbers

Data Fin:(n:Nat)*
  = fz:(k:Nat)Fin (S k)
  | fs:(k:Nat)(i:Fin k)(Fin (S k)); -- Bounded natural numbers

Data Vect (A:*) : (n:Nat)*
  = nil : Vect A O
  | cons : (k:Nat)(xs:Vect A k)(Vect A (S k)); -- Bounded vector

Match lookup : (A:*)(n:Nat)(i:Fin n)(xs:Vect A n)A =
    lookup _ _ (fz _) (cons _ _ x xs) = x
  | lookup _ _ (fs n i) (cons _ n x xs) = lookup _ _ i xs;

Ivor checks that the patterns for lookup cover all possible cases (any other patterns would not be well-typed, in particular cases for vnil), and that recursive calls are well-founded.
It will, of course, only match on constructor patterns (you can’t do anything like Epigram’s views), and you can’t develop functions interactively (i.e. leave holes in terms to fill in later) but nevertheless it’s a big improvement on what was available before.

I really ought to write up the way the system works out which patterns are needed to guarantee all possibilities are covered; intuitively I’m sure it works but writing it up more formally may reveal a few holes. But it’s too late in the evening (um, early in the morning in fact) to do that just now…

I think it would be nice to deal with implicit arguments, so that you could write, e.g.:

Match lookup : (i:Fin n)(xs:Vect A n)A =
    lookup fz (cons x xs) = x
  | lookup (fs n i) (cons x xs) = lookup i xs;

Then it’s almost beginning to look like a proper programming language. However, I expect there are more important things to do first…