Gradual Typing by Annotating Flow

点击翻译按钮获取中文摘要

Web programming is a vital and thriving field, and web software is becoming dominant in many software domains. However, web programming languages are almost exclusively dynamically typed, and dynamically typed languages do not offer the speed, assurance or tool support of statically typed languages.******Dynamic types allow a lot of flexibility, but with flexibility comes imprecision and unpredictability. Static types are more rigid, and this aids software tools, but their rigidity can make initial development slower and sometimes more difficult, due to narrowing expressibility. Gradual typing aims to fill the gap between dynamic and static types: By making type annotations optional, but validated where present, it is possible to gradually move a software system from dynamic and unchecked to static and checked. However, gradual types have significant drawbacks. They introduce a new range of possible errors. To avoid these errors, it is necessary to specify types very precisely, which is both cumbersome and hard to understand. This research aims to rectify the known problems at the interface of static and dynamic types, and discover and rectify the as-yet-unknown problems as well.******Gradually-typed languages allow sound typing, assurance and analysis tools, but create a surface between the "dynamic" and "static" worlds, introducing new errors and a new source for confusion. Partially-gradually-typed languages for the web have been created, but opting for an unsound "optional" type system, as in TypeScript and Dart. Although not generating any new runtime errors, these languages are unsound, and so not suitable for many forms of analysis. My previous work extends these to be fully gradually typed, but does not solve the fundamental problem of gradual typing's expressibility at the boundary between static and dynamic types.******This research program aims to extend the JavaScript programming language. This work involves both investigative and developmental sub-projects. New constructs must be added to restrict the incompleteness caused by dynamic flows and specify types in a dynamic way. It is also necessary to study existing programs to determine the applicability of language changes.******Upon the successful completion of this project, a set of extensions to the web programming language JavaScript will be available, with gradual typing which will greatly improve the maintainability of web software, while also avoiding many of the pitfalls that have hindered previous gradually-typed languages from being adopted. This enables more efficient code maintenance, better security and faster code extension for web programs.