3 ms·

> Ownership semantics are a form of an affine substructural type system1112 which means that they are fundamentally described by a linear logic, and explains wh

> Ownership semantics are a form of an affine substructural type system1112 which means that they are fundamentally described by a linear logic, and explains why it struggles to express non-linear problems What is a “non linear logic” or a “non linear problem “ in this context?

chrismorgan 6y ago
Linked lists and graphs are the canonical examples of things that are difficult to model and express effectively in Rust. In other languages you can just store a pointer/handle/reference to the things each node is connected to, which is commonly not the most efficient way of working (and as systems scale up they routinely replace such techniques with fancier techniques), but is very straightforward conceptually and matches people’s intuitions about how to design such a thing. In Rust, you simply can’t do that directly, roughly because it’s not provably safe (in fact, in the general case, it’s provably not safe). So you have to solve things in other ways, the simplest being to wrap each node in Rc<RefCell<_>> or similar, which is basically a way of saying “I can’t cope with ownership semantics, gimme a kludgy way of checking it at runtime”; but it’s also common to immediately reach for fancier data structures like https://lib.rs/crates/petgraph https://lib.rs/crates/petgraph. Yet even with that, you’re often spitting in the face of ownership semantics with your traversals, because traversing a potentially-cyclic graph is fundamentally against ownership semantics, so you have to be careful because some things will be being checked at runtime. In the case of these fancier data structures, it is perhaps also worth pointing out that many of them actually do follow ownership semantics, down to things like allowing shared access to multiple nodes, or exclusive access to a single node, so that no runtime checks are necessary. This is where I think the original article severely missteps in calling it a fatal flaw—because people are successfully building safe ownership-oriented abstractions using unsafe code. That’s a super-important capability of Rust.
- johnnycerberus 6y ago
  Even in Java I have problems with non-linear stuff. Clojure is my favorite when it comes to graphs and algorithms that require highly dynamic data structures. I'm not experienced in Rust (but read most of the open-source programming book), but isn't it possible to use macros to create a DSL that can describe those structures? Is this what petgraph does?
- gingerBill 6y ago
  I have noticed loads of people are commenting on the "fatal flaw" bit of the title. It is a click-bait title, and if it was anything else, no one would be commenting on the post in the first place. "A Critique of Ownership Semantics" is less interesting to click on than "The Fatal Flaw of Ownership Semantics".
monocasa 6y ago
I think they're talking about arbitrary graphs and operations on those graphs.
funcDropShadow 6y ago
Phil Wadler has several "nice" papers about linear logics, e.g. this one: http://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lineartaste-revised.pdf http://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/line... By nice I mean, nice if you are willing to deal papers about formal logic. Which excludes pretty much most people on this planet. But you asked. To put it in my own words, and bear in mind that the last time I've worked with linear logic was 15 years ago. A linear logic restricts how often you are allowed to use a proposition in a derviation or proof tree. The borrow checker is more like a linear type system. In linear type systems you restrict how often an identifier of a linear typed variable may be used. See, e.g. Phil Wadler's paper "Linear types can change the world", where he explores the idea to use linear types as an alternative to model the World(tm) in pure functional programming, i.e. an alternative to the IO monad.

chrismorgan 6y ago

Linked lists and graphs are the canonical examples of things that are difficult to model and express effectively in Rust. In other languages you can just store a pointer/handle/reference to the things each node is connected to, which is commonly not the most efficient way of working (and as systems scale up they routinely replace such techniques with fancier techniques), but is very straightforward conceptually and matches people’s intuitions about how to design such a thing. In Rust, you simply can’t do that directly, roughly because it’s not provably safe (in fact, in the general case, it’s provably not safe). So you have to solve things in other ways, the simplest being to wrap each node in Rc<RefCell<_>> or similar, which is basically a way of saying “I can’t cope with ownership semantics, gimme a kludgy way of checking it at runtime”; but it’s also common to immediately reach for fancier data structures like https://lib.rs/crates/petgraph https://lib.rs/crates/petgraph. Yet even with that, you’re often spitting in the face of ownership semantics with your traversals, because traversing a potentially-cyclic graph is fundamentally against ownership semantics, so you have to be careful because some things will be being checked at runtime. In the case of these fancier data structures, it is perhaps also worth pointing out that many of them actually do follow ownership semantics, down to things like allowing shared access to multiple nodes, or exclusive access to a single node, so that no runtime checks are necessary. This is where I think the original article severely missteps in calling it a fatal flaw—because people are successfully building safe ownership-oriented abstractions using unsafe code. That’s a super-important capability of Rust.

johnnycerberus 6y ago
Even in Java I have problems with non-linear stuff. Clojure is my favorite when it comes to graphs and algorithms that require highly dynamic data structures. I'm not experienced in Rust (but read most of the open-source programming book), but isn't it possible to use macros to create a DSL that can describe those structures? Is this what petgraph does?
gingerBill 6y ago
I have noticed loads of people are commenting on the "fatal flaw" bit of the title. It is a click-bait title, and if it was anything else, no one would be commenting on the post in the first place. "A Critique of Ownership Semantics" is less interesting to click on than "The Fatal Flaw of Ownership Semantics".

monocasa 6y ago

I think they're talking about arbitrary graphs and operations on those graphs.

funcDropShadow 6y ago

Phil Wadler has several "nice" papers about linear logics, e.g. this one: http://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lineartaste-revised.pdf http://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/line... By nice I mean, nice if you are willing to deal papers about formal logic. Which excludes pretty much most people on this planet. But you asked. To put it in my own words, and bear in mind that the last time I've worked with linear logic was 15 years ago. A linear logic restricts how often you are allowed to use a proposition in a derviation or proof tree. The borrow checker is more like a linear type system. In linear type systems you restrict how often an identifier of a linear typed variable may be used. See, e.g. Phil Wadler's paper "Linear types can change the world", where he explores the idea to use linear types as an alternative to model the World(tm) in pure functional programming, i.e. an alternative to the IO monad.