Linear types can change the world (1990) [pdf] | Hacker News Reader

Linear types can change the world (1990) [pdf]

cs.ioc.ee

95 pointsadamnemecek45 comments

GHC might get linear types: https://ghc.haskell.org/trac/ghc/wiki/LinearTypes

Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language [1]

I'm going to see the talk tomorrow at POPL, should be good.

[1] https://hal.archives-ouvertes.fr/hal-01673536/file/Linear%20...

To be honest I'm not very enthused about the way linear types are being added to Haskell. I think linear logic has a lot of potential to drastically change the way we approach programming and I'm not so interested in marginal improvements to current languages. I really like this paper [0] as an example of where we could be going. Note that the author is also part of the initiative to add linear types to GHC.

[0] http://assert-false.net/arnaud/papers/A%20dissection%20of%20...

What’s the essential difference between the approach described in the linked paper, and the one Haskell is taking? And what makes you favor the former?

In System L the evaluation contexts are first class and treated symmetrically with values. This goes beyond the functional paradigm. The Haskell proposal seeks to implement functional aspect of linear logic.

Is it still possible that the GHC garbage collector will be able to take advantage of linear types, and thus improve performance since it can free linear values after they’ve been consumed once?

I remember linear types for Haskell being presented as a way to get Rust-like performance in the cases where memory allocation/freeing is a bottleneck. But I’m not sure whether this has changed after further research.

There's no compelling evidence that that will be the case but it's possible in the far future. The emphasis at the moment is on correctness of resource usage.

Any discussion of Uniqueness or Linear types deserves a shoutout to Pony, which like Rust is built around the principle but in a really delightful way.

Also https://en.wikipedia.org/wiki/Clean_(programming_language)

What's a good language to try this out?

From the first few pages it seems to be really workable. I could see a good chunk of tailrecursive algorithms map neatly to constraints like nocopy and nodestroy

I'm no programming language nut, but it seems to me that in general if you have the language semantics to be able to explicitly narrow the capability of a structure it should lead to improvements when compiling (types in general do that as well). I remember playing around with ATS a little and it put a smile on my face that you could explicitly state that a function is tailrecursive, or mutually tailrecursive with another function. The other end of the spectrum is something like Scheme where it's not even clear from the semantics if you're capturing an environment or not! :) (which I still love and is really handy for writing stuff quick and simple, but I have no clue how a compiler has to work with that! No guarantees on mutability, stack size etc etc) ATS also is supposed to have linear types... so maybe I should revisit it some time

Rust is pretty much based around linear types (well I think technically it's a variant of that, I have heard about "affine types", don't know the difference), more precisely the move semantics.

EDIT: Oh, the expert has spoken while I was writing. See steveklabnic's answer !

> I have heard about "affine types", don't know the difference

A value with a linear type is used exactly once. A value with an affine type is used at most once. In other words, both types prevent double-use of single-use resources, but linear types additionally guarantee no leaks of said resources.

True linear types are far less common in practice, because in order to prove that a value is actually consumed, you have to prove that the program doesn't go into an infinite loop first. Which, y'know, good luck with that.

> Which, y'know, good luck with that.

Most dependent type systems like Agda, Coq, Idris, Lean, and ATS have termination checking, so it is possible! They can't determine whether arbitrary programs terminate, but you can capture a large subset of programs. Turns out most code doesn't actually need Turing completeness.

Since I've started paying attention, I've noticed that most of the code I write doesn't need anything more powerful than formal regular expressions, and vanishingly rarely needs to go beyond deterministic context-free.

Now you've got me curious :) Could you give some examples? I've never come across regular expressions outside of string handling

> True linear types are far less common in practice, because in order to prove that a value is actually consumed, you have to prove that the program doesn't go into an infinite loop first. Which, y'know, good luck with that.

I don't know much about the subject, but I just read the GHC proposal and it seems they don't consider this an issue:

https://ghc.haskell.org/trac/ghc/wiki/LinearTypes (see: "Isn't a linear function that diverges unsound?")

Key quote from your link (emphasis added):

> The properties of linear types which we need are not compromised by non-termination.

This is an implicit admission that Haskell "linear types" are not "true" linear types, but instead only have a subset of the defining properties.

I don't mean this in a disparaging fashion. Pretty much everyone uses the name "linear types" even though "affine types" is what they actually have. And I'm totally on-board with this. "Linear" is a more common word than "affine," and the defining difference isn't the property of linear types that most people care about (double-frees are a bigger deal than leaks). And, of course, the fact that you can't actually determine true linearity for Turing-Complete languages.

For what it's worth, it sounds like Haskell's "linear types" provides slightly more guarantees than true affine types, albeit less than true linear types.

Disclaimer: I am totally out of my field and I have no idea precise definitions of terms etc.

Is it haulting really in conflict with linear types?

If we inspect function from outside and we pick random time T after starting (but before finish) the event has been happen at most once. After function is finished event is done exactly once. I think conceptually situation is pretty much the same is T: 1ns | trillion years | infinite. So I feel that "It WILL happen after infinite time." is valid claim and therefore haulting by itself is not a problem.

In real world issue seems to be that we cannot run our software from very long to infinite time whenever is it haulted or not => at some point we kill that process. Killing process on the other hand is harmful thing for promise to run exactly once since killed process won't product anything new for sure. So in practice haulting results always to killing process but if process is killed it don't mean that process was haulted. So I claim that you shouldn't proof that your system won't hault but instead you should proof that process cannot be killed if anything. At the end it depends how we want box our world.

What you think?

You're right that proving that a program halts doesn't tell us whether or not it's practical to run (it could take 1 trillion years), but it can be useful for other reasons.

For example, if a function claims to return a value of type T, and we can prove that the function halts, then we know that a value of type T must exist (it's whatever the function will return, however long that takes).

This is how dependently typed languages can implement pre and post conditions: we can represent conditions as types, and put preconditions as extra argument types, and postconditions as extra return values (e.g. in a tuple).

For example, we might have a function 'f1' which turns 'A' values into 'B' values:

    f1 : A -> B
    f1 myA = ...

If we require some precondition 'PRE' to hold for the argument, and postcondition 'POST' to hold for the return value, we can use dependent types to represent them:

    f2 : (a : A) -> PRE a -> (b : B, POST b)
    f2 myA preProof = ...

We can 'f1' by just giving it an 'A' argument, but the precondition won't be checked. Likewise, we learn nothing about whether the output satisfies the postcondition.

With 'f2', we must give it an extra argument, representing a proof that the precondition holds for the given 'A' value. The function must also do more work: not only must it return a 'B' value, but it must also give us a proof that that 'B' value satisfies the postcondition (we can pass that proof around, e.g. if another function requires it as a precondition).

If we can prove that these calculations will halt, then we don't actually need to run them at all! Knowing that 'PRE a' can be proved in a finite amount of time (however long) is itself a proof of 'PRE a'! (And likewise for 'POST b'). Hence we can "erase" this proof stuff after type checking, to generate code equivalent to 'f1'.

If we don't know whether or not those proof calculations will halt, we can't use this shortcut, and we're forced to run the proof calculations in full at runtime (which may not halt, or might take a trillion years!).

In your f2 example, could you ever use/inspect the preProof argument? If the proof calculation is erased, I assume preProof could never be used in any way. Although depending on what the type PRE really is it might not be something you could do anything useful with in the first place.

I should probably learn Idris already, that would probably clear up these questions. :)

> In your f2 example, could you ever use/inspect the preProof argument?

Yes you could, but if your return value relies on details of the proof (e.g. branching on different cases) then it may no longer be erasable. Unless those parts of the return value can also be erased... it gets tricky :)

You're right to mention Idris, since it treats proofs in this way. In languages like ATS, there is a clear separation between erasable "proof-like" things and runtime "value-like" things, which makes things more predictable, but can lead to duplication.

Interesting! Thanks

> I have heard about "affine types", don't know the difference

Linear types: must be used exactly once

Affine types: can't be used more than once

Rust has affine types, but not true linear types. Some people refer to both kinds as "linear", as there's not a ton of difference, but in another perspective, there is a ton of difference. https://gankro.github.io/blah/linear-rust/

Linear types are incoming in Haskell and afaik Idris has uniqueness types, or did at one point. Haskell is closing the gap on Idris with dependent types (slowly) so you may want to get comfy with Haskell. It’s a good first step, anyway.

Aren't Rust's lifetimes closely related to linear types?

If so, they are changing the world already.

A few years ago I would have suggested LinearML - https://github.com/pikatchu/LinearML.

Now it may be quite a challenge, to just compile it.

Their siblings, affine types, change the world in the form of Rust. ;)

Relevant: https://hyper.rs/hyper/v0.9.6/hyper/client/request/struct.Re...

Could you elaborate? There isn’t much of a discussion there of the benefits from making Request affine.

headers_mut is only defined on Request<Fresh>, and you can only write body data using Request<Streaming>. This makes it so it's a type error to try to modify the headers after you already sent them.

Is this about organizing side-effects in a way that compilers can optimize?

I think you could say that. Another way to look at it would be to say it's about organising your code in such a way that side-effects don't really matter. For instance, if only I have access to a reference, then I'm free to update it without risk of disrupting anyone else's world view. You could say that there is no side-effect from my update because no-one can observe the change.

This is nice for functional programming because it gives you the performance of mutable state and destructive update, but in a way that is 'pure', or side-effect free, from the outside.

I asked myself a bit of a related question. Is this theory related to https://en.m.wikipedia.org/wiki/Static_single_assignment_for... ?

I think SSA is related to CPS, but I'm not sure of the correspondence with Linearity. I think the key difference (but I'm not sure), is that SSA only asserts that a variable is assigned once, but might be consumed multiple times. Linearity says that things must be consumed exactly once. For instance, I think:

y <- x + 1

z <- x + 2

is a legal SSA expression, but it is not a legal linear expression because x appears twice.

(Corrections welcome)

FWIW:

https://www.cs.princeton.edu/~appel/papers/ssafun.ps

It’s always fun to look at the flow of knowledge from academia to the industry, and how some things can take decades.

Reminds me of LinearML which was an experiment nearly 10 years ago.

https://github.com/pikatchu/LinearML/blob/b1a49f153e02f3cffb...

After 17 years I think we can say they did not change the world!

The author of the paper doesn't mean that the concept of linear types will change the world, but states that linear types combined with functional languages will be able to interact with and change the real world (I/O, graphics, etc). This is because functional languages have a hard time representing these concepts, and have alternate workarounds (monads).

Lisp ideas didn't caught on until 40+ years, so...

Not to mention that the first digital computer appeared in the 30s or so, and it took until 1980s and on to really say it "changed the world" (as opposed to merely improving the speed of some calculations).

Add 10 more years :)

lol ok we'll check back then, you and i

edit: haha!! just got what you said and realized my mistake :o

So, why haven't they yet as 25 years have passed?

It is nor like they are hard or expensive to implement, more like nobody cares and the claim is overblown. Most mistakes in software are in boundary conditions nowadays and not invalid type handling.

Enforcing immutability is great until you get to deal with big number of additional values of immutable types because you cannot modify them. Easy to reason about, bad for performance.

Linear types are different from immutable types. You can change the value of a linear type as long as you used the previous value somewhere else (for example i = i + 1). Languages like Rust leverage affine types (another substructural type system similar to linear type systems) in order to guarantee memory safety.

They haven't yet, but they will. Let's wait a few more years.

I think Rust is – at the moment – the biggest language that will usher that change.

Reply on news.ycombinator.com