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）的源和中间语言。尽管通用编程是关键的应用程序领域，但此处提出的thehaskell扩展将增强许多域中Haskell中依赖性类型的编程的功能。这个项目与剑桥Microsoft Research的GHCCompiler的设计师和实施者合作。该团队包括在依赖类型系统，通用编程，语言设计和实施领域的世界领域。由于GHC是一个开源项目，因此将自由分发到Haskell的扩展名。此外，该项目将通过博士生的资助并将其结果整合到高级毕业生和教学课程中，从而获得教育益处。