Background and Outline: Extensions of Dependant Type Theory - Induction, Interaction, Universes

It is a central aim of Computer Science to develop programming languages which support the development of efficient and correct programs. Most programming languages use types in order to obtain this goal. Types restrict the kind of data used by a program for input, output and for intermediate data. It is often possible to predict the size of the data stored in a data type, which allows more efficient memory management. Typed languages prevent the programmer from making mistakes, which result in data, which does not match the type, especially when combining several programs. Further, typed programming languages make it explicit what the programmer had in mind when defining data structures, which results in more transparent programs.

In simple type theory, types do not depend on other types or elements of other types. Many programming languages have added polymorphism, which means that types can depend on other types (e.g. templates/generics in object oriented languages, modules, classes and functors in functional programming languages). In dependent type theory (DTT), types might depend on both other types and their elements. An example of the expressiveness added by dependent types is matrix multiplication. In non-dependently typed languages, the arguments of this function are the three dimensions involved and two matrices of arbitrary dimension - that the dimensions of the matrices are in accordance with the dimensions specified would require dependent types and can without them only be checked at runtime. Another example is the format string operation (printf) in C, which cannot be introduced in Java, since the types of the later arguments depend on the formatting string. In DTT, it can be typed \citep{augustsson:cayenne}). Weak forms of dependent types occur in standard languages (e.g. templates in C++, generics in Ada or functors in ML), but they are too restrictive to be applicable to the above examples, do not check conformance of parameters (Ada), or only allow instantiation by constants (C++). Recently, a new direction in software engineering called generative programming has been established, with the goal of automatising the production of software. Apart from working on new language paradigms, research on generative types focuses especially on the template mechanism of C++, which has a static and therefore restrictive type system.\par It is due to Augustsson (Chalmers, Sweden that there exists now an efficient functional programming language based on full DTT, called Cayenne. Independently, H. Xi has developed two dependently typed programming languages: dependent ML and Xanadu . Xi however restricts dependencies to natural numbers. Especially Augustsson's implementation has stimulated a series of workshops on ``Dependent Types in Programming''.

Traditionally, the main application of dependent types has been the area of program verification and the development of programs with guaranteed correctness rather than ordinary programming. In DTT, a predicate is nothing but a type, which is inhabited, if the predicate is true, and otherwise empty. The property, that a list is sorted, can be expressed as a type depending on that list, and a sorting function can be typed as a function taking two lists and returning a list with this property - the property ``sorted'' is verified at compile time. Similarly, one can express for instance that a railway interlocking system is safe. Essentially any property, which can be expressed by a formula, can be written as a dependent type.

Anton Setzer
Last modified: Sun Feb 18 21:20:20 GMT 2007