*Abstract:*

Research in dependent type theories [ML71a] has, in the past,
concentrated on its use in the presentation of theorems and
theorem-proving. This thesis is concerned mainly with the
exploitation of the computational aspects of type theory for
programming, in a context where the properties of programs may
readily be specified and established. In particular, it develops
technology for programming with dependent inductive families of
datatypes and proving those programs correct. It demonstrates the
considerable advantage to be gained by indexing data structures
with pertinent characteristic information whose soundness is
ensured by typechecking, rather than human effort.

Type theory traditionally presents safe and terminating computation
on inductive datatypes by means of elimination rules which serve as
induction principles and, via their associated reduction behaviour,
recursion operators [Dyb91]. In the programming language arena,
these appear somewhat cumbersome and give rise to unappealing code,
complicated by the inevitable interaction between case analysis on
dependent types and equational reasoning on their indices which
must appear explicitly in the terms. Thierry Coquand's proposal
[Coq92] to equip type theory directly with the kind of pattern
matching notation to which functional programmers have become used
over the past three decades [Bur69, McB70] offers a remedy to many
of these difficulties. However, the status of pattern matching
relative to the traditional elimination rules has until now been in
doubt. Pattern matching implies the uniqueness of identity proofs,
which Martin Hofmann showed underivable from the conventional
definition of equality [Hof95]. This thesis shows that the adoption
of this uniqueness as axiomatic is sufficient t make pattern
matching admissible.

A datatype's elimination rule allows abstraction only over the
whole inductively defined family. In order to support pattern
matching, the application of such rules to specific instances of
dependent families has been systematised. The underlying analysis
extends beyond datatypes to other rules of a similar second order
character, suggesting they may have other roles to play in the
specification, verification and, perhaps, derivation of programs.
The technique developed shifts the specificity from the
instantiation of the type's indices into equational constraints on
indices freely chosen, allowing the elimination rule to be
applied.

Elimination by this means leaves equational hypothesis in the
resulting subgoals, which must be solved if further progress is to
be made. The first-order unification algorithm for constructor
forms in simple types presented in [McB96] has been extended to
cover dependent datatypes as well, yielding completely automated
solution to a class of problems which can be syntactically
defined.

The justification and operation of these techniques requires the
machine to construct and exploit a standardised collection of
auxiliary lemmas for each datatype. This is greatly facilitated by
two technical developments of interest in their own right:

- a more convenient definition of equality, with a relaxed formulation rule allowing elements of different types to be compared, but nonetheless equivalent to the usual equality plus the axiom of uniqueness;
- a type theory, OLEG, which incorporates incomplete objects, accounting for their `holes' entirely within the typing judgments and, novelly, not requiring any notion of explicit substitution to manage their scopes.

This report is available in the following formats:

Previous | Index | Next