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

Question

我正在查看 A Taste of Linear Logic 中的一个示例.
它首先介绍了定义了常用操作的标准数组(第 24 页):

然后建议线性等价物(使用类型签名的线性逻辑来限制数组复制)将具有稍微不同的类型签名:

其设计理念是，数组包含的值复制起来很便宜，但数组本身的复制成本很高，因此应该从使用传递到用作句柄。
问题:查找和更新的签名与标准签名很好地对应，但是我如何解释新的签名？
尤其是:

函数 new 似乎没有返回数组。如果没有提供一个数组，我该如何使用？

我想我确实理解 Arr –o Arr x X不能使用线性逻辑推导，因此需要一个在不消耗数组的情况下提取单个值的函数，但我不明白为什么 new 不直接提供该函数

Answer 1

实际上，这是关于垃圾收集的。
线性逻辑避免了复制以及留下未使用的值。因此，当您使用 new 创建数组时，您还需要确保它最终再次被清理干净。
你怎么能确保它被清理干净？好吧，在这个例子中，他们通过不返回数组作为结果来做到这一点，而是将它“借给”调用者。除了您真正感兴趣的结果之外，函数 Arr ⊸ Arr ⊗ X 最后必须返回一个数组。假设这将是您开始使用的数组的修改形式。只有 X 被传回给调用者，Arr 被释放。