by Jiří Beneš and Jonathan Brachthäuser

In Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2025.

Abstract

Type-directed overload resolution allows the programmers to reuse the same name, offloading the work on the type-checker to disambiguate and resolve the overload. Since many programming languages implement overload resolution by performing backtracking in the type checker, it is commonly believed to be incompatible with Hindley-Milner-style type systems. In this paper, we present an approach to overload resolution that combines insights from variational type-checking and algebraic subtyping. We formalize and discuss our flow-based variational framework, which captures the essence of overloads by representing them as choices. This way, it cleanly separates constraint collection, constraint solving, and overload resolution. We believe our framework not only gives rise to more modular and efficient implementations of type-checkers, but also serves as a simpler mental model and paves the way for improved error messages.