4 ms·

The 'use-once variable' described in the OP is the intellectual ancestor of Rust's borrow checker. It got a lot of attention from programming-languages research

The 'use-once variable' described in the OP is the intellectual ancestor of Rust's borrow checker. It got a lot of attention from programming-languages researchers (such as the author of the OP) after it got a lot of attention from academic logicians after the publication in 1987 by logician Jean-Yves Girard of a seminal paper entitled 'Linear Logic', the full text of which is available at https://www.sciencedirect.com/science/article/pii/0304397587900454 https://www.sciencedirect.com/science/article/pii/0304397587... That paper is the most abstract, airy, 'ungrounded' paper I have ever read that will probably have a significant positive practical impact on human flourishing (via Rust's borrow checker).

opnitro 7y ago
More specifically, while linear logic grants the 'must use-once variable', Rust implements "affine types", where values must be used no more than once.
- kibwen 7y ago
  Though in this case I don't think there's much need to make that distinction, since Rust's choice of affine types over linear types is a result of desire for user-friendliness, rather than (AFAICT) any type-theoretic constraint. Indeed, it's not hard to argue that Rust would be even simpler with linear types rather than affine types, although the cost would be that a user would be forced to explicitly invoke the destructors (in the right order!) for every owned variable in the program rather than relying on RAII to elide all that (of course sometimes such a power turns out to be quite useful, which is why std::mem::ManuallyDrop exists https://doc.rust-lang.org/std/mem/struct.ManuallyDrop.html https://doc.rust-lang.org/std/mem/struct.ManuallyDrop.html ).
- cwzwarich 7y ago
  Strictly speaking, Rust doesn't even have affine types, since even move-once variables can be borrowed multiple times before they are moved. You could argue that Rust could be elaborated into a system with affine types, but the elaboration isn't particularly simple in all cases.
  - hollerith 7y ago
    I prefer to think of a reference to a type as a type in its own right separate from the borrowed type. Looked at that way, Rust does have affine types. To bring the discussion back to my first comment, it would've been less likely for anyone to have invented the borrow checker if programming-languages researchers weren't paying a lot of attention to use-once variables, and languages researchers would've been less likely to be paying attention were it not for Girard. I haven't read Girard's paper in 20 years, but I would be extremely surprised if it contained any mention of borrowing or references, so Girard must share any credit for Rust's borrow checker with later innovators, and here I would be remiss not to mention Graydon Hoare.
    - cwzwarich 7y ago
      > I prefer to think of a reference to a type as a type in its own right separate from the borrowed type. Looked at that way, Rust does have affine types. The reference type is a separate type, but the & borrowing operator is a use of the original path. You can borrow (i.e. use) the same path multiple times before it is moved or implicitly destroyed.
      - hollerith 7y ago
        Good point: my assertion in grandparent that "Rust does have affine types" is wrong. Do you agree with my belief that it is significantly less likely the borrow checker would've been invented if programming-languages researchers hadn't paid a lot of attention to linear and affine types? Even though a Rust coder can take as many non-mutable references to a location in memory as he wants, there are certain operations (e.g., move) that the coder can only do once to it, and the inventor(s) (probably Graydon Hoare) of the borrow checker must have explored that part of the design space extensively, and it seems to me it would have been very non-obvious that it was worth exploring extensively to someone not influenced directly or indirectly by Girard.
        cwzwarich 7y ago
        > Do you agree with my belief that it is significantly less likely the borrow checker would've been invented if programming-languages researchers hadn't paid a lot of attention to linear and affine types? As I mentioned in another comment, the concept of borrowing was already present in the earliest applications of linear types to programming languages. There was contemporaneous research into region systems for ML. Later languages like Vault and Cyclone combined these two ideas, using substructural types to manage regions. From a language feature perspective, the biggest innovation of Rust was integrating the ideas from Cyclone and other research languages with the emerging C++11 style of programming with implicit destructors, move semantics, and smart pointers.
derriz 7y ago
I remember really liking his book Proofs and Types which was a revelation after struggling with Martin-Löf’s writings. One outcome of that attention was a nice and blazingly fast for an FPL called Clean which offered a more modern Haskell/MLish syntax. Actually came across this previous discussion while searching for a link: https://news.ycombinator.com/item?id=15937597 https://news.ycombinator.com/item?id=15937597

opnitro 7y ago

More specifically, while linear logic grants the 'must use-once variable', Rust implements "affine types", where values must be used no more than once.

kibwen 7y ago
Though in this case I don't think there's much need to make that distinction, since Rust's choice of affine types over linear types is a result of desire for user-friendliness, rather than (AFAICT) any type-theoretic constraint. Indeed, it's not hard to argue that Rust would be even simpler with linear types rather than affine types, although the cost would be that a user would be forced to explicitly invoke the destructors (in the right order!) for every owned variable in the program rather than relying on RAII to elide all that (of course sometimes such a power turns out to be quite useful, which is why std::mem::ManuallyDrop exists https://doc.rust-lang.org/std/mem/struct.ManuallyDrop.html https://doc.rust-lang.org/std/mem/struct.ManuallyDrop.html ).
cwzwarich 7y ago
Strictly speaking, Rust doesn't even have affine types, since even move-once variables can be borrowed multiple times before they are moved. You could argue that Rust could be elaborated into a system with affine types, but the elaboration isn't particularly simple in all cases.
- hollerith 7y ago
  I prefer to think of a reference to a type as a type in its own right separate from the borrowed type. Looked at that way, Rust does have affine types. To bring the discussion back to my first comment, it would've been less likely for anyone to have invented the borrow checker if programming-languages researchers weren't paying a lot of attention to use-once variables, and languages researchers would've been less likely to be paying attention were it not for Girard. I haven't read Girard's paper in 20 years, but I would be extremely surprised if it contained any mention of borrowing or references, so Girard must share any credit for Rust's borrow checker with later innovators, and here I would be remiss not to mention Graydon Hoare.
  - cwzwarich 7y ago
    > I prefer to think of a reference to a type as a type in its own right separate from the borrowed type. Looked at that way, Rust does have affine types. The reference type is a separate type, but the & borrowing operator is a use of the original path. You can borrow (i.e. use) the same path multiple times before it is moved or implicitly destroyed.
    - hollerith 7y ago
      Good point: my assertion in grandparent that "Rust does have affine types" is wrong. Do you agree with my belief that it is significantly less likely the borrow checker would've been invented if programming-languages researchers hadn't paid a lot of attention to linear and affine types? Even though a Rust coder can take as many non-mutable references to a location in memory as he wants, there are certain operations (e.g., move) that the coder can only do once to it, and the inventor(s) (probably Graydon Hoare) of the borrow checker must have explored that part of the design space extensively, and it seems to me it would have been very non-obvious that it was worth exploring extensively to someone not influenced directly or indirectly by Girard.
      - cwzwarich 7y ago
        > Do you agree with my belief that it is significantly less likely the borrow checker would've been invented if programming-languages researchers hadn't paid a lot of attention to linear and affine types? As I mentioned in another comment, the concept of borrowing was already present in the earliest applications of linear types to programming languages. There was contemporaneous research into region systems for ML. Later languages like Vault and Cyclone combined these two ideas, using substructural types to manage regions. From a language feature perspective, the biggest innovation of Rust was integrating the ideas from Cyclone and other research languages with the emerging C++11 style of programming with implicit destructors, move semantics, and smart pointers.

derriz 7y ago

I remember really liking his book Proofs and Types which was a revelation after struggling with Martin-Löf’s writings. One outcome of that attention was a nice and blazingly fast for an FPL called Clean which offered a more modern Haskell/MLish syntax. Actually came across this previous discussion while searching for a link: https://news.ycombinator.com/item?id=15937597 https://news.ycombinator.com/item?id=15937597