SHF: Small: Collaborative Research: A Rational Reconstruction of the Julia Type System

Julia在科学计算领域是一种很有前途的语言。Julia跨越了通用和特定于领域之间的界限，以及静态类型和动态类型之间的界限。尽管只有6岁，Julia已经被下载了超过200万次，它的社区已经开发了近2000个软件包。这个项目的新奇之处在于开发了迄今为止尚未正式确定的Julia类型系统的一些基础。该项目的影响是为该语言提供一个基础良好的规范，以便程序员可以使用该规范来推理他们的代码，并由工具开发人员为Julia社区编写程序分析和转换软件。Julia支持动态类型。程序可以在没有任何类型注释的情况下编写，就像用Python编写一样。然而，Julia的类型语法及其子类型系统让人联想到现代静态类型语言，它具有结构子类型、不变名义泛型、联合类型、存在类型、协变元组、分布性和单例类型的原始组合，以及所谓的对角线规则。这个复杂的系统用于确定Julia程序的运行时行为。具体来说，它用于确定给定的多方法的哪个实现是适用的。为了确定这一点，Julia将实参的运行时类型与各种重载的参数的静态类型进行了比较。这意味着Julia类型系统的算法行为是该语言的语义、性能和使用的核心。然而，Julia使用了一些特性，比如迭代联合，而研究界还没有为这些特性开发出足够的算法。因此，Julia的类型系统目前是由C中的参考实现指定的，经过多年的性能权衡和修补语言用户提交的错误报告的需要，这个实现已经变得复杂了。因此，该项目旨在进行实验和研究，以确定实现的潜在意图是什么，将该意图公式化为类型系统，然后开发和验证实现Julia语言核心的关键算法。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Julia is an up-and-coming language in scientific computing. Julia straddles the line between being general-purpose and being domain-specific, and the line between being statically typed versus being dynamically typed. Despite being only six years old, Julia has been downloaded over 2 million times and has had nearly 2,000 packages developed by its community. The novelty of this project is to develop some of the foundations of the Julia type system which have not been formalized to date. The project's impacts are to provide a well-grounded specification to the language so that the specification can be used by programmers to reason about their code, and by tool developers to write program analysis and transformation software for the Julia community.Julia supports dynamic typing. Programs can be written without any type annotations as they would be written in, say, Python. Yet, Julia's grammar of types and its subtyping system is reminiscent of what one would expect of a modern statically typed language with an original combination of structural subtyping, invariant nominal generics, union types, existential types, covariant tuples, distributivity, and singleton types, as well as the, so-called, diagonal rule. This complex system is used to determine the run-time behavior of Julia programs. Specifically it is used to determine, for a given multimethod, which of its implementations is applicable. To make this determination, Julia compares the run-time types of arguments with the static types of the parameters of various overloadings. This means that the algorithmic behavior of Julia's type system is central to the language's semantics, performance, and usage. Yet Julia uses features, such as iterated unions, for which the research community has not yet developed adequate algorithms. As such, Julia's type system is currently specified by a reference implementation in C, one that has been made complex after years of balancing performance trade-offs with the need to patch bug reports filed by the language's users. The project, therefore, aims to perform experiments and studies to determine what the underlying intent of the implementation is, formalize that intent axiomatically as a type system, and then develop and verify the key algorithms for implementing the core of the Julia language.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.