不要让你的编程语言类型系统处理别名推理

# 别让你的编程语言类型系统推理别名 来源：https://futhark-lang.org/blog/2026-09-22-aliasing.html 发布于2026年9月22日 本文是关于1.0版本规划文章（https://futhark-lang.org/blog/2026-08-26-towards-1.0.html）的续篇，基于我尝试解决一个遗留问题（https://github.com/diku-dk/futhark/issues/1675）的经验——这个问题我曾形容为“很容易修复”。正如我将要讨论的，这基本上是个容易修正的笔误，但修正它会以引发非平凡设计问题的方式破坏代码，而进一步探究则让我发现了另一个相关问题（https://github.com/diku-dk/futhark/issues/2531），其解决方案促使我重新思考Futhark的一些最古老的设计选择。本文将解释是哪个不寻常的类型系统特性导致了所有这些麻烦（它基本上就是别名，但与你在讨论C语言别名时所知的不同），为什么它不易修复，以及我们正在考虑哪些方案。底线是：除非你有充分理由去碰这个问题，否则别碰它。复杂性的爆炸可不是小题大做。 ### 背景（https://futhark-lang.org/blog/2026-09-22-aliasing.html#background） Futhark最独特的类型系统特性或许是**就地更新**（https://futhark-lang.org/blog/2022-06-13-uniqueness-types.html）——它允许我们编写诸如 `A with [i] = v` 这样的表达式，以获得数组`A`的一个语义副本，其中索引`i`处的元素被替换为`v`，但成本模型保证（https://futhark-lang.org/blog/2022-01-27-cost-models-are-contracts.html）其成本与单个元素成正比，而非整个数组`A`。显而易见的实现是直接对存储`A`的内存进行破坏性写入。为确保此写入永远不会被观测到，类型检查器必须确保在更新之后的任何执行路径上，`A`的旧值都未被使用。我们称`A`被**消耗**了。实际上，我们可以很大程度上忽略消耗是关于就地更新这一事实，而将其视为一种以某种方式使旧值无效的操作（也许它变得“有毒”了！）。这意味着我们的正确性规则类似于：对象具有标识性，一旦对象被消耗，它就再也不能被引用。从这个角度看，像就地更新这样的消耗操作在语义上返回一个具有新标识的对象，尽管我们的*操作*目标当然是重用内存。真正的挑战在于，我们要静态确保这个正确性规则在运行时永不被破坏，因此我们必须在类型检查器中进行关于标识性的推理。 具体来说，当一个变量`A`被消耗时，我们也必须消耗所有可能与`A`具有相同标识（操作上意味着“共享内存”）的变量，我们称之为`A`的**别名**。例如，在绑定`let B = A`之后，`B`和`A`彼此别名。我们可以想象这是通过将每个变量与一个**别名集**关联来跟踪的，该别名集是与之别名的变量集合。然后我们为每种语言构造的类型规则进行增强，以描述结果的别名如何从构成表达式的别名构建而来。我不会一一列举，但例如表达式`A`的结果的别名集无疑是`\{A\}`，而数组字面量`\[x, ..., z\]`具有空别名集，表示它构造了一个将元素复制进去的新数组。 条件表达式很有趣，因为别名跟踪是保守的，这意味着在绑定`let C = if ... then A else B`之后，我们认为`C`同时与`A`和`B`别名（反之亦然），即使在运行时实际上只会发生其中一种情况。这种保守性是关键，因为在编译时拒绝一个程序可能令人烦恼，但允许一个程序使用已消耗的值将是灾难性的。 虽然基本思想很容易理解，但大量的复杂性源于与其他语言特性的交互，以及我们的一些设计约束。虽然安全性（soundness）当然是基本要求，但第二重要的或许是**简单性**。就地更新对某些算法至关重要（也可用于很酷的黑客手段（https://futhark-lang.org/blog/2024-04-18-random-numbers-with-uniqueness-types.html）），但许多程序*根本不使用它们*，因此不应该充斥着比绝对必要更复杂的语法或规则。我们尽可能让程序员能够假装这个特性完全不存在，只要他们不需要它。这绝非易事。我们还希望所有关于消耗和别名的规则都是**局部**的，意味着它们不需要进行昂贵的整个程序分析来检查。 ### 函数（https://futhark-lang.org/blog/2026-09-22-aliasing.html#functions） 任何语言中最有趣的特性是函数。如果我们希望函数`f`能够消耗其参数之一，我们必须向`f`的调用者明确表明，调用`f`时相应的参数会被消耗。我们本质上通过在函数上放置一个**效果**（如效果系统中）来实现这一点。一个函数要么是**消耗型**的，写作`\*a -> b`，要么是**观察型**的，写作`a -> b`。作为一个不甚贴切的文字游戏，我们称之为函数的**饮食**。当我们把一个消耗型函数`f`应用于参数`A`时，`A`就被消耗了，就像它是就地更新的目标一样。由于Futhark是一个柯里化语言，其中“多参数”函数只是一个返回函数的函数，这得以很好地推广。例如，这个函数类型消耗其第二个参数，但不消耗第一个： `(a, *b) -> c` 另一个问题是确定函数的别名。一个合理的规则似乎是，函数应用的结果别名*所有*其未被消耗的参数。但这使得别名相当泛滥，意味着很快一切都会彼此别名，而且这过于保守：大多数函数实际上产生的是新构造的值。因此，我们也允许函数返回类型指示结果的**新鲜度**：要么**新鲜**（无别名），要么**不新鲜**（别名所有参数）。稍微令人困惑的是，这也用星号表示： `a -> *b -- 新鲜结果` `a -> b -- 不新鲜结果` 这些星号与参数上的星号含义*完全不同*。在返回类型中，它们描述结果的别名，而在参数上它们表示消耗效果。类似的表示法源自该部分语言设计如何从Clean的唯一性类型（https://clean.cs.ru.nl/download/html_report/CleanRep.2.2_11.htm）演化而来，后者使用星号表示唯一性（但请注意，Futhark的消耗/就地更新功能今天与唯一性类型*完全无关*）。它与仿射类型（https://users.cs.northwestern.edu/~jesse/pubs/alms/tovpucella-alms.pdf）有更大的相似性，尽管它们仍然不是同一回事。Futhark的类型系统更像一个效果系统，它禁止特定的效果顺序（先消耗值后观察值），并配以一个用于传播别名的类型系统。 新鲜度和消耗注解也对函数定义施加约束。考虑这个函数定义： `def invalid (x: []i32) : *[]i32 = x` 我们声明该函数返回一个新鲜结果，但结果`x`别名了一个未被消耗的参数。这会被类型检查器拒绝。 一个稍微微妙的规则是，即使函数被声明为返回不新鲜的结果，它也不能返回一个别名全局变量的值： `def global : []i32 = [1,2,3]` `def f1 (b: bool) : []i32 = if b then global else [4,5,6]` 考虑应用`f1 true`。结果的别名应该是什么？在`f1`的类型中没有任何地方提到`global`，因此我们无法在应用点推断出这个别名。因此，我们根据以下规则在定义点禁止`f1`： - 顶层函数定义不得返回别名除函数参数之外任何内容的值。 另一种解决方案是用更精确的别名概念来增强我们的类型系统。这将允许`f1`指定结果可能别名`global`，也允许其他函数更精确地指定结果与参数之间的别名关系。我们不这样做是为了简单性：Futhark*不是*一个像Rust那样用于仔细推理生命周期或别名的语言。我们之所以费尽周折，唯一的原因是为了允许表达某些算法，这些算法需要只有通过就地更新才能达到的性能保证，而我们希望尽可能*小*的语言特性仍能满足此要求。 ### 元组（https://futhark-lang.org/blog/2026-09-22-aliasing.html#tuples） 另一个问题是元组（或记录）结果新鲜意味着什么。考虑这个定义： `def f2 (n: i64) : *([]i64, []i64) =` `let arr = iota n` `in (arr, arr)` 这里，`iota`是构造大小为`n`的新鲜索引数组的常用函数。虽然`arr`本身没有别名，因此`f2`的结果不别名参数或全局变量，但这仍然是一个有问题的定义。考虑这个绑定： `let (a, b) = f2 10` 虽然*我们*知道`f2`返回两个相同的数组，`a`和`b`共享内存，因此在概念上是别名的，但这并未出现在`f2`的类型中任何地方。因此我们添加这条规则： - 当返回一个声明为新鲜的元组时，每个*组成部分*必须是新鲜的，即它们彼此不别名。 这在`f2`的定义点进行检查，因此上述函数会被拒绝。 这里我应该指出，在Futhark的别名系统中，*只有数组和抽象类型*（因为它们可能是数组）自身携带别名。原始类型如`i64`具有“值语义”，意味着任何使用都涉及复制，而元组、记录和和类型只是其组件的薄框架（https://futhark-lang.org/blog/2021-08-02-value-representation.html）。这意味着返回类型`\*([]i64, []i64)`，如`f2`中，实际上被解释为`(\*[]i64, \*[]i64)`。 还有更多复杂之处。如果一个函数返回不新鲜的对，比如具有这种类型的函数： `bool -> ([]i64, []i64)` 那么这两个数组有可能彼此别名，就像上面的`f2`一样。因此我们为函数应用添加另一条别名传播规则： - 如果一个函数返回一个元组，那么它的所有不新鲜组成部分彼此别名。 消耗方面也存在问题。考虑这个函数，它有一个消耗型参数，碰巧是一个元组： `def f3 [n] ((x,y): *([n]i32, [n]i32)) =` `let x' = x with [0] = 0` `in (x', y)` 首先，为了使其在直觉上有效，我们需要保证`xy`元组的两个组成部分彼此不别名。这需要在函数应用中添加一条规则： - 当为消耗型参数传递参数时，元组（或记录）组成部分不得彼此别名。 注意在`f3`中，元组在获得名称之前就立即通过模式匹配被解构了。想想如果我们改为这样写会怎样，使用投影来提取元组组成部分： `def f3_bad [n] (xy: *([n]i32, [n]i32)) =` `let x = xy.0` `let y = xy.1` `let x' = x with [0] = 0` `in (x', y)` 这个函数在当前的Futhark中会失败，因为`x`和`y`都别名于整个`xy`（或者更准确地说，别名于`xy`的两个组成部分），因此对`x`的更新也消耗了`xy`，这使得对`y`的后续引用无效。这可以说是一个设计缺陷，我们目前通过语法糖（https://futhark-lang.org/blog/2026-03-04-array-record-updates.html）来掩盖它，但我想用更好的方式修复它。 我怀疑通过细化我们的别名集，可以改进元组的处理方式——不再只是变量名的集合，而是变量名加上一个*位置*，这允许我们只别名元组的一部分。如果我们然后消耗一个元组组成部分，那么整个元组就不能再被引用，但其他未被消耗的子组件仍然可以使用。我在这方面已经做了一些探索性工作（https://github.com/diku-dk/futhark/issues/2456），但它太不完整，不值得深入。 ### 高阶函数（https://futhark-lang.org/blog/2026-09-22-aliasing.html#higher-order-functions） 高阶函数确实增加了一些复杂性，但只要我们处理的是具体类型，它们并不太难。 考虑以下高阶函数： `def f4 (p: bool -> []i32) =` `let x = p true` `let y = p false` `in ...` 我们将函数`p`应用于一些参数，并获得数组`x`和`y`。我们允许消耗它们吗？根据上述推理，答案似乎是肯定的：由于`p`返回不新鲜的结果，`x`和`y`别名于`p`的参数，而这些参数只是布尔值，并且由于原始值不携带别名，这似乎没问题。然而，请注意`p`不返回一个新鲜数组——这意味着`f4`的一个应用可能是这样的： `let arr = [1,2,3]` `in f4 (\b -> arr)` 现在我们在`f4`内部每次应用`p`都得到对`arr`的引用。显然消耗它是灾难性的。我们该如何解决？一个解决方案是对匿名函数施加与顶层函数相同的约束，即它们不得返回别名自由变量的值。那么上述将是类型错误，我们必须改为这样编写： `let arr = [1,2,3]` `in f4 (\b -> copy arr)` `copy`函数接受一个值并返回一个新鲜值（需要付出代价），并且是许多别名相关错误的有用变通方法。实际上，这种方法会导致无法忍受的样板代码数量以及`copy`的开销。我们的解决方案分为两部分： 1. 像lambda这样的局部函数允许返回别名其作用域内（非全局）变量的值。 2. 我们更改函数应用的别名规则，使得*函数本身的别名*也应用于函数应用的结果。 在`f4`的定义中，这意味着数组`x`和`y`别名于函数参数`p`，并且由于`p`不可消耗，`x`和`y`也不可消耗。操作上的解释相当直接：函数包含一个闭包，函数应用的结果可能别名该闭包。 对于顶层函数，我们要求结果*不得*别名于闭包（这就是“不得别名自由变量”规则的真正含义）。我们可以对两种情况使用相同的规则，或者互换它们，而不会损失健全性，但我们发现不一致性能带来更好的人体工学。例如，考虑顶层`transpose`函数： `val transpose [n][m] 't : [n][m]t -> [m][n]t` 如果`transpose X`的应用会别名于`transpose`本身，那将相当烦人，因为这意味着我们无法消耗结果（因为那可能会多次消耗`transpose`）。为此，我们对顶层函数施加更严格的规则。用别名表示，我们假设顶层函数定义在空环境中，意味着它们的闭包别名是空集，因为我们对其定义的别名限制意味着结果不能别名环境中的任何内容。 （某些特定功能倾向的读者现在可能会想：等等，参数性（https://www.cl.cam.ac.uk/teaching/1617/L28/parametricity.pdf）不正告诉我们`transpose`的结果不可能别名除其参数之外的任何东西吗？）