Towards a practical programming language based on dependent type theory

Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology and Göteborg University, 2007.
[pdf, bib ]

Dependent type theories have a long history of being used for theorem proving. One aspect of type theory which makes it very powerful as a proof language is that it mixes deduction with computation. This also makes type theory a good candidate for programming---the strength of the type system allows properties of programs to be stated and established, and the computational properties provide semantics for the programs.

This thesis is concerned with bridging the gap between the theoretical presentations of type theory and the requirements on a practical programming language. Although there are many challenging research problems left to solve before we have an industrial scale programming language based on type theory, this thesis takes us a good step along the way.

In functional programming languages pattern matching provides a concise notation for defining functions. In dependent type theory, pattern matching becomes even more powerful, in that inspecting the value of a particular term can reveal information about the types and values of other terms. In this thesis we give a type checking algorithm for definitions by pattern matching in type theory, supporting overlapping patterns, and pattern matching on intermediate results using the with rule.

Traditional presentations of type theory suffers from rather verbose notation, cluttering programs and proofs with, for instance, explicit type information. One solution to this problem is to allow terms that can be inferred automatically to be omitted. This is usually implemented by inserting metavariables in place of the omitted terms and using unification to solve these metavariables during type checking. We present a type checking algorithm for a theory with metavariables and prove its soundness independent of whether the metavariables are solved or not.

In any programming language it is important to be able to structure large programs into separate units or modules and limit the interaction between these modules. In this thesis we present a simple, but powerful module system for a dependently typed language. The main focus of the module system is to manage the name space of a program, and an important characteristic is a clear separation between the module system and the type checker, making it largely independent of the underlying language.

As a side track, not directly related to the use of type theory for programming, we present a connection between type theory and a first-order logic theorem prover. This connection saves the user the burden of proving simple, but tedious first-order theorems by leaving them for the prover. We use a transparent translation to first-order logic which makes the proofs constructed by the theorem prover human readable. The soundness of the connection is established by a general metatheorem.

Finally we put our work into practise in the implementation of a programming language, Agda, based on type theory. As an illustrating example we show how to program a simple certfied prover for equations in a commutative monoid, which can be used internally in Agda. Much more impressive examples have been done by others, showing that the ideas developed in this thesis are viable in practise.


Valid HTML 4.01! Disclaimer
Last modified: Fri 17 Aug 2007 03:18:35 PM CEST