SHF: Small: Collaborative Research: Foundations for Gradual Typing

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

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.