How do linear types prevent this implementation of "duplicates"?
I recently read a post on Tweag.IO about linear types, which are a useful tool for expressing arguments used only (exactly) once. They give the following example:
dup :: a ⊸ (a,a)
dup x = (x,x)
Now, maybe I don't understand this idea, but why is it impossible to get around:
dup' :: a ⊸ (a,a)
dup' x = (y,y)
where
y = x
The article specifically mentions arguments. Does this apply to all bindings in a function as well?
source to share
I feel like this article explains very little about the underlying semantics - just examples of how to use such a technology. In all fairness, this is probably a good format for blog posting.
You can browse x ⊸ y
as a synonym 1 x -> y
, which is a regular arrow whose domain 1 x
says that the variable is a :: 1 x
used exactly once. By type of output, in your second example y
gets the intended type 1 a
because y = x
and x :: 1 a
. This applies to all natural numbers and infinity. In addition, a regular arrow x -> y
can be read as ω x -> y
, where ω
is infinity.
the paper you linked gives the semantics correctly. See Section 3.1, fig. 2 - entry rule matching let
. Standard typed judgment x : T
generalizes to x :_{q} T
(which q should be an index). In existing Haskell type semantics, a term is annotated with its type. In the proposed extension to the type system, the term is annotated with its type and its multiplicity.
Note, however, that throughout this article the let construct always contains an explicit type signature on the associated variable. With the syntax of this article, your second program (and indeed most Haskell programs!) Is not even syntactically valid. But I argue (without proof) that it is not difficult to figure out how to generalize such a type system to one that is more reminiscent of the current Haskell type system. See the GHC trac proposal for more details on how this might look.
source to share