SHF: SMALL: Dependently-typed Haskell

点击翻译按钮获取中文摘要

The primary goal of this project is improve the stability of softwaresystems. Many modern programming languages use static type checking toeliminate errors from programs. However, the type systems thatunderlie these checkers are conservative and reject several classes ofuseful, correct programs. In particular, the techniques of genericprogramming, which optimize data structures, generalize interfaces andeliminate boilerplate in program development, are difficult to typecheck. Although dependent type systems provide flexibility in typechecking, particularly with respect to generic programming, they havenot yet been integrated into realistic programming languages. The proposed work of this project will augment a mature, generalpurpose, statically-typed programming language with support fordependently-typed programming. Specifically, the project will extendthe source and intermediate languages of the Glasgow Haskell Compiler(GHC). Although generic programming is the key application area, theHaskell extensions proposed here will enhance the capabilities ofdependently-typed programming in Haskell in many domains. This projectis in collaboration with the designers and implementers of the GHCcompiler at Microsoft Research, Cambridge. The team includes worldleaders 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, theproject will have educational benefits through the funding of doctoral studentsand the integration of its results into advanced graduate andundergraduate courses.