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

Julia是科学计算领域一门很有前途的语言。Julia跨越了通用和特定领域之间的界限，以及静态类型化和动态类型化之间的界限。尽管朱莉娅只有六岁，但她已经被下载了200多万次，社区开发了近2000个包。这个项目的新奇之处在于开发了Julia类型系统的一些基础，这些基础到目前为止还没有正式确定下来。该项目的影响是为该语言提供了一个基础良好的规范，以便程序员可以使用该规范来推理他们的代码，并供工具开发人员为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.