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

【问题标题】：How can linear types prevent such implementation of "duplicate"?线性类型如何防止这种“重复”的实现？
【发布时间】：2017-08-04 08:48:34
【问题描述】：

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

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

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

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

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

【问题讨论】：

Probably relevant
我觉得这篇文章几乎没有解释底层语义——只是举例说明如何使用这种技术（公平地说，这可能是博客文章的一种很好的格式）。您可以将x ⊸ y 视为1 x -> y 的同义词，这是一个常规箭头，其域为1 x，表示变量a :: 1 x 只使用了一次。通过类型推断，在您的第二个示例中，y 获得推断类型 1 a，因为 y = x 和 x :: 1 a。这扩展到所有自然数和无穷大，并且是一个很好的概括 - 常规箭头 x -> y 可以读作 ω x -> y。
更多详情请参阅trac上的提案。
哦，您链接的论文正确地给出了语义。参见第 3.1 节，图。 2 - 对应于let 的打字规则。但是，请注意，在那篇论文中，let 构造始终在let-bound 变量上包含显式类型签名。使用那篇论文的语法，您的第二个程序（实际上，大多数 Haskell 程序！）甚至在语法上都不是有效的。但重点是，论文中将标准的打字判断x : T推广到x :_{q} T（即q应该是下标）。所以一个术语用它的类型和它的多样性来注释。
@user2407038 那些 cmets 应该是一个答案 ;)

标签： haskell types linear-types

【解决方案1】：

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

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

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

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

【讨论】：