SHF: MEDIUM: Collaborative Research: The Theory and Practice of Dependent Types in Haskell

SHF：中：协作研究：Haskell 中依赖类型的理论与实践

• 批准号: 1704041
• 负责人: Christian Murphy
• 金额: $ 31.13万
• 依托单位: Bryn Mawr College
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-07-01 至 2021-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1704041&HistoricalAwards=false
• 关键词: SHF; MEDIUM; Collaborative; Research; Theory

This project's overarching goal is to prevent bugs in software by extending the Haskell programming language to support dependent types. Haskell is used by researchers and programmers in industry to build a variety of software systems, such as financial analysis tools, interactive websites, data visualizations, and automated vehicle software. Dependent types are an up-and-coming technology that allows programmers to avoid bugs in their software, allowing them to include mathematical proofs of correctness in their code. These proofs are checked before the software ever runs, ruling out the possibility of failures, such as a crashed website. The intellectual merits are insights into the integration of advanced mathematical theories with an industrial-strength development tool (Haskell) and a deeper understanding of the mathematical principles that underlie the creation of correct software. The project's broader significance and importance are to give the technology industry access to dependent types for the first time, while creating opportunities for students (including those at one principal investigator's undergraduate women's college) to engage with this technology.The project includes both practical and foundational components. The Haskell type system, as implemented in the Glasgow Haskell Compiler (GHC) version 8.0, is able to simulate dependent types through the use of many language extensions. However, this use requires awkward encodings, and the extensions that support them complicate the language. In contrast, the Haskell type system envisioned by this project is based on a uniform approach to dependently typed programming that subsumes prior extensions. Part of this project involves replacing the core language of GHC with one based on dependent type theory, using relevance annotations to ensure that these extensions are backwards compatible. Furthermore, the project also introduces matchable functions, a qualifier that determines whether function applications can be analyzed via pattern matching, enabling the integration of dependent types with GHC's current type inference algorithm. Finally, this project includes an examination of the semantics of dependently typed programming languages with partiality.

这个项目的首要目标是通过扩展Haskell编程语言来支持依赖类型，从而防止软件中的错误。Haskell被工业界的研究人员和程序员用来构建各种软件系统，如财务分析工具、交互式网站、数据可视化和自动驾驶汽车软件。依赖类型是一种新兴的技术，它允许程序员避免软件中的错误，允许他们在代码中包含正确性的数学证明。这些证据会在软件运行之前进行检查，排除失败的可能性，例如网站崩溃。智力上的优点是深入了解先进的数学理论与工业实力的开发工具（Haskell）的整合，以及对创建正确软件所依据的数学原理的更深入理解。该项目的更广泛的意义和重要性是让技术行业第一次接触到依赖类型，同时为学生（包括一位主要研究者的本科女子学院的学生）创造机会参与这项技术。在格拉斯哥Haskell编译器（GHC）8.0版中实现的Haskell类型系统能够通过使用许多语言扩展来模拟依赖类型。然而，这种使用需要笨拙的编码，并且支持它们的扩展使语言复杂化。相比之下，这个项目所设想的Haskell类型系统是基于一种统一的依赖类型编程方法，它包含了以前的扩展。这个项目的一部分涉及用一种基于依赖类型理论的语言替换GHC的核心语言，使用相关性注释来确保这些扩展是向后兼容的。此外，该项目还引入了可匹配函数，这是一个限定符，用于确定函数应用程序是否可以通过模式匹配进行分析，从而将依赖类型与GHC当前的类型推理算法集成在一起。 最后，这个项目包括一个检查的语义依赖类型的编程语言与语法。

项目成果

Seeking stability by being lazy and shallow: lazy and shallow instantiation is user friendly

通过懒惰和浅薄来寻求稳定：懒惰和浅薄的实例化是用户友好的

• DOI: 10.1145/3471874.3472985
• 发表时间: 2021
• 期刊: Haskell 2021: Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell
• 作者: Bottu, Gert-Jan;Eisenberg, Richard A.
• 通讯作者: Eisenberg, Richard A.

Partial type constructors: or, making ad hoc datatypes less ad hoc

部分类型构造函数：或者，使临时数据类型不那么临时

• DOI: 10.1145/3371108
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Jones, Mark P.;Morris, J. Garrett;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

Kind inference for datatypes

数据类型的类推论

• DOI: 10.1145/3371121
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Xie, Ningning;Eisenberg, Richard A.;Oliveira, Bruno C.
• 通讯作者: Oliveira, Bruno C.