Extending the Theory and Practice of Gradual Typing

扩展渐进打字的理论和实践

• 批准号: RGPIN-2017-04471
• 负责人: Garcia, Ronald
• 金额: $ 1.89万
• 依托单位: University of British Columbia
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=711069
• 关键词: Extending; Theory; Practice; Gradual; Typing

Programming languages are typically categorized as either statically or dynamically typed. Statically typed languages such as Java use types to ensure that a program satisfies basic behavioural guarantees before running it. Type checking catches programming errors and supports optimizations that make programs run faster and use less memory. However, programmers must add extra type annotations, and type checking often rejects programs that would otherwise run correctly. Dynamically typed languages such as Javascript and PHP use runtime checks to catch errors, so they enable flexible and fast-paced programming that is heavily used to develop web sites and mobile applications. But in trade they tend to run slower and use more memory and power, which is particularly bad for mobile apps, and deployed programs often harbour costly bugs that could have been detected right away by a type checker. Gradual typing is a new approach to language design that lets programmers seamlessly mix static and dynamic typing, combining the performance and correctness benefits of statically typed languages with the agility of dynamic languages. Industrial programming languages, such as Microsoft's Typescript (an extension of Javascript) and Facebook's Hack (an extension of PHP), now provide some support for gradual typing, while researchers in academia continue to develop its theory. My research program focuses on developing the theoretical foundations of gradual typing so as to inform the design and implementation of gradually typed languages. The results of this work have been promising, but more work is needed to make these ideas applicable to industrial-strength languages. This proposal outlines three objectives that will advance the state-of-the-art in gradual typing. First, we will develop a general theory for improving how gradually-typed languages use static type information to systematically decrease the overhead of checking programs at runtime. Second, we will extend the foundations of gradual typing to apply to type systems that guarantee not just what kinds of values computations produce, but also how computations interact with one another, assuring properties such as the confidentiality of private data and control over access to privileged resources. Third, we will develop and validate techniques for constructing high-performance and space-efficient compilers for languages that want to incorporate gradual typing by design. This research has the potential to fundamentally improve how programming languages are designed and implemented, and bridge the longstanding gap between high-confidence and agile approaches to software construction.

编程语言通常分为静态类型和动态类型。 静态类型语言（例如 Java）使用类型来确保程序在运行之前满足基本的行为保证。 类型检查可以捕获编程错误并支持优化，使程序运行得更快并使用更少的内存。然而，程序员必须添加额外的类型注释，并且类型检查通常会拒绝原本可以正确运行的程序。 Javascript 和 PHP 等动态类型语言使用运行时检查来捕获错误，因此它们可以实现灵活且快节奏的编程，广泛用于开发网站和移动应用程序。但实际上，它们往往运行速度较慢，使用更多内存和电量，这对移动应用程序尤其不利，而且部署的程序通常含有代价高昂的错误，这些错误本来可以被类型检查器立即检测到。 渐进类型是一种新的语言设计方法，它允许程序员无缝地混合静态和动态类型，将静态类型语言的性能和正确性优势与动态语言的敏捷性结合起来。 工业编程语言，例如微软的 Typescript（Javascript 的扩展）和 Facebook 的 Hack（PHP 的扩展），现在为渐进式打字提供了一些支持，而学术界的研究人员也在继续发展其理论。 我的研究项目侧重于发展渐进式打字的理论基础，以便为渐进式打字语言的设计和实现提供信息。 这项工作的结果很有希望，但需要做更多的工作才能使这些想法适用于工业强度的语言。 该提案概述了三个目标，这些目标将推动渐进打字技术的发展。 首先，我们将开发一种通用理论，用于改进渐进类型语言如何使用静态类型信息来系统地减少运行时检查程序的开销。 其次，我们将扩展渐进类型的基础，以应用于类型系统，不仅保证计算产生什么类型的值，还保证计算如何相互交互，确保私有数据的机密性和对特权资源访问的控制等属性。 第三，我们将开发和验证为想要通过设计纳入渐进类型的语言构建高性能和节省空间的编译器的技术。 这项研究有可能从根本上改善编程语言的设计和实现方式，并弥合高可信度和敏捷软件构建方法之间长期存在的差距。