haskell - 使用 mkPair 的线性和唯一类型

Question

我一直在这里阅读这篇文章http://edsko.net/2017/01/08/linearity-in-haskell/，作者提到可以构造一个具有唯一元素的非唯一数组，但你可以' t 提取它们。

IE

mkPair :: 1:a -> 1:b -> ω:(1:a, 1:b) -- correct but useless
mkPair x y = (x, y) 

但是您不能在调用函数中读取一次元素吗？也许我错过了一些东西。

此外，虽然是合法的，但从线性角度来看，同样的函数是非法的。但我认为这些只是同一枚硬币的两个面，因此该功能不会根据视角改变合法性。

Answer 1

实际上，mkPair是错误类型的（正如博客本身所说），因为它的返回类型允许复制结果对。因此，任何具有唯一类型a和值的调用者b都可以制作一对，复制它，并获取四个组件（每对两个），并获得两个类型的值a和两个类型的值b。

这将规避 and 的线性a，b因此必须没有函数具有mkPair您上面显示的类型。

Answer 2

我不确定博客文章的作者说这是正确但无用的意思。在Clean中，一种实际上实现了唯一性类型的语言，由于唯一性传播，这是不允许的。您可以在语言报告的第 9.2 节中阅读更多相关信息。根本不存在类型（在 Clean 语法中），因为由于唯一性传播，这实际上是or 。ω:(1:a, 1:b)(*a,*b)1:(1:a, 1:b)*(*a,*b)

这可能是作者试图表达的意思，但由于缺乏理论框架，我发现这篇文章很难阅读。