5 ms·

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 neatl

by 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
  > 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
- lmkg 9y 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.
  - mcaruso 9y ago
    > 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 https://ghc.haskell.org/trac/ghc/wiki/LinearTypes (see: "Isn't a linear function that diverges unsound?")
    - lmkg 9y ago
      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.
nine_k 9y ago
Aren't Rust's lifetimes closely related to linear types? If so, they are changing the world already.
vrotaru 9y ago
A few years ago I would have suggested LinearML - https://github.com/pikatchu/LinearML https://github.com/pikatchu/LinearML. Now it may be quite a challenge, to just compile it.

by geokon 9y ago

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
> 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
lmkg 9y 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.
- mcaruso 9y ago
  > 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 https://ghc.haskell.org/trac/ghc/wiki/LinearTypes (see: "Isn't a linear function that diverges unsound?")
  - lmkg 9y ago
    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.

nine_k 9y ago

Aren't Rust's lifetimes closely related to linear types? If so, they are changing the world already.

vrotaru 9y ago

A few years ago I would have suggested LinearML - https://github.com/pikatchu/LinearML https://github.com/pikatchu/LinearML. Now it may be quite a challenge, to just compile it.