The Julia programming language was designed to fill the needs of scientific computing by combining the benefits of productivity and performance languages. Julia allows users to write untyped scripts easily without needing to worry about many implementation details, as do other productivity languages. If one just wants to get the work done-regardless of how efficient or general the program might be, such a paradigm is ideal. Simultaneously, Julia also allows library developers to write efficient generic code that can run as fast as implementations in performance languages such as C or Fortran. This combination of user-facing ease and library developer-facing performance has proven quite attractive, and the language has increasing adoption. With adoption comes combinatorial challenges to correctness. Multiple dispatch -- Julia's key mechanism for abstraction -- allows many libraries to compose "out of the box." However, it creates bugs where one library's requirements do not match what another provides. Typing could address this at the cost of Julia's flexibility for scripting. I developed a "best of both worlds" solution: gradual typing for Julia. My system forms the core of a gradual type system for Julia, laying the foundation for improving the correctness of Julia programs while not getting in the way of script writers. My framework allows methods to be individually typed or untyped, allowing users to write untyped code that interacts with typed library code and vice versa. Typed methods then get a soundness guarantee that is robust in the presence of both dynamically typed code and dynamically generated definitions. I additionally describe protocols, a mechanism for typing abstraction over concrete implementation that accommodates one common pattern in Julia libraries, and describe its implementation into my typed Julia framework.

翻译：Julia 编程语言旨在通过融合生产力和性能语言的优势来满足科学计算的需求。与其他生产力语言类似，Julia 允许用户轻松编写无类型脚本，而无需担心许多实现细节。如果用户只想完成任务——无论程序效率或通用性如何——这种范式都是理想的。同时，Julia 也允许库开发者编写高效的泛型代码，其运行速度可与 C 或 Fortran 等性能语言的实现相媲美。这种面向用户的易用性与面向库开发者的性能的组合已被证明极具吸引力，该语言的采用率也在不断增长。然而，随着采用率的提升，正确性方面也面临着组合性挑战。多重分派——Julia 实现抽象的关键机制——允许许多库实现“即开即用”的组合，但这也会导致一个库的需求与另一个库的提供不匹配的缺陷。类型化可以解决这一问题，但代价是牺牲 Julia 在脚本编写中的灵活性。我开发了一种“两全其美”的解决方案：Julia 的渐进类型化。我的系统构成了 Julia 渐进类型系统的核心，为提高 Julia 程序的正确性奠定了基础，同时不会干扰脚本编写者。该框架允许方法单独进行类型化或无类型化，使用户能够编写无类型代码与类型化库代码交互，反之亦然。类型化方法随后会获得健全性保证，该保证在动态类型代码和动态生成定义并存的情况下依然稳健。此外，我还描述了协议——一种对具体实现进行抽象类型化的机制，可适应 Julia 库中的一种常见模式，并说明了其在类型化 Julia 框架中的实现。