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

点击翻译按钮获取中文摘要

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.