The Simple Essence of Overloading: Making Ad-Hoc Polymorphism More Algebraic with Flow-Based Variational Type-Checking

Type-directed overload resolution allows programmers to reuse the same name, offloading disambiguation to the type checker. 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 that captures the essence of overloads by representing them as choices. This 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.