SHF: Small: Collaborative Research: Foundations for Gradual Typing

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

• 批准号: 1909517
• 负责人: Daniel Licata
• 金额: $ 25万
• 依托单位: Wesleyan University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-10-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1909517&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Foundations; 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的法定任务，并使用基金会的知识分子优点和更广泛的影响审查标准，认为值得通过评估值得支持。