线性类型如何防止这种"重复"的实现？

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 = x和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的建议,请参阅有关GHC trac的建议.