Gradual Typing by Annotating Flow

Web编程是一个重要的和蓬勃发展的领域，Web软件正在成为许多软件领域的主导。然而，Web编程语言几乎完全是动态类型的，动态类型语言不提供静态类型语言的速度，保证或工具支持。动态类型允许很大的灵活性，但灵活性带来了不精确性和不可预测性。静态类型更严格，这有助于软件工具，但由于可表达性变窄，它们的严格性会使初始开发变慢，有时甚至更困难。渐进类型化的目标是填补动态和静态类型之间的差距：通过使类型注释可选，但在存在的地方进行验证，可以逐渐将软件系统从动态和未检查的状态转移到静态和检查的状态。然而，渐进类型具有显著的缺点。它们引入了一系列新的可能错误。为了避免这些错误，有必要非常精确地指定类型，这既麻烦又难以理解。本研究旨在纠正静态和动态类型接口处的已知问题，同时发现和纠正尚未发现的问题。**渐进类型语言允许健全的类型，保证和分析工具，但在“动态”和“静态”世界之间创建了一个表面，引入了新的错误和新的混淆源。部分渐进类型的Web语言已经创建，但选择了一个不健全的“可选”类型系统，如TypeScript和Dart。虽然没有生成任何新的运行时错误，但这些语言是不可靠的，因此不适合许多形式的分析。我以前的工作将这些扩展到完全渐进类型，但没有解决静态和动态类型之间渐进类型可表达性的基本问题。本研究计划旨在扩展JavaScript编程语言。这项工作涉及调查和发展两个次级项目。必须添加新的构造来限制动态流导致的不完整性，并以动态方式指定类型。也有必要研究现有的方案，以确定语言变化的适用性。在这个项目成功完成后，一组扩展到网络编程语言JavaScript将可用，渐进式类型将大大提高网络软件的可维护性，同时也避免了许多阻碍以前的渐进式类型语言被采用的陷阱。这使得更有效的代码维护，更好的安全性和更快的代码扩展的Web程序。

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.