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.

类型安全编程语言在程序将操作应用于错误类型的数据时报告错误-例如，列表长度的操作需要一个列表，而不是一个数字-它们有两种类型：动态类型(或非类型)语言，它在运行时捕获此类类型错误；静态类型语言，在程序运行之前，在编译时捕获类型错误。动态类型化语言非常适合软件的快速原型开发，而静态类型化则随着软件系统的发展而变得重要，因为它提供了改进的可维护性、代码文档、早期错误检测以及对编译为更快代码的支持。逐渐类型化的语言将这些好处结合在一起，允许动态类型化代码和静态类型化代码-更广泛地说，不太精确和更精确的类型化代码--共存和互操作，从而允许程序员慢慢地将他们的代码库的部分从较不精确的类型化演变为更精确的类型化。为了确保安全的互操作性，当具有不太精确的类型的数据被转换为更精确的类型时，逐步的语言插入运行时检查。渐进式打字已经在行业中得到了高度的采用，在诸如TypeScrip、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.