I learned about this topic through the convenient “Rust-internals summary”. I think that the proposed design does not work, and will explain why (both on a practical and theoretical level). The topic may have been left to sleep instead, but in my experience language questions tend to come back as they stay on people’s mind, so it is interesting to gather feedback and criticism in a central place.
First, I would like to point out that the proposal’s justification in terms of a Correspondence Principle is built on a misinterpretation or misuse of said principle.
The principle says: abstracting a function and then immediately calling it ((|| { ... })()) is the same as running the code directly. This is a special case of an operation that has been know since the 1930s, called beta-reduction (the greek letter β), that says that a function call can be understood by replacing it with the function body, where the formal parameters have been replaced by the value of the call’s arguments. This is all just fine. But the following translation, part of the first post, is not:
For a given expression expr, || expr should be equivalent.
Notice that on the right side, we are now talking about (|| expr), not (|| expr)(). This is completely wrong! This equivalence fails as soon as expr is a printing statement for example (the left expression prints, the right doesn’t). This might be a typo, but this typo is necessary to understand the proposed code example
fn main() {
// `return` would be a divergent expression and return from `main`
let id: i32 = "321".parse().or_else(|| return);
}
In here as well, || return is not applied.
Then, a general point on language design: as soon as you start doing things that are not obvious, discussing between several choices (where to return, for example), a generally safe approach is to start naming things. goto is a feature worth complaining about in various ways, but it did get one thing exactly right: when you have non-local control flow, it is safer if you name the places where you want to go (labels). If you want to introduce non-local control flow in Rust, any rule such as “well if it’s an anonymous function we could say that return goes to the outer one” should be killed with fire. If you don’t do the normal things, you should be more explicit about it, through naming. (return from main would be an idea, but it would be even more proper to explicitly name the return point independently from the function, as this design also scales to label for loops break/continue etc.).
(This is all completely orthogonal to the implementation considerations, and the design considerations of whether adding control effects is a good idea for your language.)
Finally, a bit of theory. There are theoretical programming languages out there with a notion of “co-variable” (the dual of a variable) that represent the return points of a program. They are often called "abstract machine calculi"¹, and are studied for two different reasons: they allow to understand fundamental things about programming languages (for example how to combine call-by-value and call-by-name evaluation order in a type-directed way), and they allow to give a beautiful computational meaning to classical logic (excluded-middle, or proof by contradictions, are non-local control operators); pretty cool.
In those theoretical languages, it is natural for functions to declare not only variable for their formal argument(s), but also one co-variable for its return point. For example¹ in System L, the natural notation for anonymous function (usually (λx.t) in lambda-calculus) is (μ(x·α).c), where α is a co-variable denoting the return point of the function. Now, it is known that while this syntax can express all of classical logic (control operators), it is possible to restrict it to recover intuitionistic logic (pure functional programming), by imposing that co-variables be used linearily (consumed exactly once, as a linear resource).
You can restrict your type-system to check this linear restriction on co-variables, but it is also possible to express this purely syntactically, by imposing that there is a single co-variable, traditionally written ★ (star), that occurs in the program. each binding occurrence of ★ shadows all previous occurrences, making non-local return syntactically inexpressible. This explains why the λ-calculus does not need to talk about co-variables explicitly: you can always implicitly assume that all co-variables are ★.
Introducing a control-flow-break return in this model is a reasonable extension: it implicitly refers to the ambiant co-variable ★, and there is only one. (break and continue muddy the picture a bit as you would distinguish function co-variables and loop co-variables.) But as soon as you want something more expressive, to be able to return to “other functions than the current one”, you should absolutely resort to explicitly naming your co-variables again.
¹: some (theoretical) bibliographic references would be Polarised Intermediate Representation of Lambda Calculus with Sums, Guillaume Munch-Maccagnoni and Gabriel Scherer, 2015, A dissection of L, Arnaud Spiwack, 2016, and all of Paul Downen’s recent works with Zena Ariola and co-authors.
This does sound very theoretical but it coincides with actual language designs that get this right: in abstract machines, co-terms correspond to stacks and continuations, and co-variables thus correspond to continuation variables in the Scheme community. While call/cc's continuations are in general more powerful/expressive (and dangerous) than mere return points (they can escape and be duplicated), Racket for example has a call/ec construction for “escape continuations” that correspond to return points, and a let/ec construction that precisely lets you give a name to the current return point.
