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

Question

我最近在 Tweag.IO 上阅读了关于线性类型是一种有用的工具，用于表达仅（确切地）使用一次的参数。他们提供了以下示例：

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

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

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

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

Answer 1

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

您可以将x ⊸ y其视为常规箭头的同义词1 x -> y，其域1 x表示该变量a :: 1 x仅使用一次。通过类型推断，在您的第二个示例中，y获取推断类型1 a，因为y = xand x :: 1 a。这扩展到所有自然数和无穷大。此外，正则箭头x -> y可以读作ω x -> y，其中ω是无穷大。

您链接的论文正确地给出了语义。参见第 3.1 节，图。2 - 对应的打字规则let。标准的打字判断x : T被概括为x :_{q} T（即 q 应该是一个下标）。在现有的 Haskell 类型语义中，一个术语用它的类型进行注释。在建议的类型系统扩展中，一个术语用它的类型和它的多重性来注释。

但是，请注意，在那篇论文中，let 构造始终在 let-bound 变量上包含显式类型签名。使用那篇论文的语法，您的第二个程序（实际上，大多数 Haskell 程序！）甚至在语法上都不是有效的。但我声称（没有证据）不难看出如何将这样的类型系统推广到更让人联想到当前 Haskell 类型系统的类型系统。有关外观的更多详细信息，请参阅 GHC trac上的提案。