patternMinor
Is it possible to copy data in a linear type system?
Viewed 0 times
linearsystemtypepossibledatacopy
Problem
I'm having a little problem with the abstraction layers in linear types. If every variable is used exactly once, there is no way to copy data, since you have to read each datum twice in order to write it twice to two different locations.
However, you could argue that once a variable is loaded into a register, you may do whatever you want with it, so
Linear types in programming allows a compiler to build efficient pipelines of data transformation. Single-use variables allows in-place mutations in pure functional languages, and/or a memory-efficient implementation without using a garbage collector. Copying a value might make this process a lot more difficult, if not impossible, but I'm not sure.
Is it possible to copy data in a linear type system? Why?
Are there any (big) programming languages that implement linear types with/without copying?
However, you could argue that once a variable is loaded into a register, you may do whatever you want with it, so
a -> (a,a) is a possible function. I'm simply not sure where the line is drawn, or why. Linear types in programming allows a compiler to build efficient pipelines of data transformation. Single-use variables allows in-place mutations in pure functional languages, and/or a memory-efficient implementation without using a garbage collector. Copying a value might make this process a lot more difficult, if not impossible, but I'm not sure.
Is it possible to copy data in a linear type system? Why?
Are there any (big) programming languages that implement linear types with/without copying?
Solution
I don't know why you bring up registers at all, but the answer to your first question is "sure". You (potentially) are able to copy data, you just aren't able to do it freely. For example, an operation $\mathtt{dup}_A : A \multimap A\otimes A$ may be provided, but only for certain types $A$. Most commonly there are "exponentials", written $!A$ for which $\mathtt{dup}_{!A}$ is definable or given. The opposite operation is often called $\mathtt{kill}_A : A \multimap 1$ or $\mathtt{discard}_A$. You may start to see how this leads to a kind of functional manual memory management.
For programming languages, the exponential modality is usually the opposite of what we want as it allows the defining an operation of type $!A \multimap A$ via a rule called "dereliction". If we think of $!A$ as a type that may have multiple references, then a linear type $A$ means that references to $A$ will not be duplicated, not that it hasn't already been duplicated. A different modality leading to uniqueness logic gives the more commonly desired sense of a variable of type $A$ has not been multiply referenced (and thus we are free to mutate it, for example).
The main "serious", general purpose languages I'm aware of using substructural types are: Rust, Clean, and Pony. Rust and Pony allow freely "copying" primitive types but put restrictions on reference types.
For programming languages, the exponential modality is usually the opposite of what we want as it allows the defining an operation of type $!A \multimap A$ via a rule called "dereliction". If we think of $!A$ as a type that may have multiple references, then a linear type $A$ means that references to $A$ will not be duplicated, not that it hasn't already been duplicated. A different modality leading to uniqueness logic gives the more commonly desired sense of a variable of type $A$ has not been multiply referenced (and thus we are free to mutate it, for example).
The main "serious", general purpose languages I'm aware of using substructural types are: Rust, Clean, and Pony. Rust and Pony allow freely "copying" primitive types but put restrictions on reference types.
Context
StackExchange Computer Science Q#67192, answer score: 7
Revisions (0)
No revisions yet.