Julia Belyakova

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.