Decidable subtyping for Julia (2021–…)

Decidable subtyping for the Julia language.

Questions/comments/feedback

If you have any questions or comments about the project or related papers, please, feel free to email me or submit your feedback using this Google form. I would be happy to answer questions that you might have, learn about what is unclear or confusing, or receive any other feedback.

The main publication, PLDI 2024, presents a sound and complete subtyping algorithm for a restricted grammar of a subset of the Julia types, which include bounded existential types. The restricted types are stratified as method signatures (which can use bounded existential types freely) over value types (which are restricted to use-site variance).

The PhD thesis extends the subtyping algorithm with distributivity in a sound but incomplete manner. The thesis also covers nominal subtyping between user-defined datatypes.

An empirical study of the source code of registered Julia packages shows that nearly all type annotations written in practice already conform to the proposed stratification. However, more work needs to be done to evaluate its potential effect on the language runtime.

Status: this is an ongoing work; for updates on this project, see GitHub.

Publications

PLDI 2024
Decidable Subtyping of Existential Types for Julia
Authors: Julia Belyakova, Benjamin Chung, Ross Tate, Jan Vitek
DOI: 10.1145/3656421
Venue: Proc. ACM Program. Lang., Volume 8, PLDI, Article 191 (24 pages)
Reviews

Julia is a modern scientific-computing language that relies on multiple dispatch to implement generic libraries. While the language does not have a static type system, method declarations are decorated with expressive type annotations to determine when they are applicable. To find applicable methods, the implementation uses subtyping at run-time. We show that Julia’s subtyping is undecidable, and we propose a restriction on types to recover decidability by stratifying types into method signatures over value types—where the former can freely use bounded existential types but the latter are restricted to use-site variance. A corpus analysis suggests that nearly all Julia programs written in practice already conform to this restriction.
PhD Thesis:
Decidable Subtyping of Existential Types for the Julia Language ^🔗

Authors: Julia Belyakova
Venue: Northeastern University ProQuest Dissertations Publishing, 2023

Julia is a dynamic, high-performance programming language for scientific computing. To encourage a high level of code reuse and extensibility, Julia is designed around symmetric multiple dynamic dispatch, which allows functions to have multiple implementations tailored to different argument types. To resolve multiple dispatch, Julia relies on a subtype relation over a complex language of run-time types and type annotations, which include set-theoretic unions, distributive tuples, parametric invariant types, and impredicative existential types. Notably, subtyping in Julia is undecidable, which manifests with a run-time stack-overflow error when program execution encounters a subtyping query that causes the subtype checker to loop. In this dissertation, I propose a decidable subtype relation for a restricted language of Julia types where existential types inside invariant constructors are limited to ones expressible with use-site variance. To estimate the migration effort that would be required for switching to the restricted type language, I analyze type annotations in the corpus of 9K registered Julia packages. Out of 2M statically identifiable type annotations in the corpus, 99.99% satisfy the restriction, making it a viable candidate for evolving Julia towards decidable subtyping.