为什么线性数组的类型签名与普通数组相比会发生变化？

Question

我正在看《线性逻辑的品味》中的一个例子。

\n

它首先介绍了定义了常用操作的标准数组（第 24 页）：

\n

\n

然后建议线性等效项（使用类型签名的线性逻辑来限制数组复制）将具有稍微不同的类型签名：

\n

\n

其设计思想是数组包含复制成本低廉的值，但数组本身复制成本昂贵，因此应该从使用中传递到用作句柄。

\n

问题：查找和更新的签名与标准签名很好地对应，但是如何解释新的签名？

\n

尤其：

\n

\n
• 函数 new 似乎没有返回数组。如果没有提供数组，如何获取要使用的数组？
\n
• 我想我确实明白这Arr \xe2\x80\x93o Arr x X不能使用线性逻辑推导，因此需要一个在不消耗数组的情况下提取单个值的函数，但我不明白为什么 new 不直接提供该函数
\n

\n

Answer 1

实际上，这与垃圾收集有关。

\n

线性逻辑避免了复制以及留下未使用的值。因此，当您使用 创建数组时new，您还需要确保它最终被再次清理。

\n

如何确保它被清理干净？好吧，在这个例子中，他们不将数组作为结果返回，而是将 \xe2\x80\x9clending\xe2\x80\x9d 提供给调用者。除了您真正感兴趣的结果之外，函数Arr \xe2\x8a\xb8 Arr \xe2\x8a\x97 X最后还必须返回一个数组。假设这将是数组的修改形式你开始于。只有X被传回调用者，Arr被释放。

\n