SHF: Small: Collaborative Research: Foundations for Gradual Typing

SHF：小型：协作研究：渐进打字的基础

• 批准号: 1910522
• 负责人: Amal Ahmed
• 金额: $ 25万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-10-01 至 2022-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1910522&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Foundations

Type-safe programming languages report errors when a program applies operations to data of the wrong type---e.g., a list-length operation expects a list, not a number---and they come in two flavors: dynamically typed (or untyped) languages, which catch such type errors at run time, and statically typed languages, which catch type errors at compile time before the program is ever run. Dynamically typed languages are well suited for rapid prototyping of software, while static typing becomes important as software systems grow since it offers improved maintainability, code documentation, early error detection, and support for compilation to faster code. Gradually typed languages bring together these benefits, allowing dynamically typed and statically typed code---and more generally, less precisely and more precisely typed code---to coexist and interoperate, thus allowing programmers to slowly evolve parts of their code base from less precisely typed to more precisely typed. To ensure safe interoperability, gradual languages insert runtime checks when data with a less precise type is cast to a more precise type. Gradual typing has seen high adoption in industry, in languages like TypeScript, Hack, Flow, and C#. Unfortunately, current gradually typed languages fall short in three ways. First, while normal static typing provides reasoning principles that enable safe program transformations and optimizations, naive gradual systems often do not. Second, gradual languages rarely guarantee graduality, a reasoning principle helpful to programmers, which says that making types more precise in a program merely adds in checks and the program otherwise behaves as before. Third, time and space efficiency of the runtime casts inserted by gradual languages remains a concern. This project addresses all three of these issues. The project's novelties include: (1) a new approach to the design of gradual languages by first codifying the desired reasoning principles for the language using a program logic called Gradual Type Theory (GTT), and from that deriving the behavior of runtime casts; (2) compiling to a non-gradual compiler intermediate representation (IR) in a way that preserves these principles; and (3) the ability to use GTT to reason about the correctness of optimizations and efficient implementation of casts. The project has the potential for significant impact on industrial software development since gradually typed languages provide a migration path from existing dynamically typed codebases to more maintainable statically typed code, and from traditional static types to more precise types, providing a mechanism for increased adoption of advanced type features. The project will also have impact by providing infrastructure for future language designs and investigations into improving the performance of gradual typing.The project team will apply the GTT approach to investigate gradual typing for polymorphism with data abstraction (parametricity), algebraic effects and handlers, and refinement/dependent types. For each, the team will develop cast calculi and program logics expressing better equational reasoning principles than previous proposals, with certified elaboration to a compiler intermediate language based on Call-By-Push-Value (CBPV) while preserving these properties, and design convenient surface languages that elaborate into them. The GTT program logics will be used for program verification, proving the correctness of program optimizations and refactorings.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

当程序对错误类型的数据应用操作时，类型安全的编程语言会报告错误——例如，列表长度操作需要一个列表，而不是一个数字——它们有两种类型：动态类型（或非类型） ）语言，在运行时捕获此类类型错误；静态类型语言，在程序运行之前在编译时捕获类型错误。 动态类型语言非常适合软件的快速原型设计，而静态类型随着软件系统的发展而变得重要，因为它提供了改进的可维护性、代码文档、早期错误检测以及对编译为更快代码的支持。 渐进类型语言将这些优点结合在一起，允许动态类型和静态类型代码（以及更一般地，不太精确和更精确类型的代码）共存和互操作，从而允许程序员从更少的代码慢慢发展其部分代码库。精确打字到更精确打字。 为了确保安全的互操作性，当将不太精确类型的数据转换为更精确的类型时，渐进语言会插入运行时检查。渐进式打字在业界得到了广泛采用，例如 TypeScript、Hack、Flow 和 C# 等语言。 不幸的是，当前的渐进类型语言在三个方面存在缺陷。首先，虽然普通的静态类型提供了能够实现安全程序转换和优化的推理原则，但朴素的渐进系统通常无法做到这一点。其次，渐进式语言很少保证渐进性，这是一种对程序员有帮助的推理原则，它表示在程序中使类型更精确只会添加检查，而程序在其他方面的行为与以前一样。第三，渐进语言插入的运行时转换的时间和空间效率仍然是一个问题。 该项目解决了所有这三个问题。 该项目的新颖之处包括：（1）一种设计渐进语言的新方法，首先使用称为渐进类型理论（GTT）的程序逻辑来编纂该语言所需的推理原则，并从中导出运行时强制转换的行为； (2) 以保留这些原则的方式编译为非渐进编译器中间表示 (IR)； (3) 能够使用 GTT 来推断优化的正确性和强制转换的高效实现。该项目有可能对工业软件开发产生重大影响，因为逐步类型化语言提供了从现有动态类型代码库到​​更可维护的静态类型代码、从传统静态类型到更精确类型的迁移路径，提供了一种增加采用先进技术的机制。类型特征。 该项目还将通过为未来的语言设计和改进渐进式打字性能的研究提供基础设施来产生影响。项目团队将应用 GTT 方法来研究具有数据抽象（参数性）、代数效应和处理程序的多态性的渐进式打字细化/依赖类型。 对于每一个，该团队将开发铸造演算和程序逻辑，表达比以前的提案更好的等式推理原理，并通过认证详细阐述基于按推值调用（CBPV）的编译器中间语言，同时保留这些属性，并设计方便的表面详细阐述它们的语言。 GTT程序逻辑将用于程序验证，证明程序优化和重构的正确性。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，认为值得支持。

项目成果

Gradual type theory

渐进式理论

• DOI: 10.1017/s0956796821000125
• 发表时间: 2021
• 期刊: Journal of Functional Programming
• 影响因子: 1.1
• 作者: NEW, MAX S.;LICATA, DANIEL R.;AHMED, AMAL
• 通讯作者: AHMED, AMAL

Graduality and parametricity: together again for the first time

渐进性和参数化：首次再次结合在一起

• DOI: 10.1145/3371114
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: New, Max S.;Jamner, Dustin;Ahmed, Amal
• 通讯作者: Ahmed, Amal

Call-by-name Gradual Type Theory

点名渐进型理论

• DOI: 10.23638/lmcs-16(1:7)2020
• 发表时间: 2020
• 期刊: Logical methods in computer science
• 影响因子: 0.6
• 作者: New, Max S.;Licata, Daniel R.
• 通讯作者: Licata, Daniel R.