CIF: Small: Rich Type Inference for Functional Programming

CIF：小型：函数式编程的丰富类型推理

• 批准号: 1319880
• 负责人: Stephanie Weirich
• 金额: $ 45万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2018-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319880&HistoricalAwards=false
• 关键词: CIF; Small; Rich; Type; Inference

The correctness of computer software often relies on its adherence to application-specific invariants during the course of its execution. These invariants are complex, often involving relationships between many different parts of the system, and implicit, often never formally expressed in the text of the program. Violating these invariants, however, leads to numerous bugs and security holes. As a result, programmers employ static type systems to capture these invariants and enable the use of automated tools to check that they are maintained. Algorithms for type inference allow complex types to remain implicit, easing software development and maintenance, while still readily available for documentation and enforcement. While recent type system extensions greatly enrich the expressiveness of statically typed languages, type inference algorithms have not kept pace. This research evaluates the integration of SMT (Satisfiability Modulo Theory) solvers into the type inference algorithm of an industrial-strength functional programming language. In particular, in collaboration with researchers at Microsoft Research Cambridge, it extends the type inference algorithm of the Glasgow Haskell Compiler (GHC). GHC is a mature, open source, Haskell Compiler that is gaining popularity in industry due to its rich type system. The project also includes education and outreach components in the form of an advanced undergraduate/masters level course and in the direct support of Ph.D. students.

计算机软件的正确性通常依赖于其在执行过程中对特定于应用的不变量的遵守。这些不变量是复杂的，通常涉及系统的许多不同部分之间的关系，并且是隐式的，通常从未在程序的文本中正式表达。然而，违反这些不变量会导致许多错误和安全漏洞。因此，程序员使用静态类型系统来捕获这些不变量，并允许使用自动化工具来检查它们是否得到维护。 类型推断的算法允许复杂类型保持隐式，从而简化软件开发和维护，同时仍然可以随时用于文档编制和实施。虽然最近的类型系统扩展极大地丰富了静态类型语言的表达能力，但类型推理算法却没有跟上。本研究评估SMT（可满足性模理论）求解器到工业强度的函数式编程语言的类型推理算法的集成。特别是，与微软研究院剑桥的研究人员合作，它扩展了格拉斯哥Haskell算法（GHC）的类型推理算法。 GHC是一个成熟的、开源的Haskell编译器，由于其丰富的类型系统而在工业界越来越受欢迎。该项目还包括教育和推广部分，其形式是高级本科/硕士课程，并得到博士生的直接支持。学生

项目成果

Total Haskell is reasonable Coq

• DOI: 10.1145/3167092
• 发表时间: 2017-11
• 期刊: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
• 作者: Antal Spector-Zabusky;Joachim Breitner;C. Rizkallah;Stephanie Weirich

Keep your laziness in check

控制你的懒惰

• DOI: 10.1145/3236797
• 发表时间: 2018
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Foner, Kenneth;Zhang, Hengchu;Lampropoulos, Leonidas
• 通讯作者: Lampropoulos, Leonidas

A specification for dependent types in Haskell

Haskell 中依赖类型的规范

• DOI: 10.1145/3110275
• 发表时间: 2017
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Weirich, Stephanie;Voizard, Antoine;de Amorim, Pedro Henrique;Eisenberg, Richard A.
• 通讯作者: Eisenberg, Richard A.

A role for dependent types in Haskell

Haskell 中依赖类型的角色

• DOI: 10.1145/3341705
• 发表时间: 2019
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Weirich, Stephanie;Choudhury, Pritam;Voizard, Antoine;Eisenberg, Richard A.
• 通讯作者: Eisenberg, Richard A.

Type variables in patterns

在模式中键入变量

• DOI: 10.1145/3242744.3242753
• 发表时间: 2018
• 期刊: Haskell Symposium
• 作者: Eisenberg, Richard A.;Breitner, Joachim;Peyton Jones, Simon
• 通讯作者: Peyton Jones, Simon