2026-08-12 –, Room 1
JuliaSubtyping is a new implementation of Julia's core subtyping (and intersection / type-subtraction) algorithms. This talk will motivate the new implementation and explore the theory behind its operation.
Despite being built on complex theory (SAT solvers, QBF, and more), the new design attempts to be more performant and transparently correct than Julia's existing implementation, while also being straightforward to extend with new kinds of reasoning. At the heart of the design a "logical core" is combined with a "type logic" to form the basis of the algorithm and provides semantics rich enough to describe many interesting subtyping algorithms.
You can of course expect many challenges along the way. Every theoretician's favorite enemy (undecidability) will rear its head along our journey, along with other practical engineering trade-offs. We'll investigate performance and demonstrate how the new algorithm stands with respect to the old. Finally we'll speculate about what new types of compiler reasoning this kind of typing algorithm may one day support.
A compiler engineer at JuliaHub.