Extending the Theory and Practice of 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.