Futhark语言中最大的语义难题

Futhark编程语言最初的理念是（某些问题的）并行编程不需要复杂的语言。事实上，我们相信其复杂性不必超过大学一年级通常教授的函数式语言。（并行算法的复杂性则是另一回事。）总体而言，我认为Futhark在这方面是成功的。Futhark程序的含义使用基于环境的常规语义相当容易确定；即使是像唯一性类型这样棘手的东西，主要是在操作意义上复杂，在类型系统方面某种程度上也是如此——程序（一旦通过类型检查）的含义是显而易见的。这种语义简洁性在实现中也很明显——虽然编译器有许多复杂的优化和精细的转换，但参考解释器大体上是直截了当的，并且在结构上非常类似于学习编程语言的人会编写的第一个树遍历解释器。

你会注意到上一段充满了像“总体”、“大体”和“相当”这样的词——这是因为有一个语言特性已被证明是边界情况和实现错误的特别肥沃的土壤。那个特性就是尺寸类型。在下文中，我将解释为什么一个看似简单的类型系统特性被证明如此具有挑战性。

尺寸参数

回顾基本思想，尺寸类型允许Futhark函数对其参数的大小施加约束。一个简单的例子是点积的定义，它接受两个必须是相同大小向量的参数：

1
2

def dotprod [n] (x: [n]f64) (y: [n]f64) : f64 =
  f64.sum (map2 (*) x y)

这里n是一个尺寸参数，每当应用函数dotprod时，根据传递的具体数组隐式实例化。这本身并不那么困难。通过将尺寸视为不同种类的类型，可以轻松地将尺寸纳入类型检查算法——细节不重要，只需相信这是可行的。（写博客文章比写学术论文容易。）

主要的麻烦出现在我们引入将尺寸用作项级变量的能力时，例如length的定义：

1

def length [n] 't (x: [n]t) : i64 = n

当尺寸参数在作用域内时，它可以在表达式中使用。毫不奇怪，尺寸参数的值是某个数组中相应维度的大小。有趣的是，我们可以在不实际提及x本身的情况下访问x的大小。直观上，我们可以想象n的具体值是在运行时通过实际查看x（例如，通过计算其元素）来确定的，目前这种直觉是成立的。

但现在让我们考虑一个获取矩阵列数（“内部长度”）的函数会发生什么：

1

def cols [n] [m] 't (x: [n][m]t) : i64 = m

现在有两个尺寸参数n和m，我们获取后者。在n为零的情况下，这个情况有点挑战性——因为我们不能简单地检索一行并查看它以确定m——因为没有行。然而，像cols (replicate 0 (replicate 3 0))这样的表达式仍然应该工作（并求值为3）。这意味着我们需要扩展关于尺寸参数值如何确定的概念，因为它不能通过查看数组值的语法形式并计算元素来完成（因为replicate 0 (replicate 3 0)实际上只是写成[]）。解决方案是扩展我们的（概念上的，甚至可能是具体的）数组表示，使得数组除了实际元素外，始终携带一个形状。

然后直观上，为了确定某个尺寸参数的值，我们仍然寻找在某处具有该尺寸的值（例如上面的x），并从中提取它。

但现在，也许不知不觉中，我们选择了一场艰难的战斗。问题是有时我们必须在没有任何元素示例的情况下创建多维数组！然而我们仍然必须以某种方式为数组变出正确的形状。作为一个例子，考虑map函数，其类型如下：

1

val map [n] 'a 'b : (f: a -> b) -> (as: [n]a) -> [n]b

返回数组的元素类型由我们映射的函数（f）的返回类型给出。但如果我们映射一个空数组，那么f可能永远不会被应用：

1
2

> map (\(x:i32) -> [x,x,x]) []
[]

那么，我们如何确定这个空数组的形状实际上是[0][3]？当数组在map内部构造时，只知道外部大小是n（已知为0），并且元素类型是某个b，但我们没有类型为b的值可以用来确定形状可能是什么！我们确实有一个函数a -> b，但我们也没有a——我们拥有的只是一个类型为[0]a的数组，显然其中没有任何a……

这个问题的一个解决方案归功于Barry Jay，并在论文《A Semantics for Shape》中解释。想法是任何“形状良好”的函数可以正常求值（带值，产生值）或带形状求值，产生形状。因此，“形状良好”函数是指结果形状仅取决于输入形状的函数——这排除了诸如过滤这样的函数，其中结果形状也取决于值。这对Futhark本身不是问题，因为我们只希望允许使用具有可预测结果的函数进行映射，以避免不规则数组。

使用这种方法要求我们有两种应用函数的方式：针对值和针对形状。这是一个轻微的语义复杂化，但也许我们可以忍受。但我们也必须从某处获取输入形状——而在map的情况下，只知道输入具有类型a。如果每当调用函数时，我们还接收类型为a的值的具体形状（假设这是可能的，但因为a用于数组元素，我们知道它必须具有有意义的形状），那么事情可能可以工作。但如果我们这样做，那么为什么不直接从b获取形状，避免这整个形状良好函数的事务呢？

确实，这就是Futhark的求值模型。在任何时候，多态函数可以查询类型参数已被实例化的具体类型，并在必要时提取形状。然后这可以用于用它们的完整形状注释任何构造的数组。注意这是一个模型——解释器这样做，因为解释器旨在紧密反映模型，但实际编译器当然不会字面上这样做，因为类型参数在运行时不存在——它只需要以产生相同结果的方式完成。（实际上，它进行单态化。）

麻烦

我们这样做不是因为它容易。我们这样做是因为我们认为它会容易。遗憾的是，结果证明它并不容易。基本问题是我们现在有义务始终知道任何类型的完整形状（除了那些永远不能用作数组元素的类型，但让我们暂时搁置那些）。结果证明这需要比基于环境的标准求值更复杂的机制。根本问题非常明显：我们需要连同表达式一起求值类型，以防它们最终用于构造数组，而类型出现在各种意想不到的地方。

例如，考虑一个模块定义了一些局部绑定cnt和一个也引用cnt的尺寸参数化类型：

1
2
3
4

module M = {
  def cnt : i64 = ... -- 定义不重要
  type C [n] = [n][n*cnt]f64
}

像type C [n] = ...这样的多态类型定义的通常工作方式是它们作为类型构造器添加到类型环境中，然后在使用时实例化。

现在，M.C [n]本身没有形状，因为n尚不知道。在未来的某个时间点，我们可能最终得到某个具体k的实例化M.C [k]，当这种情况发生时，我们可以计算类型的形状，即[k][k*M.cnt]。但不能保证M.cnt实际上在作用域内——它可能是模块M内部的某个隐藏定义，即使不是，从表达式n*cnt并在其最初定义的不同作用域中赋予它含义也是困难的。

由于Futhark是一种纯语言，我们可以在解释类型定义C时，立即将求值cnt的结果替换到其右侧。但这也不舒服：这是一个语法操作，虽然基于替换的语义在理论工作中相当常见，但它们在实现中是不可取的，因为它们非常低效——虽然表达式n*cnt很小，但其他表达式可能很大。解释器不仅应该是参考实现；它还应该证明Futhark的求值不需要任何低效或奇怪的操作（即使解释器中的具体代码在某些情况下可能很幼稚），例如语法替换——语义必须能够通过基于符号表的环境来表达。

我们的解决方案是类型定义不仅捕获定义的右侧，还捕获其环境——也就是说，类型构造器是闭包。当在未来的某个时间点我们最终实例化M.C并有一个k值给n时，我们使用绑定n=>k扩展捕获的环境，并求值所有尺寸中的表达式。这是一个非常奇怪的实现，我们花了相当长的时间才解决——如果我有更多实现依赖类型语言的经验，那么也许我不会觉得它如此奇怪，因为它实际上只是使类型构造器类似于函数，在完全依赖类型语言中它们就是函数。

要点

我们在解释器中遇到了许多与尺寸相关的错误（2316、2273、2258、2222、2219、2209），包括其他我没有心情详细讨论的棘手情况。这是语言中导致最多错误的部分。虽然我们已经形式化了基于尺寸的类型系统的一部分并证明了其健全性，但我们没有处理其与模块系统的交互——而且理论表述通常基于语法替换，而不是环境。我希望当前严重基于环境的实现基本上是正确的方法，尽管我并不真正相信没有剩余错误。

附录

原文发布后撰写。

一些评论者问为什么尺寸参数不总是由调用者显式传递，但有时必须从值中提取。或者换句话说，为什么不按照通常实现依赖类型的方式来做。这是一个好问题，问题仅源于我在上面未涵盖的语言特性。根本问题是模块允许尺寸对调用者隐藏。考虑：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

module M : {
  type~ arr
  val mk : i32 -> arr
  val unmk : arr -> i64
} = {
    type~ arr = ?[n].[n]i32

    def mk (x: i32) : arr = [x,x,x]

    def unmk [n] (a: [n]i32) = n
}

?[n].[n]i32看起来像一个依赖对，但实际上不是——除了数组本身之外，没有包含n的盒子，而?[n]部分只是一个类型级量词。在模块内部，arr实际上只是[n]i32，每当实例化时都有一个新鲜但灵活的n，与仅使用type arr [n] = [n]i32几乎没有区别。特别是，运行时表示是相同的。但对模块的用户来说，尺寸是隐藏的：只有一个类型M.arr。所以如果我们进行像M.unmk (M.mk 123)这样的应用，调用者在任何时候都不知道unmk实际上有一些必须实例化的尺寸参数。嗯，准确地说，在类型检查期间调用者不知道（因为M.arr是抽象的），在求值期间我们当然具体知道M是什么，但我们希望避免在求值期间重新进行任何类型或尺寸推断，而是坚持类型检查器留下的注释。在这种情况下没有注释，因此尺寸参数有两种方式接收它们的值：

1. 它们从实际包含相应尺寸内容的值中提取。这是我通常解释模型的方式，因为它类似于在没有尺寸类型的语言中编程的方式，并且相当清楚为什么它有效。
2. 它们由函数的调用者传递。

如果我们没有在函数调用间隐藏尺寸的方法，那么选项2总是有效。但是，嗯，不幸的是我们有。（也有不涉及模块的方法，但这些例子甚至更复杂。）

如果我们使用传统的依赖积来表示像?[n].[n]i32这样的类型，作为依赖类型语言中的一种特殊值，这也不会发生。这是我们在设计尺寸类型系统时做出的选择——在某种意义上，编译器自动包装和解包依赖积，以提供类似于传统语言的编程体验。也许我们在这方面做对了——这真的取决于语义混乱是否最终成为困扰Futhark程序员的东西。