Abstract

Developing Dependently Typed Programs in LEGO, Conor McBride.

I've spent the last couple of years working on technology to support dependently typed functional programming within LEGO. This boils down to tactics for expressing pattern matching programs in terms of the elimination rules (recursion principles) LEGO provides for datatypes. But I'm not going to talk about how it works; I'm going to talk about what I've done with it: a peek over the terms-in-types horizon.

I've written a common garden unification algorithm for a first order syntax. What's new? By the wonder of types dependending on terms, I've built enough extra information into the datatypes to make this program (higher-order) primitive recursive.

Furthermore, the technology for applying datatype elimination rules is so much fun that I've been manufacturing elimination rules for other things as well: programs, for instance. They turn out to be extremely handy for reasoning about one program as a component of another, greatly simplifying the correctness proof of the unification algorithm, for example.

Tom Chothia

Last modified: Mon May 10 14:42:45 BST 1999