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.

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