一句话：证明 Julia 子类型不可判定，并提出将方法签名与值类型分层的限制以恢复可判定性。
Julia 通过多重分派实现泛型库，方法声明上的类型标注在运行时用于判定方法是否适用，因此其子类型关系对语言实现至关重要。本文首先证明 Julia 的子类型判定是不可判定的；随后提出一种类型限制：将类型分层为方法签名与值类型，前者可自由使用有界存在类型，后者仅允许使用使用点方差（use-site variance），从而恢复子类型关系的可判定性。作者还进行了真实代码语料库分析，结果表明实践中几乎所有的 Julia 程序都已经满足这一限制。
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.
@article{BelyakovaCTV24,
title = {Decidable Subtyping of Existential Types for Julia},
author = {Julia Belyakova and Benjamin Chung and Ross Tate and Jan Vitek},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656421}
}