I've been reading through this article here http://edsko.net/2017/01/08/linearity-in-haskell/ and the author mentions that one can construct a non-unique array with unique elements but that you can't extract them.
I.e.
mkPair :: 1:a -> 1:b -> ω:(1:a, 1:b) -- correct but useless
mkPair x y = (x, y)
but couldn't you read the elements once in the calling function? Maybe I'm missing something.
Also, although legal, this same function is illegal when looking at it from a linearity perspective. But I thought these were just 2 sides of the same coin, so the function would not change legality depending upon perspective.
I'm not sure what the author of the blog post means when he says that this is correct but useless. In Clean, a language which has actually implemented uniqueness types, this is not allowed due to uniqueness propagation. You can read more about that in section 9.2 of the language report. There simply does not exist a type ω:(1:a, 1:b) (which is (*a,*b) in Clean syntax), because due to uniqueness propagation this actually is 1:(1:a, 1:b) or *(*a,*b).
This may be what the author is trying to express, but I find the post hard to read due to the lack of a theoretical framework.