一句话：提出 HMQ，将 HM 类型规则重构为“前缀下的类型推断”，直接推出与 Algorithm W 一致的主类型，并简化 FreezeML、HMF 及 Koka 静态重载的形式化。
HM 类型系统的抽象规则允许 lambda 参数类型被“猜测”，这既保证了最一般类型（主类型）的存在，也使后续扩展（如 HMF、FreezeML、Boxy types 等不可谓词类型推断）必须引入复杂附加条件来维持主类型性质，而这些条件难以直接写成逻辑推导规则。本文把 HM 类型规则重新表述为“前缀下的类型推断”，称为 HMQ。HMQ 相对于 HM 类型规则是可靠且完备的，但总是推导出与 Algorithm W 推断结果对应的主类型；其规则既保留了声明式 HM 规则的清晰性，又足够具体，可以直接“读出”推断算法，因而适合作为描述类型系统扩展的基础。作者展示了如何用前缀下的推断重新描述 FreezeML 和 HMF，从而不再需要复杂附加条件，并给出了 Koka 语言中静态重载的一种新的 HMQ 形式化。
At the heart of the Damas-Hindley-Milner (HM) type system lies the abstraction rule which derives a function type for a lambda expression. In this rule, the type of the parameter can be "guessed", and can be any type that fits the derivation. The beauty of the HM system is that there always exists a most general type that encompasses all possible derivations – Algorithm W is used to infer these most general types in practice. Unfortunately, this property is also the bane of the HM type rules. Many languages extend HM typing with additional features which often require complex side conditions to the type rules to maintain principal types. For example, various type systems for impredicative type inference, like HMF, FreezeML, or Boxy types, require let-bindings to always assign most general types. Such a restriction is difficult to specify as a logical deduction rule though, as it ranges over all possible derivations. Despite these complications, the actual implementations of various type inference algorithms are usually straightforward extensions of algorithm W , and from an implementation perspective, much of the complexity of various type system extensions, like boxes or polymorphic weights, is in some sense artificial. In this article we rephrase the HM type rules as type inference under a prefix , called HMQ. HMQ is sound and complete with respect to the HM type rules, but always derives principal types that correspond to the types inferred by algorithm W. The HMQ type rules are close to the clarity of the declarative HM type rules, but also specific enough to "read off" an inference algorithm, and can form an excellent basis to describe type system extensions in practice. We show in particular how to describe the FreezeML and HMF systems in terms of inference under a prefix, and how we no longer require complex side conditions. We also show a novel formalization of static overloading in HMQ as implemented in Koka language.
@article{paperbot3117,
title = {Principal Type Inference under a Prefix: A Fresh Look at Static Overloading},
author = {Daan Leijen and Wenjia Ye},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729308}
}