conclusion]

至此，我们循着 Pierce 与 Turner 的足迹，完整地剖析了一套精巧而强大的局部类型推断机制。通过将局部类型参数合成与双向类型检查这两项核心技术相结合，我们最终完成了一个真正强大的类型检查器的设计。它不仅能在理论上驾驭如 System $F_{\le}$ 这样兼具子类型化与非直谓多态的强大类型系统，更在实践中，精准地解决了由多态、高阶编程与纯函数式风格所引发的最为普遍和恼人的类型标注问题。这套完全基于「局部性」原则的算法，其行为可预测、易于实现且错误提示友好，堪称是连接艰深理论与日常编程实践的一座典范之桥。

当然，本文所探讨的，仅是这篇经典论文的核心部分。原文的疆域更为广阔，其中最重要的扩展，便是对有界量化（Bounded Quantification）的支持。有界量化，即形如 $\forall (X \lt: T_2, Y \lt: T_2, \cdots) . e$ 的多态，它允许类型参数本身受到其超类型的约束。这一特性对于精确建模面向对象语言中的继承等高级特性至关重要，是通往更强大表达能力的必由之路。原文第五章详细阐述了如何将本文介绍的局部推断技术扩展至支持有界量化的系统。该扩展使得算法，尤其是约束的生成与求解，将变得更为精妙和复杂，特别是在处理 $\bot$ 类型与类型边界的相互作用时，引入了新的挑战。限于篇幅，对这一部分的深入剖析，或许只能留待未来的文章再行探讨。此外，本文的另一大遗憾是「形式证明」的缺失。我们关注的重点，在于阐明算法的设计动机与直觉，并以一种接近实际代码实现的方式来呈现其逻辑。为此，我们省略了诸多严谨的数学证明细节，例如约束生成算法的可靠性与完备性证明，仅以提要的形式一笔带过。

最后，值得一提的是，本文对类型系统代数性质的倚重——例如，确保任意类型间的最小上界（join）与最大下界（meet）总是存在——揭示了一条深刻的设计原则：一个具有良好代数结构的类型系统，往往更能催生出简洁而强大的类型推断算法。自这篇论文发表以来，寻求更优美的子类型化代数理论的探索从未停止。后续的研究，如 Stephen Dolan 等人提出的「代数子类型」（Algebraic Subtyping），正是沿着这一思想路径，对子类型关系的形式化进行了更为深刻的抽象与简化，在笔者看来，它是真正改变子类型研究的天才之作。当然，对这些更前沿工作的介绍，已然超出了对这篇 2000 年经典论文本身进行解读的范畴，我们把它留给未来的文章。