Extending the Theory and Practice of Gradual Typing

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

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.