The primary goal of this project is improve the stability of software systems. Many modern programming languages use static type checking to eliminate errors from programs. However, the type systems that underlie these checkers are conservative and reject several classes of useful, correct programs. In particular, the techniques of generic programming, which optimize data structures, generalize interfaces and eliminate boilerplate in program development, are difficult to type check. Although dependent type systems provide flexibility in type checking, particularly with respect to generic programming, they have not yet been integrated into realistic programming languages.
The proposed work of this project will augment a mature, general purpose, statically-typed programming language with support for dependently-typed programming. Specifically, the project will extend the source and intermediate languages of the Glasgow Haskell Compiler (GHC). Although generic programming is the key application area, the Haskell extensions proposed here will enhance the capabilities of dependently-typed programming in Haskell in many domains. This project is in collaboration with the designers and implementers of the GHC compiler at Microsoft Research, Cambridge. The team includes world leaders in the areas of dependent type systems, generic programming, language design and implementation. As GHC is an open-source project, the extensions to Haskell will be freely distributed. Furthermore, the project will have educational benefits through the funding of doctoral students and the integration of its results into advanced graduate and undergraduate courses.
