线性类型如何防止这种“复制”的实现？

Question

我最近读了Tweag的帖子。关于线性类型是表达参数的有用工具，只（准确地）使用一次。他们提出了以下例子：

dup :: a ⊸ (a,a)
dup x = (x,x)

现在，也许我误解了这个想法，但为什么不能用以下方法来规避呢：

dup' :: a ⊸ (a,a)
dup' x = (y,y)
  where
    y = x

这篇文章特别提到了论点。这是否也扩展到了函数中的所有绑定？

Answer 1

我觉得这篇文章几乎没有解释底层语义——只是举例说明如何使用这种技术。公平地说，这可能是一个很好的博客帖子格式。

你可以查看x⊸ y作为x的同义词-

你链接的论文给出了正确的语义学。参见第3.1节，图2-对应于let的键入规则。标准的键入判断x： T被推广为x：_{q}T（q应该是下标）。在现有的哈斯克尔类型语义学中，术语用其类型来注释。在对类型系统的拟议扩展中，术语用其类型和多重性进行注释。

然而，请注意，在那篇文章中，let构造总是在let绑定变量上包含一个显式类型签名。根据那篇文章的语法，你的第二个程序（事实上，大多数Haskell程序！）甚至在语法上都是无效的。但我声称（没有证据）不难看出如何将这样一个类型系统推广到一个更能让人想起当前Haskell类型系统的系统。请参阅GHC trac上的提案，以了解更多关于这可能的细节。