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.