揭秘 MLsub – 代数子类型的简单本质
本文深入浅出地解析了 MLsub 类型系统的核心原理——代数子类型（Algebraic Subtyping）。作者通过简洁的数学推导和直观的示例，展示了如何在保持 ML 风格类型推断简洁性的同时，引入表达力更强的子类型机制，并揭示了其背后统一的代数结构。无论你是类型系统研究者还是函数式编程爱好者，都能从中理解子类型化与参数多态如何优雅共存的本质。
背景速读
- 这篇技术文章讲解的是 "MLsub" — 一种结合了 Hindley-Milner 类型推断（函数式语言如 OCaml 和 Haskell 使用的经典系统）与子类型（subtyping）的类型系统。
- 作者 Stephen Dolan 是剑桥大学研究员，他的研究成果之一是让子类型和类型推断能够高效共存，这之前被认为是非常困难的数学问题。
- 类型推断是指编译器能自动推导出变量类型，无需程序员手动标注；子类型是指一种类型可以被当作另一种类型的实例（例如 "猫" 是 "动物" 的子类型）。
- 传统上，HM 类型推断与子类型互相冲突，导致许多实用的编程语言（如 TypeScript 或 Java）不得不放弃其一。Dolan 的工作找到了两者的优雅结合，开辟了更灵活类型系统的工程路径。
- 这篇文章是面向具备一定类型系统背景的读者的技术解读，不涉及编程教程或产品推广。