Programming languages for scalable incremental computation and advanced gradual typing

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

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

Scalable incremental computation Software 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 typing Advances 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. Impact By 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内核。这些系统的重要性证明了核查它们的费用是合理的。然而，对于大多数应用程序来说，需求经常变化，缺陷的后果不太严重。因此，对大多数软件来说，完全验证可能仍然过于昂贵。 精化类型占据了中间位置，排除了大类的缺陷，减少了开发人员的培训和时间投资。然而，精化类型有一个传统类型系统的缺点：要么对整个程序进行类型检查，要么不检查。使打字功能更强大增加了程序员的负担，他们有时间只验证软件中最关键的部分。 渐进式类型化允许程序的不同部分根据不同的类型化级别进行检查。我们的第二个长期目标是开发工具，使语言设计者能够轻松地构建渐进类型语言。 因此，我们将开发渐进式类型化的通用机制，允许程序员选择何时何地为不同级别的类型化保证付出代价。 我们将通过对大型增量系统的逐步输入来将这两个长期目标联合收割机结合起来。 影响 通过使增量更容易实现，可扩展IC将软化性能和可维护性之间的权衡。先进的渐进类型将使程序员能够在细粒度级别上选择实际的验证量。 拟议的研究将为3名博士，2名硕士和3名本科生在学术研究和工业领域的成功职业生涯做好准备。