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

http://www.cs.ioc.ee/ewscs/2010/mycroft/linear-2up.pdf

by adamnemecek • 9 years ago

95 45 9 years ago

cs.ioc.ee

qznc• 9 years ago

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

sprt• 9 years ago

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

tomjakubowski• 9 years ago

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

danharaj4• 9 years ago

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

johnbender• 9 years ago

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

danharaj4• 9 years ago

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

runeks2• 9 years ago

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.

danharaj4• 9 years ago

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.

KirinDave• 9 years ago

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.

steveklabnik3• 9 years ago

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

blurbleblurble• 9 years ago

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

bsaul2• 9 years ago

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

jw-2• 9 years ago

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)

kthielen• 9 years ago

FWIW:

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

jw-2• 9 years ago

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.

geokon2• 9 years ago

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

efnx• 9 years ago

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.

steveklabnik3• 9 years ago

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/

navaati• 9 years ago

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 !

steveklabnik3• 9 years ago

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

lmkg2• 9 years ago

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.

nine_k• 9 years ago

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

If so, they are changing the world already.

vrotaru• 9 years ago

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.

moocowtruck2• 9 years ago

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

bsaul2• 9 years ago

Add 10 more years :)

moocowtruck2• 9 years ago

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

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

kbr2• 9 years ago

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

coldtea• 9 years ago

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

AstralStorm• 9 years ago

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.

kbr2• 9 years ago

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.

GolDDranks• 9 years ago

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.

amenghra• 9 years ago

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

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

Related Stories