一句话：提出基于流的变分类型检查框架，将重载视为选择，统一约束收集、求解与重载消解。
重载消解依靠类型导向，让程序员复用同名标识符并把歧义交给类型检查器。但许多语言在类型检查中回溯以处理重载，这使其常被视为与 Hindley-Milner 风格类型系统不兼容。本文结合变分类型检查与代数子类型，提出基于流的变分框架，将重载本质地表示为选择（choice），从而清晰分离约束收集、约束求解与重载消解。作者形式化并讨论了该框架，认为它可带来更模块化、更高效的类型检查器实现，同时提供更简单的心智模型，并为改进错误信息铺路。
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.
@article{paperbot2907,
title = {The Simple Essence of Overloading: Making Ad-Hoc Polymorphism More Algebraic with Flow-Based Variational Type-Checking},
author = {Jiří Beneš and Jonathan Immanuel Brachthäuser},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763168}
}