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:
This report is available in the following formats:Previous | Index | Next