SHF: SMALL: Dependently-typed Haskell

SHF：小：依赖类型的 Haskell

• 批准号: 1116620
• 负责人: Stephanie Weirich
• 金额: $ 49.68万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-08-01 至 2016-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1116620&HistoricalAwards=false
• 关键词: 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.

该项目的主要目标是提高软件系统的稳定性。许多现代编程语言使用静态类型检查来消除程序中的错误。然而，作为这些检查器基础的类型系统是保守的，并且拒绝了几类有用的正确程序。特别是泛型编程技术，它优化了程序开发中的数据结构，概括了接口，并界定了样板，很难进行类型检查。尽管依赖类型系统在类型检查方面提供了灵活性，特别是在泛型编程方面，但它们还没有被集成到实际的编程语言中。 这个项目的建议工作将增加一个成熟的，通用的，静态类型的编程语言支持依赖类型的编程。具体来说，该项目将扩展格拉斯哥Haskell编译器（GHC）的源语言和中间语言。虽然泛型编程是Haskell的主要应用领域，但本文提出的Haskell扩展将在许多领域增强Haskell的依赖类型编程能力。这个项目是与剑桥微软研究院的GHC编译器的设计者和实现者合作完成的。该团队包括依赖类型系统，泛型编程，语言设计和实现领域的世界领先者。由于GHC是一个开源项目，Haskell的扩展将免费分发。此外，该项目将通过资助博士生和将其结果纳入高级研究生和本科生课程而产生教育效益。