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

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

• 批准号: 1703835
• 负责人: Stephanie Weirich
• 金额: $ 63.87万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-07-01 至 2022-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1703835&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）的整合的见解，以及对创建正确软件的数学原理的更深入的了解。该项目的重要性和重要性是首次使技术行业获得依赖类型，同时为学生（包括一名主要研究人员的本科妇女学院的学生创造机会）与该技术互动。该项目包括实用和基础组成部分。 Glasgow Haskell编译器（GHC）8.0版中实现的Haskell类型系统能够通过使用许多语言扩展来模拟相关类型。但是，此用途需要尴尬的编码，并且支持它们的扩展使语言变得复杂。相比之下，该项目设想的Haskell类型系统基于一种统一的方法，用于依赖于先前扩展的依赖类型的编程。该项目的一部分涉及使用相关注释以确保这些扩展为向后兼容的相关注释，将GHC的核心语言用一种基于依赖类型理论替换。此外，该项目还引入了可匹配的功能，该功能可以通过模式匹配来确定是否可以通过模式匹配来分析功能应用程序，从而使依赖类型与GHC的当前类型推理算法的集成。 最后，该项目包括对有局部性的相关编程语言的语义检查。

项目成果

Composing effects into tasks and workflows

• DOI: 10.1145/3406088.3409023
• 发表时间: 2020-08
• 期刊: Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell
• 作者: Yves Parès;Jean-Philippe Bernardy;R. Eisenberg

Eta-equivalence in Core Dependent Haskell

核心依赖 Haskell 中的 eta 等价

• DOI: 10.4230/lipics.types.2019.7
• 发表时间: 2020
• 期刊: Leibniz international proceedings in informatics
• 作者: Kravchuk-Kirilyuk, Anastasiya;Voizard, Antoine;Weirich, Stephanie
• 通讯作者: Weirich, Stephanie

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.

Stitch: the sound type-indexed type checker (functional pearl)

针迹：音型索引型格子（功能性珍珠）

• DOI: 10.1145/3406088.3409015
• 发表时间: 2020
• 期刊: Haskell 2020: Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell
• 作者: Eisenberg, Richard A.

A Dependent Dependency Calculus

依赖依赖演算

• DOI: 10.1007/978-3-030-99336-8_15
• 发表时间: 2022
• 期刊: Lecture notes in computer science
• 作者: Choudhury, Pritam;Eades III, Harley;Weirich, Stephanie
• 通讯作者: Weirich, Stephanie