Decidable Subtyping of Existential Types for Julia

Abstract:

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.

BibTeX:

@article{belyakova_decidable_2024,
    title = {{Decidable Subtyping of Existential Types for Julia}},
    author = {Belyakova, Julia and Chung, Benjamin and Tate, Ross and Vitek, Jan},
    year = {2024},
    journal = {{Proc. ACM Program. Lang.}},
    number = {PLDI},
    doi = {10.1145/3656421},
    pages = {191:1091--191:1114},
    url = {https://dl.acm.org/doi/10.1145/3656421},
    volume = {8},
}

Journal article