Extending the Theory and Practice of Gradual Typing

编程语言通常分为静态类型和动态类型。Java等静态类型语言使用类型来确保程序在运行之前满足基本的行为保证。类型检查捕获编程错误，并支持优化，使程序运行更快，使用更少的内存。但是，程序员必须添加额外的类型注释，并且类型检查通常会拒绝本来可以正常运行的程序。动态类型语言（如Javascript和PHP）使用运行时检查来捕获错误，因此它们支持灵活且快节奏的编程，这些编程被大量用于开发网站和移动应用程序。但在交易中，它们往往运行得更慢，占用更多内存和电力，这对移动应用来说尤其糟糕，而且已部署的程序往往存在代价高昂的错误，而这些错误本可以被类型检查器立即发现。渐进式类型是一种新的语言设计方法，它可以让程序员无缝地混合静态类型和动态类型，将静态类型语言的性能和正确性优势与动态语言的敏捷性结合起来。工业编程语言，如微软的Typescript （Javascript的扩展）和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.