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

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

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.