Mechanized type inference for record concatenation

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

The context behind this post is that I’m working on a type checker and language server for Nix and there are three features of the language which make it tricky to typecheck (which I’ll dub the “three horsemen of Nix type inference”): computed imports (imports that depend on values in scope), computed record fields, and field accesses // (the biased record concatenation operator) which is the subject of this post! 本文的背景是我正在为 Nix 开发一个类型检查器和语言服务器。Nix 语言中有三个特性使其类型检查变得非常棘手（我将其戏称为“Nix 类型推导的三骑士”）：计算导入（依赖于作用域内值的导入）、计算记录字段，以及字段访问运算符 //（偏置记录拼接运算符），这正是本文的主题！

Here “biased record concatenation” means combining two records, preferring fields from one record if they overlap. For example, in Nix the // operator prefers fields from the right record in case of overlap: 这里的“偏置记录拼接”是指合并两个记录，如果字段重叠，则优先保留其中一个记录的字段。例如，在 Nix 中，如果发生重叠，// 运算符会优先保留右侧记录的字段：

nix-repl> { x = 1; y = 2; } // { y = true; z = "hi"; }
{ x = 1; y = true; z = "hi"; }

The good news is that type inference for biased record concatenation is not a research problem because the algorithm was published in 1991 as Type inference for record concatenation and multiple inheritance by Mitchell Wand (henceforth “the Wand paper”). The bad news is that as far as I can tell no language in existence implements the type inference algorithm described in that paper, so even though it’s not a research problem it’s still not a solved problem. 好消息是，偏置记录拼接的类型推导并非一个研究课题，因为该算法早在 1991 年就由 Mitchell Wand 发表在《记录拼接与多重继承的类型推导》（以下简称“Wand 论文”）一文中。坏消息是，据我所知，目前没有任何现存语言实现了该论文中描述的类型推导算法，因此尽管它不是一个研究课题，但它仍然是一个未解决的工程问题。

A big reason why is that the paper isn’t “easy to mechanize” meaning that it doesn’t translate well to code. In this post I hope to fix that by spelling out a formal algorithm equivalent to the original paper. In particular, I’ll formalize the algorithm in three ways: a declarative natural deduction semantics, an algorithmic semantics using constraint generation and resolution, and a reference Haskell implementation (≈400 lines of code) … and I also published a companion project on GitHub that you can use to test the reference Haskell implementation. 造成这种情况的一个主要原因是该论文“不易机械化”，意味着它很难直接转化为代码。在本文中，我希望通过阐述一个与原论文等价的形式化算法来解决这个问题。具体来说，我将通过三种方式对该算法进行形式化：声明式自然演绎语义、使用约束生成与解析的算法语义，以及一个 Haskell 参考实现（约 400 行代码）。此外，我还在 GitHub 上发布了一个配套项目，你可以用它来测试这个参考实现。

This post builds upon my previous post: Record type inference for dummies. Reading that post will not necessarily prepare you for this post if you’re a type theory newcomer, but it will at least help you understand the basic terminology/syntax and also appreciate why this is a challenging problem to solve. 本文建立在我之前的文章《记录类型推导入门》基础之上。如果你是类型理论的新手，阅读那篇文章未必能让你完全准备好理解本文，但它至少能帮助你理解基本的术语和语法，并让你体会到为什么这是一个具有挑战性的问题。

Motivation

动机

Why do we even want to support type inference for this specific operator? After all, there are variations on this operator that are easier to type check, like a record concatenation operator that rejects conflicting fields. Maybe we should just use something like that instead? 我们为什么要支持这个特定运算符的类型推导呢？毕竟，该运算符存在一些更容易进行类型检查的变体，例如拒绝冲突字段的记录拼接运算符。也许我们应该直接使用类似那样的东西？

Well, I know that Nix needs this specific operator and not other variations, because this operator (plus recursion) powers Nixpkgs support for “late binding” of dependencies, where you can override a package and all reverse dependencies pick up the overridden package. This is a critical feature in the age of rampant supply chain attacks because you need to be able to patch or upgrade a dependency and ensure that all downstream packages pick up the fixed dependency. 我之所以确定 Nix 需要这个特定的运算符而非其他变体，是因为该运算符（加上递归）支撑了 Nixpkgs 对依赖项“后期绑定（late binding）”的支持。通过它，你可以覆盖一个包，而所有反向依赖项都会自动获取该被覆盖后的包。在供应链攻击猖獗的时代，这是一个至关重要的特性，因为你需要能够修补或升级某个依赖项，并确保所有下游包都能获取到修复后的版本。

The fundamental reason why the // operator is tricky to type-check is because late binding is tricky to type-check. We could replace Nix’s // operator with some other operator or language feature, but so long as Nixpkgs needs late binding then type inference will remain tricky. I’m hoping that this post will not only progress the state-of-the-art for type checking Nix but also pave the way for more typed languages to support the Wand inference algorithm. That way we can get nicer inferred types with smaller constraints requiring fewer annotations. // 运算符难以进行类型检查的根本原因在于后期绑定本身就难以进行类型检查。我们可以用其他运算符或语言特性替换 Nix 的 // 运算符，但只要 Nixpkgs 需要后期绑定，类型推导就依然会很棘手。我希望本文不仅能推动 Nix 类型检查技术的进步，还能为更多类型化语言支持 Wand 推导算法铺平道路。这样，我们就能获得更简洁的推导类型，减少约束，从而降低对类型标注的需求。

Prior art

先前技术

Currently only one language I’m aware of (PureScript) supports biased record concatenation and also can infer a useful type for this example function (taken from the paper): 目前据我所知，只有一种语言（PureScript）既支持偏置记录拼接，又能为以下示例函数（摘自论文）推导出有用的类型：

-- 或使用 Nix 语法:
r: s: (r // s).x + 1

Note that there are a few typed languages that support biased record concatenation: Dhall (using the same operator as Nix: r // s), TypeScript/Flow (using spread syntax: { ...r, ...s }), and PureScript (using the Record.merge function). But Dhall, TypeScript, and Flow can only work forwards when performing type inference on this operator, meaning they require concrete types for the two input records (e.g., r and s). 请注意，有一些类型化语言支持偏置记录拼接：Dhall（使用与 Nix 相同的运算符：r // s）、TypeScript/Flow（使用展开语法：{ ...r, ...s }）以及 PureScript（使用 Record.merge 函数）。但 Dhall、TypeScript 和 Flow 在对该运算符进行类型推导时只能向前工作，这意味着它们要求两个输入记录（例如 r 和 s）必须具有具体的类型。

For example, in TypeScript if you try to define function example(r, s): number { return { ...r, ...s }.x + 1; };, the type checker will complain that r and s have an inferred type of any because the type checker cannot work backwards to infer useful types for the inputs. 例如，在 TypeScript 中，如果你尝试定义 function example(r, s): number { return { ...r, ...s }.x + 1; };，类型检查器会报错，提示 r 和 s 被推导为 any 类型，因为类型检查器无法反向推导输入参数的有用类型。

PureScript is the only language in that list that can infer a useful and general type for that function without any annotation: 在上述列表中，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

However, PureScript is not using the approach described in the paper and I prefer the approach from the paper because it leads to simpler inferred types and constraints. As I mentioned earlier, no language implements the original paper because it’s so loosely formalized, but I hope to fix that by translating the paper into an algorithm that any person (or any coding agent) can methodically translate to code. 然而，PureScript 并没有使用论文中描述的方法。我更倾向于论文中的方法，因为它能带来更简单的推导类型和约束。正如我之前提到的，没有语言实现原论文的方法是因为它形式化得太松散了，但我希望通过将论文转化为一种任何人（或任何编码智能体）都能按部就班地转化为代码的算法来解决这个问题。

Domains

域 (Domains)

The Wand paper observes that you can think of a row-polymorphic record type such as this one: { x: Int | ρ } as a potentially infinite record consisting of explicit fields (x: Int) and an implicit set of potential fields denoted by a “row variable” (ρ). This row variable stands in for all other fields that might be present, and we’ll call those other fields the row variable’s “domain”. Wand 论文指出，你可以将诸如 { x: Int | ρ } 这样的行多态记录类型视为一个潜在的无限记录，它由显式字段（x: Int）和由“行变量”（ρ）表示的一组隐式潜在字段组成。这个行变量代表了所有可能存在的其他字段，我们将这些其他字段称为该行变量的“域（domain）”。

However, not all row variables are created equal. For example, consider this other record type: { y: Bool | σ }. Both ρ and σ range over two potentially infinite sets of fields (two domains), but they do not range over the same two domains. Specifically, ρ ranges over “all fields that are neither x nor y” and σ ranges over “all fields that are not y”, so σ ranges over one more potential field (x) than ρ. That means we can’t compare ρ and σ as-is because that wouldn’t be an apples-to-apples comparison. The Wand paper builds on that idea to note that… 然而，并非所有的行变量都是平等的。例如，考虑另一个记录类型：{ y: Bool | σ }。ρ 和 σ 都覆盖了两个潜在的无限字段集（两个域），但它们覆盖的并不是同一个域。具体来说，ρ 覆盖的是“既不是 x 也不是 y 的所有字段”，而 σ 覆盖的是“不是 y 的所有字段”，因此 σ 比 ρ 多覆盖了一个潜在字段（x）。这意味着我们不能直接比较 ρ 和 σ，因为那不是同类项比较。Wand 论文正是基于这一思想指出……