August 30, 2024
This talk is a slightly extended version of the PLDI 2024 presentation. Before diving into the main part, we will start with a brief discussion of several concepts relevant to the technical content of the talk: inference rules, transitivity, and decidability. We will also take a quick look at the Julia language.
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.
About Julia Belyakova
Julia Belyakova is a postdoctoral researcher at Purdue University, working with Suresh Jagannathan. Julia received her PhD at Northeastern University, where she worked with Jan Vitek on formalizing various aspects of the Julia language.