Linear and Unique types with mkPair

Question

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.

Answer 1

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.

Answer 2

Actually, mkPair is ill-typed (as the blog itself states), since its return type allows one to duplicate the resulting pair. So, any caller having unique values of types a and b, could make a pair, duplicate it, and take the four components (two from each pair), and obtain two values of type a, and two values of type b.

This would circumvent the linearity of a and b, so there must be no function having a type as the one of mkPair you show above.