一句话：首次系统形式化类型推断实现中广泛使用的 levels 技术，并说明其可用于实际类型推断实现。
现代函数式语言依赖复杂的类型推断算法，但理论表述与工程实现之间存在鸿沟：实现常采用形式规范未涵盖的技术，导致开发者困惑，且理论保证未必适用于实现。本文聚焦其中一种名为 levels 的技术。该技术在实践中被广泛使用，却缺乏理论研究。作者首次对 levels 进行全面形式化，并展示其如何应用于类型推断实现，从而弥合形式规范与实现之间的差距。摘要未报告具体实验评估。
Modern functional languages rely on sophisticated type inference algorithms. However, there often exists a gap between the theoretical presentation of these algorithms and their practical implementations. Specifically, implementations employ techniques not explicitly included in formal specifications, causing undesirable consequences. First, this leads to confusion and unforeseen challenges for developers adhering to the formal specification. Moreover, theoretical guarantees established for a formal presentation may not directly translate to the implementation. This paper focuses on formalizing one such technique, known as levels , which is widely used in practice but whose theoretical treatment remains largely understudied. We present the first comprehensive formalization of levels and demonstrate their applicability to type inference implementations.