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
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.
Last modified: Mon May 10 14:42:45 BST 1999