Gradual Typing by Annotating Flow

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