Do not let your type system reason about aliasing in your programming language

不要让你的类型系统去推断编程语言中的别名（Aliasing）

This post is a followup to the one about the plans for version 1.0, and is based on my experience trying to address one of the outstanding issues that I had described as “easy to fix”. As I will discuss below, it’s basically a typo that is easy enough to fix, but doing so breaks code in ways that raise nontrivial design questions, and further pulling on the thread made me discover a related issue, the solution to which has made me rethink some of Futhark’s oldest design choices. In this post I will explain which unusual type system feature causes all this trouble (it’s basically aliasing, but not in the way you may know about from discussions about aliasing in C), why it is not so easy to fix, and which options we are considering. The bottom line is: unless you have a good reason to pick this fight, don’t do it. The explosion in complexity is not trivial.

这篇文章是关于 1.0 版本计划的后续文章，基于我尝试解决之前描述为“易于修复”的遗留问题时的经验。正如我将在下文讨论的那样，这本质上是一个很容易修复的拼写错误，但这样做会以引发非平凡设计问题的方式破坏代码。顺藤摸瓜，我发现了一个相关问题，其解决方案促使我重新思考 Futhark 一些最古老的设计选择。在这篇文章中，我将解释是哪种不寻常的类型系统特性导致了所有这些麻烦（它本质上是别名，但与你在 C 语言别名讨论中所了解的并不一样），为什么它不容易修复，以及我们正在考虑哪些方案。底线是：除非你有充分的理由去打这场仗，否则不要这样做。其带来的复杂性爆炸绝非小事。

Background

背景

Perhaps Futhark’s most unusual type system feature is in-place updates - it is a feature that lets us write expressions such as A with [i] = v to obtain a semantic copy of the array A with the element at index i replaced by v, but with the cost model guarantee that the cost is proportional to a single element, rather than the entire array A. The obvious implementation is to simply perform a destructive write to the memory where A is stored. To ensure this write cannot ever be observed, the type checker must ensure that the old value of A is never used on any execution path following the update. We say that A is consumed.

Futhark 最不寻常的类型系统特性可能就是原地更新（in-place updates）——这一特性允许我们编写诸如 A with [i] = v 的表达式，从而获得数组 A 的语义副本，其中索引 i 处的元素被替换为 v。但其成本模型保证了开销仅与单个元素成正比，而不是整个数组 A。最显而易见的实现方式是直接对 A 所存储的内存执行破坏性写入。为了确保这种写入永远不会被观测到，类型检查器必须确保在更新后的任何执行路径上，A 的旧值都不会再被使用。我们称 A 被“消费”（consumed）了。

In fact, we can largely ignore the fact that consumption is about in-place updates, and just treat it as an operation that makes the old value invalid somehow (maybe it becomes toxic!). This means that our correctness rule is something like this: objects have identity, and once an object is consumed, it may never be referenced again. In this perspective, a consuming operation like an in-place update semantically returns an object with a new identity, even though our operational goal is of course to reuse memory. The real challenge is that we want to statically ensure that this correctness rule is never broken at run-time, and hence we have to reason about identity in the type checker.

事实上，我们可以很大程度上忽略“消费”是关于原地更新这一事实，而仅仅将其视为一种使旧值以某种方式失效的操作（也许它变得“有毒”了！）。这意味着我们的正确性规则大致如下：对象具有标识（identity），一旦对象被消费，它就永远不能再被引用。从这个角度来看，像原地更新这样的消费操作在语义上返回了一个具有新标识的对象，尽管我们的操作目标当然是重用内存。真正的挑战在于，我们希望在静态层面确保这一正确性规则在运行时永远不会被破坏，因此我们必须在类型检查器中对标识进行推断。

Specifically, when a variable A is consumed, we must also consume any variables that potentially have the same identity (operationally, “share memory”) as A, which we call the aliases of A. As an example, after the binding let B = A then B and A are aliased with each other. We can imagine that this is tracked by associating each variable with an alias set, which a set of the variables it aliases. We then augment the type rules for every language construct to describe how the aliases of the result are constructed from the aliases of the constituent expressions.

具体来说，当变量 A 被消费时，我们也必须消费任何可能与 A 具有相同标识（在操作上即“共享内存”）的变量，我们称之为 A 的别名。例如，在绑定 let B = A 之后，B 和 A 就互为别名。我们可以想象通过将每个变量与一个别名集（alias set）关联来跟踪这一点，该集合包含它所引用的变量。然后，我们为每个语言结构扩充类型规则，以描述结果的别名是如何从组成表达式的别名中构建出来的。

Functions

函数

The most interesting feature in any language is functions. If we want a function f to be able to consume one of its parameters, we must make it clear to callers of f that the corresponding argument is consumed when calling f. We do this by essentially putting an effect (as in effect systems) on the function. A function is either consuming, written *a -> b, or observing, written a -> b. As a poorly conceived pun, we call this the diet of the function. When we apply a consuming function f to an argument A, then A is consumed, exactly as if it was the target of an in-place update.

任何语言中最有趣的特性都是函数。如果我们希望函数 f 能够消费其参数之一，我们必须向 f 的调用者明确指出，在调用 f 时相应的参数会被消费。我们通过本质上在函数上放置一个“效果”（类似于效果系统）来实现这一点。函数要么是消费型的，写作 *a -> b，要么是观察型的，写作 a -> b。作为一个构思拙劣的双关语，我们称之为函数的“饮食”（diet）。当我们对参数 A 应用一个消费型函数 f 时，A 就会被消费，就像它是原地更新的目标一样。