15 ms·

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

95 points by adamnemecek 9y ago

qznc 9y ago
Their siblings, affine types, change the world in the form of Rust. ;)
- sprt 9y ago
  Relevant: https://hyper.rs/hyper/v0.9.6/hyper/client/request/struct.Request.html https://hyper.rs/hyper/v0.9.6/hyper/client/request/struct.Re...
  - tomjakubowski 9y ago
    Could you elaborate? There isn’t much of a discussion there of the benefits from making Request affine.
    - carry_bit 9y ago
      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.
- deleted 9y ago
  [deleted]
danharaj 9y ago
GHC might get linear types: https://ghc.haskell.org/trac/ghc/wiki/LinearTypes https://ghc.haskell.org/trac/ghc/wiki/LinearTypes
- johnbender 9y 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%20Haskell%20practical%20linearity%20in%20a%20higher-order%20polymorphic%20language.pdf https://hal.archives-ouvertes.fr/hal-01673536/file/Linear%20...
  - danharaj 9y 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%20L.pdf http://assert-false.net/arnaud/papers/A%20dissection%20of%20...
    - runeks 9y ago
      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?
      - danharaj 9y ago
        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.
- runeks 9y 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.
  - danharaj 9y 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 9y 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.
- steveklabnik 9y ago
  Also https://en.wikipedia.org/wiki/Clean_(programming_language) https://en.wikipedia.org/wiki/Clean_(programming_language)
macawfish 9y ago
Is this about organizing side-effects in a way that compilers can optimize?
- bsaul 9y ago
  I asked myself a bit of a related question. Is this theory related to https://en.m.wikipedia.org/wiki/Static_single_assignment_form https://en.m.wikipedia.org/wiki/Static_single_assignment_for... ?
  - jw- 9y 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 9y ago
    FWIW: https://www.cs.princeton.edu/~appel/papers/ssafun.ps https://www.cs.princeton.edu/~appel/papers/ssafun.ps
- jw- 9y 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.
geokon 9y 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 9y 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.
- steveklabnik 9y 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/ https://gankro.github.io/blah/linear-rust/
- navaati 9y 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 !
  - steveklabnik 9y ago
moocowtruck 9y ago
After 17 years I think we can say they did not change the world!
- bsaul 9y ago
  Add 10 more years :)
  - moocowtruck 9y ago
    lol ok we'll check back then, you and i edit: haha!! just got what you said and realized my mistake :o
- kbr 9y 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 9y 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 9y 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.
- kbr 9y 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 9y 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 9y 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/b1a49f153e02f3cffb32784f2eeb7fca017b2791/README https://github.com/pikatchu/LinearML/blob/b1a49f153e02f3cffb...

95 points by adamnemecek 9y ago

qznc 9y ago

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

sprt 9y ago
Relevant: https://hyper.rs/hyper/v0.9.6/hyper/client/request/struct.Request.html https://hyper.rs/hyper/v0.9.6/hyper/client/request/struct.Re...
- tomjakubowski 9y ago
  Could you elaborate? There isn’t much of a discussion there of the benefits from making Request affine.
  - carry_bit 9y ago
    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.
deleted 9y ago
[deleted]

danharaj 9y ago

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

johnbender 9y 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%20Haskell%20practical%20linearity%20in%20a%20higher-order%20polymorphic%20language.pdf https://hal.archives-ouvertes.fr/hal-01673536/file/Linear%20...
- danharaj 9y 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%20L.pdf http://assert-false.net/arnaud/papers/A%20dissection%20of%20...
  - runeks 9y ago
    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?
    - danharaj 9y ago
      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.
runeks 9y 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.
- danharaj 9y 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 9y 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.

steveklabnik 9y ago
Also https://en.wikipedia.org/wiki/Clean_(programming_language) https://en.wikipedia.org/wiki/Clean_(programming_language)

macawfish 9y ago

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

bsaul 9y ago
I asked myself a bit of a related question. Is this theory related to https://en.m.wikipedia.org/wiki/Static_single_assignment_form https://en.m.wikipedia.org/wiki/Static_single_assignment_for... ?
- jw- 9y 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 9y ago
  FWIW: https://www.cs.princeton.edu/~appel/papers/ssafun.ps https://www.cs.princeton.edu/~appel/papers/ssafun.ps
jw- 9y 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.

geokon 9y 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 9y 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.
steveklabnik 9y 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/ https://gankro.github.io/blah/linear-rust/
navaati 9y 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 !
- steveklabnik 9y ago

moocowtruck 9y ago

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

bsaul 9y ago
Add 10 more years :)
- moocowtruck 9y ago
  lol ok we'll check back then, you and i edit: haha!! just got what you said and realized my mistake :o
kbr 9y 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 9y 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 9y 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.

kbr 9y 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 9y 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 9y 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/b1a49f153e02f3cffb32784f2eeb7fca017b2791/README https://github.com/pikatchu/LinearML/blob/b1a49f153e02f3cffb...