Hacker News Reader

Comment by AnimalMuppet | Hacker News Reader

This has been bugging me for a while: Why are type names what they are? I get why sum types and product types are named what they are.

But linear types? A value can be used only once? Cool. We call that "linearity"? Um, what? What's linear about that?

View on HN

Vector spaces and linear maps between them form a model of the linearly-typed lambda calculus. That is, each type can be interpreted as a vector space, with each well-typed term representing a linear map between vector spaces.

1. The linear tensor product A ⊗ B gets interpreted as the tensor product of vector spaces.

2. The linear function space A ⊸ B gets interpreted as the vector space of linear functions between A and B.

3. The Cartesian product A × B gets interpreted as the direct product of vector spaces (i.e., the categorical product).

4. The sum type A + B gets interpreted as the direct sum of vector spaces (i.e., the categorical coproduct).

5. The exponential !A gets interpreted by the Fock space construction.

This explains why the choice of name is sensible, but I don't actually know if that was the reason why Jean-Yves Girard named it so. If memory serves, he invented linear logic after thinking about Berry's notion of stable functions, but I don't know for sure when the vector space model was invented. (It's not in his 1987 paper, but it can't have appeared very long after that.)

Are vector spaces really the right category? In particular the product and coproduct of vector spaces are isomorphic (both isomorphic to the direct sum).

It depends on what you mean by right category. It is true that vector spaces identify certain constructs that linear logic distinguishes, but it doesn't identify everything so it still has some interesting content. Finding models that don't make unnecessary identifications is one of main lines of research in the field.

They're not the right category for computation, but they are a valid interpretation of linear typing. They're one of Girard's original inspirations for linear logic. The resource interpretation came later.

Is there an explanation out there about the vector space model? Perhaps one that relates to Gir87's phase semantics?

The reasoning is sort of a technical analogy. Linear Logic was discovered by an analysis of the structure of Coherent Spaces, which are a model of Intuitionistic logic distilled from Scott domains. Jean-Yves Girard realized that function spaces A => B can be decomposed into two finer constructions as !A -o B where `A -o B` is a space of functions whose properties resemble linear functions between vector spaces and `!A` resembles the Fock space construction on a vector space.

There are two ways this resemblance manifests.

First off, the basic elements of a coherent space are called cliques which are analogous to vectors in a vector space. The functions constituting the coherent space A => B preserve directed unions of cliques but the linear functions of A -o B preserve arbitrary unions of cliques which is strongly analogous to preserving arbitrary linear combinations of vectors.

Second off is that you can build a symmetric monoidal category out of coherent spaces and vector spaces are the archetypal symmetric monoidal category. There are models of fragments of Linear Logic where the linear functions are literally polynomials of degree 1, but in its full generality it doesn't quite match exactly with linear algebra.

Nonetheless the metaphor goes deep and you can even capture notions of differentiability in extensions to the logic.

For a technical exposition you can read this paper by a guy who's applying this sort of stuff to machine learning: https://arxiv.org/abs/1407.2650 I apologize if this is all too obscure to justify the name. Linear Logic's applications to programming were sort of secondary to its proof theoretic novelty at its inception.

This is the intuition I have: In algebra, a function or operator f(x) is generally thought of as linear if f(a * x + b * y) = a * f(x) + b * f(y). A linear function f(x) can only "use" x once in a multiplication. For example, the function f(x) = 1 is not linear (f(1+1) != f(1)+f(1)) as it only uses x zero times[0]. Similarly, the function f(x) = x * x is not linear. On the other hand, if x is only used once (after factoring), the function can be linear. Indeed, f(x) = k * x satisfies the linearity condition so long as k does not "use" x. Note that this is obviously not a sufficient condition, it's just an intuition.

[0]: this requires you to discard the intuition that a linear function looks like a line when plotted.

> this requires you to discard the intuition that a linear function looks like a line when plotted

To be more precise, linear functions correspond to lines/planes/etc passing through the origin since f(0)=0

So I can't make a linear function that returns a number cubed?

Math.pow(x,y) cannot be made into a linear function?

no.

Why would mult(x,y) be linear then if x has to be used more than once in order to do the actual multiplication?

Sorry, I got confused on the meaning linear.

As explained in the other answer, it's possible to implement the power function which is "type-linear" on each argument, but that function will not otherwise be linear (ie, the mathematical meaning of linear) on its arguments.

In Rust for instance, affine types are used to restrict usage of values linearly, which means that a value passed as argument will be by default moved from caller to callee: The value will not be available anymore to the caller. This has some consequences for instance for binary operators on values which require special care when moved (structures, arrays): with the restriction explained above, a value cannot be passed more than once to a function, and thus doing something like 'mult(x,x)' (where x is eg. a matrix) will not work because x appears twice, but may only be moved once. The solution offered by the language, called "borrowing" is to use references for the arguments: a borrowed value is no longer being moved; instead, it remains in the scope of the caller, and the callee only receives a reference. References may be created and duplicated, allowing multiple uses of the same piece of data.

Forgive me but if we actually have to implement mathematics from pure computational theory, wouldn't type-linear functions be equivalent to actual mathematical linear functions?

Well, if copies may be borrowed, as it is the case in Rust, I suppose that a type-linear function, as I called it, doesn't have to be computationally linear. The `mult` example we discussed could not be applied twice to the same value, unless it is declared as borrowing its parameters from the caller.

Elaborating on this, with a function signature like the following:

    fn mult(x : Vec<f32>, y : Vec<f32>) -> Vec<f32> {
       // matrix product implementation 
    }

arguments x and y cannot point to the same value, because a value cannot be moved twice. A call like

    mult(a,a)

will generate an error.

Conversely, with the following signature:

    fn mult(x : &Vec<f32>, y : &Vec<f32>) -> Vec<f32> {
       // ...
    }

the call:

    mult(&a,&a)

will typecheck, because values are passed by reference.

Now, nothing prevents one to implement the function square, based on the second version of mult:

    fn square(x : Vec<f32>) -> Vec<f32> {
        return mult(&x,&x)
    }

which is type-linear on its parameter x, but computationally is not linear.

Clearly your original question was spot on.

I see what you mean with the copying. I just thought based on OPs comments there would have been a strong correspondence between lambda calculus numbers (Church encoding) and the operations on them, and actual type-linear functions.

You're taking the intuition a little too far, I think. If we're talking about linear types, Math.pow can be linear because you can _copy_ the value x as many times as you want. As far as memory management is concerned, the x that was passed in was only used once (to make however many copies).

Because you can see their usage as a series of "points" linked to exactly one other point, that forms a "line", as opposed to other systems where you could have more of a graph or tree.

The original name was because the logic seemed to do with time. If some proposition p is true, and then some event q comes along and we can derive "if p and q then r" then now we know that r is true, but we can no longer be sure that p is still true. Maybe the derivation of r was an event or it transformed the nature of p in some way and we can't go back. People don't really think of linear logic as being temporal (one thing happening after another) anymore, the "resource interpretation" is more common, although still not 100% accurate. In this view, p is a resource that is consumed by q when r is derived. The logic/axioms are the same in both cases, it's just what people's subjective intuition says the logic describes. If linear logic finds its way into mainstream programming, it will probably be just in the simplified sense of "use-once function" like you called it, which is a little bit like calling lambda calculus using functions without names.

They're linear because they can only be used once. If you draw out the set of 'references' to the object in a timeline it'll always be a line, whereas with a non-linear object, it could be any DAG.

https://en.wikipedia.org/wiki/Substructural_type_system#Line...

That doesn’t really answer his question.

https://math.stackexchange.com/questions/2339147/why-is-it-c...

Apparently there is some connection to vector spaces in the structure of linear logic which linear types are based on.

Reply on news.ycombinator.com