Mozilla ought to chip in for the the research into what borrow checking is so it isn't maimed by function / abstraction boundaries. At that point do notation works fine.
Actually, I'm pretty sure it's a research limitation. It's not clear how lifetimes and locations (in the lvalues sense) relates to more traditional linear logic which is well understood. And this despite the existing research into regions.
I think lifetimes and lvalues are both reasonably straightforward to understand in terms of linear logic.
IMO, the main difficulty with adding monad-like abstractions to Rust actually lies elsewhere, in the fact that Rust doesn't really have function types -- or rather, it has too many of them. Roughly speaking, Rust does not have a function type constructor. Instead, every function you define in Rust gets its own special, unique type, which implements a function interface -- of which there are three, Fn, FnMut and FnOnce, to represent the different ownership states of the variables captured in a closure.
This means that monad-style interfaces involving higher-order functions and higher kinds will end up needing not just polymorphism over type constructors, but also constrained polymorphism over interfaces. This represents a much more substantial extension to Rust's type system than you might first expect.
The reason Rust does this is because if every definition gets its own type, then type inference can tell you very precisely which functions are called where, which makes inlining a lot more precise and effective. This is an important piece of how Rust turns (for example) iterator-heavy code into efficient loops -- there are actually many fewer indirect calls than it superficially looks like.
Personally, I think this was a design mistake, but it is also a choice that I would not revisit now. Once a system is in the wild, with users who depend on you, we are usually constrained to evolutionary development rather than radical redesigns.
I wouldn't think Rust's closure types are to blame. I would say Fn, FnMut, and FnOnce are a completely beside the point. In fact, Haskell, scared to worry about the differing structural properties of variables being closed over in its single function type, is about to adopt a substructure extension far weaker (and in my view inferior) to Rust's.
Rust has one (family of) function type(s) `fn(...) -> ...`. Well that and `for<...> fn(...) -> ...`. This is fine. Those traits are just sugar.
Bigger problems are that there is that there is
- No way to abstract over & vs &mut.
- Within a function, we can treat the initialized-ness of individual fields (really lvalues/locations broken down into trees), but across functions everything is initialized or some unsafe escape hatch.
- Lifetimes within a function are arbitrary subgraphs of the CFG, but between functions follow a LIFO discapline to model the stack. We have to break the so we have all 4 combinations. (Also, really the second type of lifetime should be a special stack management thing using with regular lifetimes and not an implicitly different sort of lifetime.)
My problem is not that "Rust just isn't dank enough", but that expressive power is great than its abstractive power: You can do more interesting things than you can hope to reuse. This I think creates some perverse incentives. Haskell (before this linear proposal at least) doesn't let you do anything you can't abstract over, even when it means less fancy tricks than Rust. I like those incentives better.
I’d be interested in some citations; I wasn’t aware of this. Then again it’s not my area of focus, so that’s not super surprising! We don’t do global type inference as a design decision, and since lifetimes are also generic types, I thought this was also the case. I think you can make a compelling argument that this inference would be bad, regardless of possibility.
https://arxiv.org/abs/1803.02796 has a good intro referencing other work. The paper doesn't go into much detail on the borrow checking side of things, but that author is both thoroughly steeped in the linear types research tradition and knows Rust and mentions it a bunch.
The fact that that paper talks about the affine types far more than the lifetimes obliquely illustrates my point in my view, I'm not sure if it's been stated more directly.
So in Rust today type inference strategies are less the point this hinges on. It's more about abolishing the difference between intra-procedural control flow / data flow / whatever, and their inter-procedural equivalents. Similarly, if we had an annotated version of the MIR which was borrow-check correct under composition that would also be good. NLL is great, and starts to clarify what borrow checking is, but running it in "whole" functions makes it to what clear it is a compositional analysis.
This way you can encode current binding environment into state and state changing code and have operations that use existing type checking and inference facilities of current Haskell (or Agda, or something else) compiler to rule out violations.
I keep saying that what is language feature in Rust, C#, C++, Java and some other currently hot programming languages is an ordinary library in Haskell.
It's more like it's hard to mix together built in and modeled notions together. Like I could hand-write some CPS and then compile that all go gotos, but if I forget to never return the invariant is broken and the compile fails. Monads in rust sort of work if you don't use any "native" control flow.
Comments
At least from Rust’s end, it is unclear if do notation is even possible, which is why we have pursued two special cases rather than it directly.
Mozilla ought to chip in for the the research into what borrow checking is so it isn't maimed by function / abstraction boundaries. At that point do notation works fine.
This is a design decision, not some inherent research limitation. And that’s not the main issue for do notation either.
Actually, I'm pretty sure it's a research limitation. It's not clear how lifetimes and locations (in the lvalues sense) relates to more traditional linear logic which is well understood. And this despite the existing research into regions.
I think lifetimes and lvalues are both reasonably straightforward to understand in terms of linear logic.
IMO, the main difficulty with adding monad-like abstractions to Rust actually lies elsewhere, in the fact that Rust doesn't really have function types -- or rather, it has too many of them. Roughly speaking, Rust does not have a function type constructor. Instead, every function you define in Rust gets its own special, unique type, which implements a function interface -- of which there are three, Fn, FnMut and FnOnce, to represent the different ownership states of the variables captured in a closure.
This means that monad-style interfaces involving higher-order functions and higher kinds will end up needing not just polymorphism over type constructors, but also constrained polymorphism over interfaces. This represents a much more substantial extension to Rust's type system than you might first expect.
The reason Rust does this is because if every definition gets its own type, then type inference can tell you very precisely which functions are called where, which makes inlining a lot more precise and effective. This is an important piece of how Rust turns (for example) iterator-heavy code into efficient loops -- there are actually many fewer indirect calls than it superficially looks like.
Personally, I think this was a design mistake, but it is also a choice that I would not revisit now. Once a system is in the wild, with users who depend on you, we are usually constrained to evolutionary development rather than radical redesigns.
Are you https://www.cl.cam.ac.uk/~nk480/ ??
I wouldn't think Rust's closure types are to blame. I would say Fn, FnMut, and FnOnce are a completely beside the point. In fact, Haskell, scared to worry about the differing structural properties of variables being closed over in its single function type, is about to adopt a substructure extension far weaker (and in my view inferior) to Rust's.
Rust has one (family of) function type(s) `fn(...) -> ...`. Well that and `for<...> fn(...) -> ...`. This is fine. Those traits are just sugar.
Bigger problems are that there is that there is
- No way to abstract over & vs &mut.
- Within a function, we can treat the initialized-ness of individual fields (really lvalues/locations broken down into trees), but across functions everything is initialized or some unsafe escape hatch.
- Lifetimes within a function are arbitrary subgraphs of the CFG, but between functions follow a LIFO discapline to model the stack. We have to break the so we have all 4 combinations. (Also, really the second type of lifetime should be a special stack management thing using with regular lifetimes and not an implicitly different sort of lifetime.)
My problem is not that "Rust just isn't dank enough", but that expressive power is great than its abstractive power: You can do more interesting things than you can hope to reuse. This I think creates some perverse incentives. Haskell (before this linear proposal at least) doesn't let you do anything you can't abstract over, even when it means less fancy tricks than Rust. I like those incentives better.
I’d be interested in some citations; I wasn’t aware of this. Then again it’s not my area of focus, so that’s not super surprising! We don’t do global type inference as a design decision, and since lifetimes are also generic types, I thought this was also the case. I think you can make a compelling argument that this inference would be bad, regardless of possibility.
https://arxiv.org/abs/1803.02796 has a good intro referencing other work. The paper doesn't go into much detail on the borrow checking side of things, but that author is both thoroughly steeped in the linear types research tradition and knows Rust and mentions it a bunch.
The fact that that paper talks about the affine types far more than the lifetimes obliquely illustrates my point in my view, I'm not sure if it's been stated more directly.
https://gallium.inria.fr/~fpottier/slides/fpottier-2007-05-l... has some nice history. It wish there is a newer version for things that have been published since, in case the issue is more resolved and I'm out of date.
So in Rust today type inference strategies are less the point this hinges on. It's more about abolishing the difference between intra-procedural control flow / data flow / whatever, and their inter-procedural equivalents. Similarly, if we had an annotated version of the MIR which was borrow-check correct under composition that would also be good. NLL is great, and starts to clarify what borrow checking is, but running it in "whole" functions makes it to what clear it is a compositional analysis.
Thanks!
So you're saying borrow checking is the one thing that can't be modelled as a monad?
You have to have parametrized monad [1] - a type like M inState outState result.
[1] http://blog.sigfpe.com/2009/02/beyond-monads.html
This way you can encode current binding environment into state and state changing code and have operations that use existing type checking and inference facilities of current Haskell (or Agda, or something else) compiler to rule out violations.
[2] https://jpaykin.github.io/papers/pz_linearity_monad_2017.pdf
I keep saying that what is language feature in Rust, C#, C++, Java and some other currently hot programming languages is an ordinary library in Haskell.
It's more like it's hard to mix together built in and modeled notions together. Like I could hand-write some CPS and then compile that all go gotos, but if I forget to never return the invariant is broken and the compile fails. Monads in rust sort of work if you don't use any "native" control flow.
Three special cases, I think? Future, Result, and Option.
Result and option are the same special case, the Try trait.