记录类型推断入门指南

# 小白也能懂的记录类型推断 来源：https://haskellforall.com/2026/06/record-type-inference-for-dummies 之所以写这篇文章，是因为我本来想写一篇更高级的匿名记录类型推断文章，但意识到大多数读者无法孤立地理解那篇文章。于是我觉得先写这篇入门文章，向刚接触类型理论的人介绍基础知识。我之所以两篇都写，是因为我认为优秀的匿名记录类型推断是阻碍静态类型语言发展的主要因素之一[^1]（https://haskellforall.com/2026/06/record-type-inference-for-dummies#user-content-fn-1），但很多人并未意识到或理解其中原因。我还认为，编程语言专家所理解的可行方案与普通程序员所熟悉或习惯的方案之间存在巨大鸿沟。借用XKCD #2501（https://xkcd.com/2501/）的梗： 所以这篇文章（以及下一篇）将介绍**三十多年前**类型理论领域的研究成果，而我们的行业至今仍未完全跟上。 ## 匿名记录 我说过这是一篇关于*匿名记录*类型推断的文章，我遇到过一些程序员不知道匿名记录是什么，或者至少不熟悉这个名称，所以我简单介绍一下。匿名记录是不需要关联数据类型声明的记录，在动态类型语言中很常见。例如： - JavaScript 称之为“对象”：`` { name: "Alice", age: 25 } `` - Python 称之为“字典”：`` { "name": "Alice", "age": 25 } `` - Ruby 称之为“哈希”：`` { :name => "Alice", :age => 25 } # ... 或等价形式：{ name: "Alice", age: 25 } `` - Nix 称之为“属性集”：`` { name = "Alice"; age = 25; } `` 如果你用过 JSON，那么你已经接触过匿名记录，因为 JSON 对象（就像 JavaScript 对象一样）就是匿名记录。 ## 静态类型 少数静态类型编程语言支持匿名记录，因为静态类型语言通常更喜欢命名数据类型。例如，Haskell 不支持匿名记录，要求所有记录都有数据类型声明，像这样： `` data Person = Person{ name :: Text, age :: Integer } example :: Person example = Person{ name = "Alice", age = 25 } `` 但也有一些静态类型编程语言确实支持匿名记录，比如 TypeScript： `` { name: "Alice", age: 25 } : { name: string, age: number } `` 或者 C#（称之为“匿名类型”）： `` new { Name = "Alice"; Age = 25 } `` 或者 PureScript（称之为“记录”）： `` { name: "Alice", age: 25 } : { name :: String, age :: Int } `` 如果只需要语言支持记录字面量，而不需要记录上的任何操作，那么推断它们的类型相当容易。不过，为了做到这一点，我要先介绍一些基本的类型理论表示法。 我们定义一个基本的抽象语法树，其中表达式（）可以是： - 一个（例如） - 一个（例如） - 一个包含 0 个或更多字段的记录（例如） 形式化地写出这个定义如下[^2]（https://haskellforall.com/2026/06/record-type-inference-for-dummies#user-content-fn-2）： ... 等价的 Haskell 代码大致是： `` type Identifier = Text data Expression = Boolean Bool | String Text | Number Double | Record (Map Identifier Expression) `` 字段可以存储任意表达式，这意味着你可以嵌套记录，例如： 我们还需要为推断出的类型定义一个抽象语法树，它可以为： - 类型 - 类型 - 类型 - 包含 0 个或更多字段的记录类型（例如） 表示法如下： 等价的 Haskell 代码大致是： `` data Type = BooleanType | StringType | NumberType | RecordType (Map Identifier Type) `` 现在我们有了表达式和类型的语法，我们可以定义一些基本的类型推断规则： - 和总是有类型 - 一个（比如）总是有类型 - 一个（比如）总是有类型 我们使用以下表示法写出这些规则： 如果你以前没见过这种表示法，你可以把它看作实现类型推断函数的数学伪代码。等价的 Haskell 函数大致是： `` infer :: [(Identifier, Type)] -- ^ 上下文，即 "Γ"（目前未使用） -> Expression -- ^ 输入表达式 -> Either Text Type -- ^ 输出推断类型（目前永不失败） infer context (Boolean _) = return BooleanType infer context (String _) = return StringType infer context (Number _) = return NumberType `` > **注意：**你可以在附录中找到完整的 Haskell 代码。 现在假设我们要推断这样一个记录字面量的类型： 通常我们会像这样手动推理表达式的类型： 1. 要推断的类型，我们需要推断每个字段的类型： A. 首先，推断的类型（它是） B. 然后，推断的类型（它是） 2. 现在将这些组合成最终的记录类型： 类型理论家有一种表示法来描述这种推理过程，看起来像这样： 这就是所谓的“类型推导”，其工作原理是“外部”推理步骤（比如步骤 1 和 2）放在底部，“内部”推理步骤（比如步骤 A 和 B）放在顶部。 如果我们把这个推理过程推广到所有记录，可能会写出类似这样的东西： ... 你可以理解为：“如果要推断一个记录的类型，那么推断每个字段的类型，并用推断出的类型替换每个字段”。 在 Haskell 中就是： `` infer context (Record fields) = do fieldTypes <- traverse (infer context) fields return (RecordType fieldTypes) `` 我们可以验证这在 Haskell REPL 中可以工作： `` ghci> :set -XOverloadedStrings -XOverloadedLists ghci> infer [] (Record [("name", String "Alice"), ("age", Number 25)]) Right (RecordType (fromList [("age",NumberType),("name",StringType)])) `` ## 字段访问 任何名副其实的编程语言[^3]（https://haskellforall.com/2026/06/record-type-inference-for-dummies#user-content-fn-3）也会支持使用类似点号表示法（例如）的记录字段访问。例如，在 Nix 中是这样： `` nix-repl> { name = "Alice"; age = 25; }.name "Alice" `` 所以我们将为字段访问添加一条类型推断规则，但首先我们需要扩展表达式语法以支持点号表示法： ... 现在我们可以添加这条类型推断规则： 这表示：如果推断出的类型是一个包含名为的字段的记录，那么我们可以从表达式中访问该字段。该字段访问的推断类型就是字段的推断类型。 等价的 Haskell 代码大致是： `` data Expression = ... | FieldAccess Expression Identifier ... infer context (FieldAccess expression field) = do expressionType <- infer context expression case expressionType of RecordType fieldTypes -> case Map.lookup field fieldTypes of Just fieldType -> return fieldType Nothing -> Left "missing field" _ -> Left "not a record" `` 这是我们添加的第一条可能失败的类型推断规则。如果我们要推断像这样的表达式的类型，那么它不符合那条类型推断规则（或任何其他规则），因此我们将拒绝该表达式并给出类型错误（“not a record”）。但是，如果字段缺失，该规则也会拒绝字段访问。如果我们要推断的类型，那*也*不符合我们的类型推断规则，因此我们将拒绝该表达式并给出类型错误（“missing field”）。 在继续之前，让我们用一个例子测试这条类型推断规则。假设我们要推断这个表达式的类型： 我们的推理过程可能如下： - 要知道字段访问（）的类型，我需要记录的类型 - 要知道记录的类型，我需要字段的类型 - 字段的类型（设置为）是 - 记录的类型是 - 字段访问（）的类型是 等价的正式推导是： 我们可以在 Haskell 中确认推断出的类型确实是： `` exampleRecord :: Expression exampleRecord = Record [("name", String "Alice"), ("age", Number 25)] exampleAccess :: Expression exampleAccess = FieldAccess exampleRecord "age" `` `` ghci> infer [] exampleAccess Right NumberType `` ## 变量 你可能会想，为什么我们不这样写规则： 换句话说，为什么我们在推断字段类型时不查阅表达式的*值*而是查阅表达式的*类型*？毕竟，对于最后一个例子，这会使推理过程更直接： - 要知道字段访问（）的类型，我需要字段的类型（设置为） - 的类型是 - 字段访问（）的类型是 等价的正式推导也更简单： 查阅值对我们当前（非常简单）的编程语言是可行的，但一旦我们添加了变量支持，它就不再适用了，因为像这样的表达式会被拒绝： 你可以将其理解为将表达式（）赋值给局部变量（），然后从该变量访问字段。我们只能通过查阅的类型来推断这个表达式的类型。我们不能查阅的值，因为目前只是一个未求值的变量（不是记录字面量）。我们*可以*先求值表达式以得到的值，但那会违背类型检查的目的：通常我们在求值表达式*之前*进行类型检查，以便在求值开始前发现错误[^4]（https://haskellforall.com/2026/06/record-type-inference-for-dummies#user-content-fn-4）。 因此，让我们将变量和变量赋值添加到我们非常简化的语言中： 现在是一个有效的表达式（求值为），这个也是： ... 求值为。 > **注意：**我不会在这篇文章中详细说明求值规则，因为我只专注于解释类型推断。 for 的类型推断规则是我们第一次真正使用到目前为止一直忽略的上下文（）： 这表示：为了推断一个表达式的类型，我们需要首先推断每个局部变量赋值（,, ...）的右侧表达式的类型。然后，我们在推断最终结果（）的类型时，用每个赋值局部变量的推断类型（）扩展我们的类型推断上下文（）。 `` data Expression = ... | Let [(Identifier, Expression)] Expression ... infer context (Let [] expression) = do infer context expression infer context (Let ((x, assignment) : assignments) expression) = do assignmentType <- infer context assignment infer ((x, assignmentType) : context) (Let assignments expression) `` 这条规则与变量的类型推断规则配对使用： ... 你可以理解为：“要推断一个名为的变量的类型，在上下文中查找的推断类型”。如果上下文中缺少，则此规则不匹配，我们将拒绝该表达式并给出类型错误（“unbound variable”）。这里的就像是一个“命名的省略号”，代表我们当前不关心的其他推断类型。 `` data Expression = ... | Variable Identifier infer context (Variable identifier) = do case lookup identifier context of Just assignmentType -> return assignmentType Nothing -> Left "unbound variable" `` 有了这两条新规则，我们现在可以为之前的例子写出类型推导，以推断其类型： 这基本上是在说： - 有类型，因为... - 有类型，因为... - 有类型 - ... 因此有类型 - ... 因此有类型 我们也可以在 Haskell 中验证： `` exampleLet :: Expression exampleLet = Let [("r", Record [("x", Number 1)])] (FieldAccess (Variable "r") "x") `` `` ghci> infer [] exampleLet Right NumberType `` ## 函数 如果我们的编程语言只需要这些，那么匿名记录的类型推断就很简单，大多数静态类型编程语言都会支持匿名记录。然而，每种编程语言都支持函数，而这正是类型推断开始变得棘手的地方。 为了理解原因，考虑这个 TypeScript 函数： `` const getName = person => person.name; `` ... 在 lambda 演算中写作，或者在 Nix 中写作： `` getName = person: person.name; `` 我们为这个函数推断出什么类型？为了回答这个问题，我们首先需要扩展语法，用表示一个或多个参数的匿名函数： ... 我们还需要为函数类型添加新语法： ... 其中表示一个输入类型为、输出类型为的函数。然后我们可以添加一条函数类型推断规则： 这是我们写的第一条不能直接按原样翻译成 Haskell 代码的类型推断规则（*确实*可以使用 unification（https://en.wikipedia.org/wiki/Unification_(computer_science)#Application:_type_inference） 或类似方法编码，但这超出了本文的范围）。但是，你可以将这条规则理解为：如果当具有类型时具有类型，那么具有类型。 即使没有代码，我们仍然可以使用这条规则来推理出的类型应该是什么： 换句话说，是一个函数，其输入类型为（一个至少包含一个类型为的字段的记录），输出类型为。这很合理！到目前为止一切顺利。 然而，这并不*完全*是大多数编程语言会推断或期望的类型。具体来说，大多数编程语言不支持记录类型中的省略号，但这是因为有两种稍好的方式来处理这样的类型。 ### 子类型 一些静态类型编程语言（如 TypeScript）将记录类型视为所有共享相同字段的更大记录的子类型。换句话说： 在这种方法下，省略号是多余的，因为所有记录类型都隐含省略号。这意味着在 TypeScript 中你可以写： `` const getName = (person: { name: string }) => person.name; `` ... 并且`getName`在更大的记录（例如`{ name: "Alice", age: 25 }`）上调用时仍然有效[^5]（https://haskellforall.com/2026/06/record-type-inference-for-dummies#user-content-fn-5）。这种方法效果不错，但还有更好的处理额外记录字段的方法，这就是： ### 行多态 第二种方法不是*去掉*省略号，而是*命名*省略号，也就是说，不是这样： ... 我们写成这样： 这是 PureScript 和 Elm 等语言采用的方法，PureScript 会将类型写成这样： `` { name :: String | other } `` ... Elm 使用类似的语法： `` { other | name : String } `` 这有一些很好的优点，我们将在下一节中讨论，但首先让我们形式化“命名省略号”的含义。首先，我们会创建一类新的标识符（称为“行变量”）： > “行”是一个古老的名称，意为“一组字段”。请记住，这类类型推断的研究发生在很久以前，甚至早于 JSON 的出现。不过，这个名称的好处是类型理论家可以稍微调皮地使用希腊字母（“rho”）来表示“行”。 然后我们将更改记录类型的抽象语法，以允许出现可选的行变量： ... 并更新字段访问的类型推断规则，使用行变量而不是省略号： 这种使用命名省略号的方法被称为“行多态”，因为它允许我们抽象（成为“多态”）其他字段集（“行”）。 ## 记录扩展 你可能会想：为什么我们要抽象其他字段集？特别是，为什么要给这些其他字段一个*名称*？一个原因是支持我们的下一个记录运算符：记录扩展。我们将使用这个语法： ... 你可以理解为“用 扩展记录