5 ms·

Can somebody explain what is "linear" about linear types. There seems to be a common pattern in computer science of reusing well established mathematical terms

Can somebody explain what is "linear" about linear types. There seems to be a common pattern in computer science of reusing well established mathematical terms (e.g. vectors, tensors) in confusing ways.

ajjenkins 4y ago
This is my first type hearing about linear types, but my guess is the name comes from the fact that you have to repeatedly “thread” a value through your code to keep using it. If you look at the example for Files, you have to pass the outputted file pointer from writeFile as an input value to the next writeFile. So you can picture that one file pointer as linearly threading through you code. And it’s specifically linear because your “thread” can’t “branch”, because that would mean you’re using the same value twice (except an if-statement is kind of a branch, but it’s ok because when the code runs the value will follow a linear path). But I agree that “linear types” is not a great name. Something like “single use types” would be clearer to me.
henrydark 4y ago
It comes from Linear Logic, where there's no inference A&B->A. I think the point of the name is "there's always progress". This talk explains some other origins as well as the connections between different logics to different type systems (though the focus is on stack languages) https://youtu.be/_IgqJr8jG8M https://youtu.be/_IgqJr8jG8M
mdm12 4y ago
My understanding is that the 'linear' terminology derives from the field of Linear Logic[1]. But, I am by no means an expert on theoretical computer science etymology! [1] https://en.wikipedia.org/wiki/Linear_logic https://en.wikipedia.org/wiki/Linear_logic
justincormack 4y ago
Linear in the sense you can draw a line, not a tree, through the usage - in terms of memory allocation, the linear item cannot be copied (ie create an allocation), or destroyed during its lifetime. The naming comes from linear logic.
ogogmad 4y ago
Linear types <- linear logic <- linear algebra. See here: See here: https://www.cs.bham.ac.uk/~drg/bll/steve.pdf https://www.cs.bham.ac.uk/~drg/bll/steve.pdf There's also "affine logic" which riffs on the same thing.
- college_physics 4y ago
  Ahh, thats cool. Thanks for the link
zetalyrae 4y ago
It comes from linear logic and that's as far as I know. It's not great because it can scare away programmers who hear "linear" and think abstract nonsense. But there's not really a better name. "Uniqueness type" or "Single-use type" is too verbose. I'd rather not bikeshed the terminology too much and just use what exists.
- eternalban 4y ago
  Disposable Type.
- Nevermark 4y ago
  “Single-instance” type? ”Single-reference”?
- masklinn 4y ago
  It's not just single-use, an affine type is also single-use: colloquially, a single-use item is not a must-use item.
bmacho 4y ago
Nothing, it just has the name for historic reasons.
- dboreham 4y ago
  I've been scratching my head over this all day since reading the beginning of the thread earlier. This is the one correct answer.
  - naasking 4y ago
    This is not correct actually. It comes from linear logic, and it's connection to ordinary linear functions we all learned in school is clear if you think about it: any linear function f(x) can be written in a form where x appears only once on the right hand side, ie. f(x) = Bx + C. That's exactly the property linear typing enforces: a new binding only appears once on the right hand side, ie. let x = v in e, where e references x only once.
    - deleted 4y ago
      [deleted]
trenchgun 4y ago
> Girard himself, in his native language (cf. Girard, Cours de Logique I, Hermann, 2006, Section 1.B.2), writes: > "La logique linéaire est issue d'une prise en compte systématique de l'interprétation catégorique. En particulier, les espaces cohérents [...], proches des espaces vectoriels [...] font apparaître des structures logiques familières en algèbre linéaires [...]" > Translation: "Linear logic developed from systematically taking into consideration the categorical interpretation. In particular, coherent spaces [...], similar to vector spaces [...] give rise to logical structures which are familiar from linear algebra." > So, in one sentence, it is called linear logic because it involves semantics which resemble structures from linear algebra. https://math.stackexchange.com/questions/2339147/why-is-it-called-linear-logic https://math.stackexchange.com/questions/2339147/why-is-it-c...

ajjenkins 4y ago

This is my first type hearing about linear types, but my guess is the name comes from the fact that you have to repeatedly “thread” a value through your code to keep using it. If you look at the example for Files, you have to pass the outputted file pointer from writeFile as an input value to the next writeFile. So you can picture that one file pointer as linearly threading through you code. And it’s specifically linear because your “thread” can’t “branch”, because that would mean you’re using the same value twice (except an if-statement is kind of a branch, but it’s ok because when the code runs the value will follow a linear path). But I agree that “linear types” is not a great name. Something like “single use types” would be clearer to me.

henrydark 4y ago

It comes from Linear Logic, where there's no inference A&B->A. I think the point of the name is "there's always progress". This talk explains some other origins as well as the connections between different logics to different type systems (though the focus is on stack languages) https://youtu.be/_IgqJr8jG8M https://youtu.be/_IgqJr8jG8M

mdm12 4y ago

My understanding is that the 'linear' terminology derives from the field of Linear Logic[1]. But, I am by no means an expert on theoretical computer science etymology! [1] https://en.wikipedia.org/wiki/Linear_logic https://en.wikipedia.org/wiki/Linear_logic

justincormack 4y ago

Linear in the sense you can draw a line, not a tree, through the usage - in terms of memory allocation, the linear item cannot be copied (ie create an allocation), or destroyed during its lifetime. The naming comes from linear logic.

ogogmad 4y ago

Linear types <- linear logic <- linear algebra. See here: See here: https://www.cs.bham.ac.uk/~drg/bll/steve.pdf https://www.cs.bham.ac.uk/~drg/bll/steve.pdf There's also "affine logic" which riffs on the same thing.

college_physics 4y ago
Ahh, thats cool. Thanks for the link

zetalyrae 4y ago

It comes from linear logic and that's as far as I know. It's not great because it can scare away programmers who hear "linear" and think abstract nonsense. But there's not really a better name. "Uniqueness type" or "Single-use type" is too verbose. I'd rather not bikeshed the terminology too much and just use what exists.

eternalban 4y ago
Disposable Type.
Nevermark 4y ago
“Single-instance” type? ”Single-reference”?
masklinn 4y ago
It's not just single-use, an affine type is also single-use: colloquially, a single-use item is not a must-use item.

bmacho 4y ago

Nothing, it just has the name for historic reasons.

dboreham 4y ago
I've been scratching my head over this all day since reading the beginning of the thread earlier. This is the one correct answer.
- naasking 4y ago
  This is not correct actually. It comes from linear logic, and it's connection to ordinary linear functions we all learned in school is clear if you think about it: any linear function f(x) can be written in a form where x appears only once on the right hand side, ie. f(x) = Bx + C. That's exactly the property linear typing enforces: a new binding only appears once on the right hand side, ie. let x = v in e, where e references x only once.
  - deleted 4y ago
    [deleted]

trenchgun 4y ago

> Girard himself, in his native language (cf. Girard, Cours de Logique I, Hermann, 2006, Section 1.B.2), writes: > "La logique linéaire est issue d'une prise en compte systématique de l'interprétation catégorique. En particulier, les espaces cohérents [...], proches des espaces vectoriels [...] font apparaître des structures logiques familières en algèbre linéaires [...]" > Translation: "Linear logic developed from systematically taking into consideration the categorical interpretation. In particular, coherent spaces [...], similar to vector spaces [...] give rise to logical structures which are familiar from linear algebra." > So, in one sentence, it is called linear logic because it involves semantics which resemble structures from linear algebra. https://math.stackexchange.com/questions/2339147/why-is-it-called-linear-logic https://math.stackexchange.com/questions/2339147/why-is-it-c...