一句话：提出用子类型约束刻画数据流，将类型错误解释为错误数据流并展示相关程序位置，改进约束类型推断的错误信息。
针对基于约束的类型推断系统，类型错误信息通常反映底层约束求解算法的实现细节，而非导致类型不匹配的具体因素，因此难以帮助程序员定位和理解错误。本文提出使用刻画数据流的子类型约束来分类并解释类型错误，将错误归因于错误的数据流，并以相关程序位置序列的形式展示出来。该方法不限于支持子类型的语言，也可集成到 Hindley-Milner 类型推断中。作者还开展用户研究，比较所提错误信息与其他实现的质量。定量评估未显示基于数据流的消息在错误定位或原因理解上有显著提升，但定性评估表明程序员对此类消息存在真实需求。
Creating good type error messages for constraint-based type inference systems is difficult. Typical type error messages reflect implementation details of the underlying constraint-solving algorithms rather than the specific factors leading to type mismatches. We propose using subtyping constraints that capture data flow to classify and explain type errors. Our algorithm explains type errors as faulty data flows, which programmers are already used to reasoning about, and illustrates these data flows as sequences of relevant program locations. We show that our ideas and algorithm are not limited to languages with subtyping, as they can be readily integrated with Hindley-Milner type inference. In addition to these core contributions, we present the results of a user study to evaluate the quality of our messages compared to other implementations. While the quantitative evaluation does not show that flow-based messages improve the localization or understanding of the causes of type errors, the qualitative evaluation suggests a real need and demand for flow-based messages.
@article{paperbot1893,
title = {Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference},
author = {Ishan Bhanuka and Lionel Parreaux and David Binder and Jonathan Immanuel Brachthäuser},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622812}
}