How can linear types prevent such implementation of "duplicate"?

Question

I recently read the post on Tweag.IO about Linear Types being an useful tool for expressing arguments used only(exactly) once. They present the following example:

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

Now, maybe I'm misunderstanding the idea, but why couldn't this be circumvented with:

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

The article specifically mentions arguments. Does that extend to all bindings in the function as well?

Answer 1

I feel this article gives almost no explanation of the underlying semantics - just examples of how one uses such a technology. To be fair, this is probably a good format for a blog post.

You could view x ⊸ y as a synonym for 1 x -> y which is a regular arrow, whose domain is 1 x which says the variable a :: 1 x is used exactly once. By type inference, in your second example, y gets the inferred type 1 a because y = x and x :: 1 a. This extends to all natural numbers and infinity. Furthermore, the regular arrow x -> y can be read as ω x -> y, where ω is infinity.

The paper you've linked gives the semantics properly. See sec 3.1, fig. 2 - the typing rule corresponding to let. The standard typing judgment x : T is generalized to x :_{q} T (that q should be a subscript). In existing Haskell type semantics, a term is annotated with its type. In the proposed extension to the type system, a term is annotated with its type, and its multiplicity.

However, note that in that paper, the let construct always contains an explicit type signature on the let-bound variable. With the syntax of that paper, your 2nd program (and indeed, most Haskell programs!) are not even syntactically valid. But I claim (without proof) that it is not hard to see how to generalize such a type system to one with more reminiscent of the current Haskell type system. See the proposal on the GHC trac for more details on how that might look.