记录拼接的机械化类型推断

# 记录拼接的机械化类型推断 来源: https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation 这篇文章的背景是，我正在为 Nix 开发一个类型检查器和语言服务器，该语言有三个特性使得类型检查变得棘手（我称之为“Nix 类型推断的三骑士”）： - 计算导入（依赖于作用域中值的导入）¹ (https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation#user-content-fn-computed) - 计算的记录² (https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation#user-content-fn-attribute) 字段和字段访问 - `//`（偏置的记录拼接运算符），这正是本文的主题！ 这里“偏置的记录拼接”意味着合并两个记录，如果字段重叠则优先选择其中一个记录的字段。例如，在 Nix 中，`//` 运算符在重叠时优先选择右侧记录的字段： ``` nix-repl> { x = 1; y = 2; } // { y = true; z = "hi"; } { x = 1; y = true; z = "hi"; } ``` 好消息是，偏置记录拼接的类型推断**不是**一个研究问题，因为该算法早在 1991 年就已发表为《记录拼接与多重继承的类型推断》（https://www.sciencedirect.com/science/article/pii/089054019190050C），作者是 Mitchell Wand（以下简称“Wand 论文”）。坏消息是，据我所知，**目前没有任何语言**实现了该论文描述的类型推断算法，因此尽管它不是一个*研究问题*，但仍然不是一个*已解决的问题*。 一个主要原因是该论文并不“易于机械化”，也就是说它不容易转化为代码。在这篇文章中，我希望能通过详细阐述一个与原始论文等价的正式算法来解决这个问题。具体来说，我将以三种形式形式化该算法： - 声明式的自然演绎语义 - 使用约束生成与消解的算法语义 - 一个参考 Haskell 实现（约 400 行代码） ... 此外，我还发布了一个配套项目在 GitHub 上（https://github.com/Gabriella439/record-concatenation），你可以用它来测试这个参考 Haskell 实现。 这篇文章建立在我之前的一篇文章之上：《记录类型推断入门》（https://haskellforall.com/2026/06/record-type-inference-for-dummies）。如果你是类型理论新手，阅读那篇文章不一定能让你完全准备好理解本文，但至少能帮助你理解基本的术语/语法，并理解为什么这是一个具有挑战性的问题。 ## 动机 为什么我们非要支持这个特定运算符的类型推断？毕竟，有一些更容易进行类型检查的变体，比如一个拒绝冲突字段的记录拼接运算符。也许我们应该换用那种？ 嗯，我知道 Nix 需要这个特定的运算符，而不是其他变体，因为该运算符（加上递归）为 Nixpkgs 的依赖“晚期绑定”提供了支持，即你可以覆盖一个包，然后所有反向依赖都会使用被覆盖的包。在供应链攻击猖獗的时代，这是一个关键特性，因为你需要能够修补或升级一个依赖，并确保所有下游包都使用修复后的依赖。 `//` 运算符难以进行类型检查的根本原因是：**晚期绑定本身就难以进行类型检查**。我们可以用其他运算符或语言特性替换 Nix 的 `//` 运算符，但只要 Nixpkgs 需要晚期绑定，类型推断就会仍然棘手。 我希望这篇文章不仅能推动 Nix 类型检查的技术水平，还能为更多类型语言支持 Wand 推断算法铺平道路。这样我们就能得到更优雅的推断类型，同时减少所需的注解约束。 ## 先前工作 目前据我所知，只有一种语言（PureScript）既支持偏置记录拼接，又能为论文中的示例函数推断出有用的类型： ... 或者用 Nix 语法表示： ``` r: s: (r // s).x + 1 ``` 注意，确实有一些类型语言支持偏置记录拼接： - Dhall（使用与 Nix 相同的运算符：`r // s`） - TypeScript/Flow（使用展开语法：`{ ...r, ...s }`） - PureScript（使用 `Record.merge` 函数（https://pursuit.purescript.org/packages/purescript-record/4.0.0/docs/Record#v:merge）） ... 但 Dhall、TypeScript 和 Flow 在执行此运算符的类型推断时只能*正向工作*，即它们要求两个输入记录（例如 `r` 和 `s`）具有具体类型。 例如，在 TypeScript 中，如果你尝试定义： ``` function example(r, s): number { return { ...r, ...s }.x + 1; }; ``` ... 类型检查器会抱怨 `r` 和 `s` 被推断为 `any` 类型，因为类型检查器无法*逆向工作*来为输入推断有用的类型。 PureScript 是该列表中唯一能够在没有注解的情况下为那个函数推断出有用且通用类型的语言： ``` -- 此类型注解是可选的。 PureScript 已经推断出此类型 example :: forall a b c d . Union b a c => Nub c (x :: Int | d) => Record a -> Record b -> Int example r s = (merge s r).x + 1 ``` 然而，PureScript 并没有使用论文中描述的方法，而我更喜欢论文中的方法，因为它会产生更简单的推断类型和约束。正如我前面提到的，没有语言实现原始论文，因为它形式化得过于松散，但我希望通过将论文翻译成一个任何人都可以系统化地翻译成代码的算法来改变这一现状。 ## 域 Wand 论文指出，你可以将一个行多态记录类型（例如这个类型）： ... 视为一个潜在的无限记录，它由显式字段（和）以及一个由“行变量”（）表示的隐式*潜在字段*集合组成。这个行变量代表所有*可能*存在的其他字段，我们将这些其他字段称为行变量的“域”。 然而，并非所有行变量都是一样的。例如，考虑另一个记录类型： 两个变量和分别覆盖两个潜在的无限字段集合（两个域），但它们并**不**覆盖**相同**的两个域。具体来说，覆盖“既不是也不是的所有字段”，而覆盖“不是的所有字段”，因此覆盖的范围比多一个潜在字段（）。这意味着我们不能直接比较和，因为那不是一个公平的比较。 Wand 论文基于这个想法指出，当两个记录共享相同的显式字段集合时，记录合一就会变得容易得多，因为这样只需要处理三种情况³ (https://haskellforall.com/2026/07/mechanized-type-inference-for-record-concatenation#user-content-fn-case4)： - **情况 0：** 合一两个封闭记录类型（例如 ）。由于两个记录共享相同的显式字段集合，你可以通过合一它们各自字段的类型（例如 ）来合一这两个记录类型。 - **情况 1：** 合一两个开放记录类型（例如 ）。类似于**情况 0**，但我们还需合一它们的行变量（例如 ），因为它们共享相同的域。 - **情况 2：** 一个记录类型是开放的（例如 ）。我们通过将解为空的字段集合来解决这种情况。 ## 字段实例化 - 第一部分 这意味着我们需要一种方法将任意两个记录类型调整为具有相同的显式字段集合，我们将这个过程称为**字段实例化**。 例如，如果我们要合一这两个记录类型： ... 开始时它们有一个不匹配：左侧记录类型提到了，而右侧记录类型提到了。然而，我们可以通过取（所有不是的字段）并“拆分”出一个显式字段，留下一个新的行变量来表示既不是也不是的所有字段来修复这个不匹配： 这里我们引入了一种新的语法，用来表示是一个*潜在字段*，意味着我们仍然不确定是否存在。然而，无论是否存在，都不再覆盖。 类似地，我们可以将替换为显式提及和一个新的行变量，该变量表示既不是也不是的所有字段： 现在我们可以合一和，因为它们共享相同的域（既不是也不是的字段），但是我们如何合一和呢？ ## 字段注解 这时我们需要引入一些正式的表示法来表示潜在字段（此后简称为“字段”），它们可以是（带有相关字段类型）、，或者未知（用字段变量表示，例如）： 因此，例如： - 表示该记录有一个名为的字段，存储一个 - 表示该记录没有名为的字段 - 表示我们不知道字段是否存在 我们还定义为的语法糖，以支持传统的记录类型，所以如果我们要合一这两个类型： ... 我们会“解糖”为： ... 然后解糖为： ... 然后逐字段合一得到： ... 而行变量合一得到： ... 如果我们把这些等式代回类型中，我们得到两个记录的统一类型（任意优先选择）： ... 我们可以将其“重糖”为： 不过，如果我们合一两个封闭记录类型（比如这些）会发生什么？ 嗯，我们仍然要让它们在显式字段上一致，但由于右侧记录类型是封闭的，我们没有潜在的字段可以引入，所以我们只能引入一个字段： 然后，如果我们解糖左侧记录类型： ... 我们就会得到一个无法调和的不匹配，因为我们无法将和合一，所以合一失败。 ## 约束 现在让我们重新审视之前相同的例子： 我们应该为那个例子推断出什么类型？ 在深入正式表示法之前，让我们先用英语思考一下。我们确定的部分是： - 和必须是记录（因为我们使用拼接它们） - 必须是一个存储的记录字段（因为我们给它加上了） ... 但我们不知道字段来自*哪个*记录，因为可能是或的字段，也可能是*两个*记录的字段（在这种情况下，我们会从获取字段，因为在重叠时优先选择右侧记录）。 Wand 推断算法通过产生一个*类型*以及一个*约束*（类似于 PureScript）来处理这种不确定性。论文推断出的基本类型（调整为本文使用的表示法）将是： ... 这表示我们函数的输入都是记录，每个记录可能或可能没有字段，它们也可能有一些其他字段。此外，函数的输出是。 另外，Wand 算法会生成一个约束： ... 你可以将其解读为：我们的字段要么来自左侧记录（如果缺少字段，则来自左侧记录），要么来自右侧记录（无论左侧记录中是否存在）。 我们甚至可以将那个约束作为推断类型的一部分呈现给最终用户，像这样： 然而，我并不太喜欢这种表示法，在本文中我将提出一种更简单的约束表示法，不仅是为了缩短类型签名，也是为了支持一个更容易机械化的算法。 ## 字段拼接 我将提出的表示法是定义一个新的类型级运算符，用于“合并”两个字段： 具体来说，该运算符返回最右侧的那个字段，如果两个字段都不是，则返回： 你可以把这个运算符想象成类似于运算符，但合并的是字段*类型*而不是字段*值*。 这个运算符大大简化了约束。例如，我们可以使用这个运算符将的推断类型简化为： ... 这等价于 Wand 算法推断出的类型。 > **证明：** 为真当且仅当为真，你可以通过计算两个约束在的所有九种排列下的真值表来证明这一点（其中）。 现在，有几种方式可以在我们的形式语义中建模这个运算符。一种方法是把这个运算符定义为另一种字段类型： 我不喜欢这种方法，因为这不是字段的**规范**表示，也就是说我们的抽象语法允许我们用多种方式表示同一个字段。例如，在这种方法下，和是同一个字段的两种不同语法表示，这是不理想的。 **规范**表示是指每个字段都有唯一的语法表示，根据我的经验，规范表示能促进更简单的算法（和证明）。一种更好的（规范的）表示字段并同时支持字段拼接的方式是： 这里我引入了一种新的表示法：上方的横线表示“零次或多次重复”，所以表示“零个或多个字段变量”。 在这种表示法中，表示我们确定该字段存在，并且*可能*具有类型，除非中的字段变量覆盖了该类型。反之，表示该字段*可能*不存在，除非中的字段变量是。 我们还会添加一点语法糖，写作作为的简写，或者更一般地，写作作为的简写。 使用 Haskell 代码，这看起来像： ```haskell newtype Variable = ID Int data Field = Present Type [Variable] -- ^ 我们尚未定义 Type，但即将定义 | Absent [Variable] present :: Type -> Field present fieldType = Present fieldType [] absent :: Field absent = Absent [] ``` 现在让我们用这种新表示法来定义： > 这个定义满足以下代数性质（幺半群律）：…… 幺半群律的证明包含在附录中。 从概念上讲，这种规范表示记录了最右侧的字段（如果有）。如果存在这样的字段，那么我们就丢弃左边的所有内容，并保留右边的所有字段变量。如果没有这样的字段存在，那么我们就保留所有字段变量。 这种表示法也给了我们一个简单的字段相等性算法：**两个字段当且仅当它们的规范表示相等时才相等**。 例如，和都相等，因为它们共享相同的规范表示：。 在 Haskell 中，我们将使用 `Semigroup` 的追加运算符 `(<>)` 作为的 Haskell 对应： ```haskell instance Semigroup Field where _ <> Present a gs = Present a gs Present a fs <> Absent gs = Present a (fs ++ gs) Absent fs <> Absent gs = Absent (fs ++ gs) instance Monoid Field where mempty = Absent [] ``` 我们还可以定义一个便捷函数来将零个或多个字段合并成一个字段： ... 在 Haskell 中，这其实就是 `mconcat`（使用 `mempty` 和 `(<>)` 将列表扁平化为单个值的函数）： ```haskell mergeFields :: [Field] -> Field mergeFields = mconcat ``` 将视为一个函数而不是语法，意味着我们可以简化任何出现的，比如在我之前提出的约束中： ... 那里我们可以解糖为： ... 计算结果为： ... 并且我们可以将其重糖为简写版本：，这实际上删除了约束中的部分： ... 我们可以将其解读为“要么是或的字段，并且最右边的那个存储了”。 ## 行拼接 我们将以类似的方式重构行变量，但首先我们需要引入类型的抽象语法： ... 在 Haskell 中，这会是： ```haskell import Data.Map (Map) newtype Identifier = Identifier Text newtype Variable = ID Int newtype Row = Row [Variable] data Type = BooleanType | StringType | NumberType | RecordType (Map Identifier Field) Row | FunctionType Type Type | VariableType Variable ``` 如果你读过我之前的文章《记录类型推断入门》（https://haskellforall.com/2026/06/record-type-inference-for-dummies），你会发现这与之前类似，但有一些不同： - 每个字段类型的语法从 变为了 。这意味着我们现在可以显式地将字段标记为缺失（使用）或指定我们不确定字段是否存在（使用）。不过，我们仍然可以使用 作为 的简写，所以这个语法是...（由于内容过长，翻译中断。请继续提供后续内容，我将继续翻译。）