一句话：提出 Simple-sub，以更直观的算法实现 MLsub 的带子类型主类型推断，并实验验证两者一致。
MLsub 将 Hindley-Milner 推断扩展到子类型，同时保持紧凑的主类型，但其 biunification 规范依赖 bisubstitution、polar types 和抽象代数，难以理解。本文指出这些概念并非理解 MLsub 机制所必需，提出替代算法 Simple-sub。它不到 500 行代码即可高效实现，包含解析、简化和漂亮打印，形式更熟悉、更易理解。作者在百万个随机生成且良好作用域的表达式上对比 Simple-sub 与 MLsub，二者结果一致；该评估还发现 MLsub 可变自动机实现中的若干 bug。文章基于类型系统的句法规范给出了 Simple-sub 的 soundness 与 completeness 论证思路，面向新类型系统和语言设计者，形式化程度轻、洞见丰富。
MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bisubstitution and polar types, and making use of advanced notions from abstract algebra. In this paper, we show that these are in fact not essential to understanding the mechanisms at play in MLsub. We propose an alternative algorithm called Simple-sub, which can be implemented efficiently in under 500 lines of code (including parsing, simplification, and pretty-printing), looks more familiar, and is easier to understand. We present an experimental evaluation of Simple-sub against MLsub on a million randomly-generated well-scoped expressions, showing that the two systems agree. The mutable automaton-based implementation of MLsub is quite far from its algebraic specification, leaving a lot of space for errors; in fact, our evaluation uncovered several bugs in it. We sketch more straightforward soundness and completeness arguments for Simple-sub, based on a syntactic specification of the type system. This paper is meant to be light in formalism, rich in insights, and easy to consume for prospective designers of new type systems and programming languages. In particular, no abstract algebra is inflicted on readers.
@article{Parreaux20,
title = {The simple essence of algebraic subtyping: principal type inference with subtyping made easy (functional pearl)},
author = {Lionel Parreaux},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3409006}
}