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）重用以前的工作。但是，当子计算之间的依赖关系很微妙时，重用工作就很困难。 IC 编程语言通过扩展语言和编译器来自动重用：在程序注释的指导下，编译器增量化程序。这种方法无需程序员大量工作即可实现渐近加速。但是，现有方法不适用于较大的系统。我们的第一个长期目标是实现大型软件系统（例如编译器）的自动增量化。为了实现这一目标，我们将设计和实现一种具有复杂结构的增量程序的语言和语义，描述更大的增量系统的行为。为了理解更高层次的行为并指导程序员的理解，我们将设计和实现检查增量程序不变量的类型系统。高级渐进式类型化形式验证的进步带来了经过充分验证的软件，例如 CompCert C 编译器和 seL4 OS 内核。此类系统的重要性证明了验证它们的费用是合理的。然而，对于大多数应用来说，需求经常变化，缺陷的后果也不太严重。因此，对于大多数软件来说，全面验证可能仍然过于昂贵。细化类型占据中间立场，以较少的开发人员培训和时间投入排除大类缺陷。然而，细化类型与传统类型系统有一个共同的缺点：要么对整个程序进行类型检查，要么不进行类型检查。让打字变得更强大会增加程序员的负担，因为他们有时间只验证软件最关键的部分。渐进打字允许根据不同级别的打字检查程序的不同部分。我们的第二个长期目标是开发工具，使语言设计者能够轻松构建渐进类型语言。因此，我们将开发渐进类型的通用机制，允许程序员选择何时何地为不同级别的类型保证付出代价。我们将通过大型增量系统的渐进类型将这两个长期目标结合起来。影响通过使增量更容易实现，可扩展 IC 将软化性能和可维护性之间的权衡。高级渐进式打字将使程序员能够在细粒度水平上选择实际的验证量。拟议的研究将为 3 名博士生、2 名硕士生和 3 名本科生在学术研究和行业的成功职业生涯做好准备。