Gradual Typing by Annotating Flow

Web编程是一个重要且蓬勃发展的领域，Web软件正在许多软件领域占据主导地位。然而，Web编程语言几乎完全是动态类型化的，并且动态类型化语言不提供静态类型化语言的速度、保证或工具支持。 动态类型允许很大的灵活性，但随之而来的是不精确性和不可预测性。静态类型更严格，这有助于软件工具，但它们的僵化可能会使初始开发变得更慢，有时还会因为表达能力的缩小而变得更加困难。渐进式类型旨在填补动态类型和静态类型之间的空白：通过使类型注释成为可选的，但在存在的情况下经过验证，可以将软件系统从动态的、未检查的逐渐移动到静态的、检查的。然而，渐进型有很大的缺点。它们引入了一系列新的可能的错误。为了避免这些错误，必须非常精确地指定类型，这既繁琐又难以理解。本研究的目的是纠正静态和动态类型界面上的已知问题，并发现和纠正未知的问题。 渐进式语言允许健全的打字、保证和分析工具，但在“动态”和“静态”世界之间制造了一个表面，引入了新的错误和混乱的新来源。已经为网络创建了部分渐进类型的语言，但选择了一种不健全的“可选”类型系统，如TypeScrip和DART。尽管不会生成任何新的运行时错误，但这些语言并不健全，因此不适合许多形式的分析。我以前的工作将这些扩展为完全渐进式类型，但没有解决渐进式类型在静态类型和动态类型之间的边界上的可表现性这一根本问题。 本研究项目旨在扩展Java的编程语言。这项工作既涉及调查项目，也涉及发展子项目。必须添加新的构造，以限制动态流造成的不完整性，并以动态方式指定类型。还有必要研究现有的程序，以确定语言变化的适用性。 在这个项目成功完成后，将有一套网络编程语言的扩展，包括逐步打字，这将极大地改善网络软件的可维护性，同时也避免了许多阻碍以前逐步打字语言被采用的陷阱。这为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.