类型推断

类型推断自动重建表达式的类型，允许程序员省略类型标注，而编译器则计算出最通用的类型。

Definition

类型推断（type reconstruction）是根据表达式的结构和用法，推导出其有效且最通用类型的过程，而无需程序员提供所有类型标注。

Scope

本主题涵盖了在没有显式标注的情况下推断类型的算法和理论，重点是Hindley-Milner系统和使用统一（unification）与let多态（let-polymorphism）的算法W。它涉及主类型（principal types）、可判定性（decidability）和复杂性，以及将推断扩展到具有子类型（subtyping）、高阶多态（higher-rank polymorphism）或依赖类型（dependent types）的更丰富系统所面临的困难。

Core questions

• 当没有写入类型时，编译器如何重建类型？
• 什么是主类型，以及它何时总是存在？
• 统一如何驱动Hindley-Milner类型推断？
• 为什么在更丰富的类型系统中，类型推断会变得不可判定或不完整？

Key theories

Hindley-Milner类型推断

Milner的多态类型规程，连同算法W，使用统一为带有let绑定多态的lambda演算推断类型，构成了ML家族语言中类型推断的基础。

主类型方案

Damas和Milner证明，每个可类型化的表达式都具有一个主类型方案，即所有有效类型都是其实例的最通用类型，并且算法W能够计算出它。

组合逻辑中的主类型

Hindley确立了可类型化项存在主类型，这一先行结果为后来的编程语言类型推断奠定了基础。

Clinical relevance

类型推断通过消除标注负担，同时保留安全性，使静态类型语言更加便捷，并为现代编辑器功能（如类型提示和自动补全）提供支持。其在表达性系统中的局限性决定了程序员仍需提供标注的场景。

History

Hindley于1969年关于组合逻辑中主类型的工作预示了实际的类型推断。Milner于1978年发表的论文介绍了ML语言的多态类型系统和算法W，而Damas和Milner于1982年发表的论文证明了其主类型特性。Hindley-Milner系统成为ML、Haskell和许多后续语言的标准，并且持续有研究将其推断能力扩展到更丰富的环境。

Debates

推断多少与标注多少

随着类型系统表达能力的增强，完全推断变得不可判定，这引发了关于应该自动推断多少以及需要显式标注多少的争论，以保持推断的可处理性和可预测性。

Key figures

• Robin Milner
• Luis Damas
• Roger Hindley
• Benjamin Pierce

Seminal works

• milner1978
• damas1982
• hindley1969
• pierce2002

Frequently asked questions

什么是主类型？

主类型是表达式最通用的类型，使得该表达式的所有其他有效类型都是其替换实例；Hindley-Milner推断在主类型存在时总是能计算出它。

为什么并非所有类型系统都能自动推断类型？

类型推断依赖于可解的约束；在具有高阶或依赖类型等表达性系统中，完全推断变得不可判定，因此程序员必须提供一些标注。