Programming languages for scalable incremental computation and advanced gradual typing

用于可扩展增量计算和高级渐进类型的编程语言

• 批准号: RGPIN-2018-04352
• 负责人: Dunfield, Jana
• 金额: $ 2.4万
• 依托单位: Queen's University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=750616
• 关键词: Programming; languages; scalable; incremental; computation

Scalable incremental computationSoftware defects are everywhere. Slow software is also defective: a right answer is no better than a wrong one, if it takes too long. Many software systems receive similar inputs over time: compilers are often re-run after changing a single line of code. These systems can reuse previous work through incremental computation (IC).However, reusing work is difficult when the dependencies between subcomputations are subtle. Programming languages for IC automate reuse by extending languages and compilers: guided by program annotations, the compiler incrementalizes the program. This approach can achieve asymptotic speedups without extensive programmer effort.Existing approaches, however, do not work for larger systems. Our first long-term goal is to enable automatic incrementalization of large software systems, such as compilers.To achieve this goal, we will design and implement a language and semantics of incremental programs with complex structure, describing the behaviour of larger incremental systems. To understand higher-level behaviour and guide programmer understanding, we will design and implement type systems that check invariants of incremental programs.Advanced gradual typingAdvances in formal verification have led to fully verified software, such as the CompCert C compiler and the seL4 OS kernel. The importance of such systems justifies the expense of verifying them. For most applications, however, requirements change often and defects' consequences are less severe. Thus, full verification will probably remain too expensive for most software.Refinement typing occupies the middle ground, ruling out large categories of defects with less developer investment of training and time. However, refinement typing shares a drawback of traditional type systems: either the entire program type-checks, or it doesn't. Making typing more powerful increases the burden on programmers who have time to verify only the most critical parts of their software.Gradual typing allows different parts of a program to be checked against different levels of typing. Our second long-term goal is to develop tools that enable language designers to build gradually typed languages easily.Thus, we will develop general mechanisms for gradual typing that allow programmers to choose when and where to pay the price for different levels of typing guarantees.We will combine both long-term goals through gradual typing for large incremental systems.ImpactBy making incrementality easier to achieve, scalable IC will soften the tradeoff between performance and maintainability. Advanced gradual typing will enable programmers to choose a practical amount of verification at a fine-grained level.The proposed research will prepare 3 PhD, 2 MSc and 3 undergraduate students for successful careers in both academic research and industry.

可伸缩的增量计算软件缺陷无处不在。速度慢的软件也有缺陷：如果花费的时间太长，正确的答案并不比错误的好。随着时间的推移，许多软件系统都会收到类似的输入：编译器经常在更改一行代码后重新运行。这些系统可以通过增量计算（IC）重用以前的工作，但是，当子计算之间的依赖关系很微妙时，重用工作是困难的。集成电路编程语言通过扩展语言和编译器自动重用：在程序注释的指导下，编译器递增程序。这种方法不需要程序员大量的工作就可以获得渐进的加速比，但是现有的方法并不适用于大型系统。我们的第一个长期目标是实现大型软件系统（如编译器）的自动增量化。为了实现这一目标，我们将设计和实现一种具有复杂结构的增量程序语言和语义，描述大型增量系统的行为。为了理解更高层次的行为和指导程序员的理解，我们将设计和实现类型系统，检查增量程序的不变量。先进的渐进式类型化在形式验证的进步已经导致完全验证的软件，如CompCert C编译器和seL4 OS内核。这些系统的重要性证明了核查它们的费用是合理的。然而，对于大多数应用程序来说，需求经常变化，缺陷的后果不太严重。因此，对于大多数软件来说，完全验证可能仍然过于昂贵。细化类型占据中间立场，排除了大类别的缺陷，同时减少了开发人员的培训和时间投资。然而，精化类型有一个传统类型系统的缺点：要么对整个程序进行类型检查，要么不检查。使类型更强大增加了程序员的负担，他们有时间只验证软件中最关键的部分。渐进类型允许根据不同的类型级别来检查程序的不同部分。我们的第二个长期目标是开发工具，使语言设计者能够轻松地构建渐进类型的语言。因此，我们将开发渐进类型的通用机制，允许程序员选择何时何地为不同级别的类型保证付出代价。我们将通过渐进类型为大型增量系统联合收割机这两个长期目标。影响通过使增量更容易实现，可扩展的集成电路将软化性能和可维护性之间的权衡。先进的渐进式打字将使程序员能够在细粒度级别上选择实际数量的验证。拟议的研究将为3名博士，2名硕士和3名本科生在学术研究和工业领域的成功职业生涯做好准备。