SHF: SMALL: Dependently-typed Haskell

这个项目的主要目标是提高软件系统的稳定性。许多现代编程语言使用静态类型检查来消除程序中的错误。然而，作为这些检查器基础的类型系统是保守的，会拒绝一些有用的、正确的程序。特别是，泛型编程技术，优化数据结构，泛化接口和消除程序开发中的样板，很难进行类型检查。尽管依赖类型系统在类型检查方面提供了灵活性，特别是在泛型编程方面，但它们还没有被集成到实际的编程语言中。这个项目提出的工作将增加一个成熟的、通用的、静态类型的编程语言，支持依赖类型的编程。具体来说，该项目将扩展格拉斯哥Haskell编译器（GHC）的源语言和中间语言。虽然泛型编程是关键的应用领域，但这里提出的Haskell扩展将在许多领域增强Haskell中依赖类型编程的能力。这个项目是与剑桥微软研究院ghc编译器的设计者和实现者合作完成的。该团队包括依赖类型系统、泛型编程、语言设计和实现领域的全球领导者。由于GHC是一个开源项目，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.