Hacker News Reader

Comment by college_physics | Hacker News Reader

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.

View on HN

Linear types <- linear logic <- linear algebra. See here: See here: https://www.cs.bham.ac.uk/~drg/bll/steve.pdf

There's also "affine logic" which riffs on the same thing.

Ahh, thats cool. Thanks for the link

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

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.

> 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-c...

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.

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.

Disposable Type.

“Single-instance” type?

”Single-reference”?

It's not just single-use, an affine type is also single-use: colloquially, a single-use item is not a must-use item.

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

Nothing, it just has the name for historic reasons.

I've been scratching my head over this all day since reading the beginning of the thread earlier. This is the one correct answer.

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.

Reply on news.ycombinator.com