4 ms·

The issue with `return expr` not having a type is that you lose the ability to write something like let y = match option { Some(x) => x, None => return

The issue with `return expr` not having a type is that you lose the ability to write something like let y = match option { Some(x) => x, None => return Err("whoops!"), }; Without a type, the None branch loses the ability to unify with the Some branch. Now you could say that Rust should just only require branches’ types to unify when all of them have a type, but the ! never type accomplishes that goal just fine.

derriz 1y ago
I'm responding here because so many replies are making the same point. In your particular example, let's put your example into a context. Is fn foo(option: Option<i32>) -> i32 { let y = match option { Some(x) => x, None => return Err("whoops!"), }; return 1; } well typed? It should be if we are to believe that "return <expr>" is an expression of type () - but, naturally, it causes a compilation error because the compiler specifically treats "return <expr>" unlike other expressions. So there is no improvement in regularity, while it admits all sorts of incomprehensible "puzzlers". I don't see why you'd lose this ability if you removed the claim that "return <expr>" is itself an expression. Most/many languages have mechanisms to allow expressions to affect flow control - e.g. with exceptions, yield, etc. - which do not these constructs (for example "throw x") to have a type. Rust could just as easily supported the syntax you use above without making "return <expr>" a tapeable expression.
- steveklabnik 1y ago
  > Is ... well typed? It's not, but not due to the return, it's because you're trying to return a Result from a function that returns an i32. This works: fn foo(option: Option<i32>) -> Result<i32, &'static str> { let y = match option { Some(x) => x, None => return Err("whoops!"), }; return Ok(1); } > It should be if we are to believe that "return <expr>" is an expression of type () It is not, it is an expression of type !. This type unifies with every other type, so the overall type of y is i32. return is not treated in a special way. > if you removed the claim that "return <expr>" is itself an expression This code would no longer work, because blocks that end in an expression evaluate to (), and so you would get the divergent, not well typed error, because one arm is i32 and the other is ().
  - derriz 1y ago
    Sorry for the confusion - I meant to use ! and not (). "It's not, but not due to the return, it's because you're trying to return a Result from a function that returns an i32." That's exactly my point. "return <expr>" is not just an expression which can be typed. If you tell me the types of all the identifiers used, I can look at any expression in Rust which does not include a return, and tell you if it's well typed or not. If the expression includes a return, then I cannot tell you whether the expression is well-formed.
    - steveklabnik 1y ago
      > "return <expr>" is not just an expression which can be typed. Yes, it is, and it can. It has the type !, no matter the type of <expr>.
      - derriz 1y ago
        It only has type !, if the return type of the lexically enclosing function declaration has the same type as that of <expr>, otherwise it's illformed. For any expression NOT involving "return", I can write, for example: const Z = <expr> but I cannot if <expr> contains a return embedded somewhere. The existence of a "return" somewhere in an expression changes the character of the entire expression. I.e. there are two classes of "expressions". Those NOT containing returns (which are equivalent to the notion of "expression" in the languages that Rust was inspired by) and those containing a return somewhere in them which are subject to further rules about wellformedness. My point is that none of this is necessary at all - you don't need to provide type rules for every lexical feature of your language to have a language with a powerful expressive type system (like Rust's).
        steveklabnik 1y ago
        Okay, I think we are indeed talking past each other and I see what you are saying here. I am not sure that I agree, exactly, but I appreciate your point. I'm going to have to think about it a bit more.
        1y ago
- efnx 1y ago
  Well now we’re just talking about personal preferences, then.
- bobbylarrybobby 1y ago
  The type of return is !, not (). Meaning there are zero instances of this type (whereas there is one instance of ()). ! can coerce to any type. Also, the type of return is a separate matter from the type of the thing being returned. You obviously can't return Result from a function returning i32. The point of type coercion is that you can yield `return Err(...)` in one branch of a match and have it type check with the other branch(es).
- rtpg 1y ago
  When discussing well typed-ness, and with more complex languages where you have weird undecideable components, you can end up with a notion of "Well typed" as follows: e: T is well typed _if_ the end result of e would be of type T (end result being hand-wave-y) It's not a guarantee that e is a value of a certain type, but a guarantee that if e is a value in the first place, then it will be a certain type. You sidestep having to prove the halting nature of e. This leaves a nice spot for computation that doesn't complete! let y = return 1 f(y) y could be any type, and it's well typed, because you're never in a secnario where f(y) will be provided a value of the wrong type. Well-typed-ness, by my understanding in more complex type system, is not a guarantee of control flow, but a guarantee that _if_ we evaluate some expression, then it will be fine. And so... you can put `!` as a type in your system, treat return as an expression, and have a simpler semantic model, without really losing anything. Less moving parts, etc.... that's my read of it anyways.

derriz 1y ago

I'm responding here because so many replies are making the same point. In your particular example, let's put your example into a context. Is fn foo(option: Option<i32>) -> i32 { let y = match option { Some(x) => x, None => return Err("whoops!"), }; return 1; } well typed? It should be if we are to believe that "return <expr>" is an expression of type () - but, naturally, it causes a compilation error because the compiler specifically treats "return <expr>" unlike other expressions. So there is no improvement in regularity, while it admits all sorts of incomprehensible "puzzlers". I don't see why you'd lose this ability if you removed the claim that "return <expr>" is itself an expression. Most/many languages have mechanisms to allow expressions to affect flow control - e.g. with exceptions, yield, etc. - which do not these constructs (for example "throw x") to have a type. Rust could just as easily supported the syntax you use above without making "return <expr>" a tapeable expression.

steveklabnik 1y ago
> Is ... well typed? It's not, but not due to the return, it's because you're trying to return a Result from a function that returns an i32. This works: fn foo(option: Option<i32>) -> Result<i32, &'static str> { let y = match option { Some(x) => x, None => return Err("whoops!"), }; return Ok(1); } > It should be if we are to believe that "return <expr>" is an expression of type () It is not, it is an expression of type !. This type unifies with every other type, so the overall type of y is i32. return is not treated in a special way. > if you removed the claim that "return <expr>" is itself an expression This code would no longer work, because blocks that end in an expression evaluate to (), and so you would get the divergent, not well typed error, because one arm is i32 and the other is ().
- derriz 1y ago
  Sorry for the confusion - I meant to use ! and not (). "It's not, but not due to the return, it's because you're trying to return a Result from a function that returns an i32." That's exactly my point. "return <expr>" is not just an expression which can be typed. If you tell me the types of all the identifiers used, I can look at any expression in Rust which does not include a return, and tell you if it's well typed or not. If the expression includes a return, then I cannot tell you whether the expression is well-formed.
  - steveklabnik 1y ago
    > "return <expr>" is not just an expression which can be typed. Yes, it is, and it can. It has the type !, no matter the type of <expr>.
    - derriz 1y ago
      It only has type !, if the return type of the lexically enclosing function declaration has the same type as that of <expr>, otherwise it's illformed. For any expression NOT involving "return", I can write, for example: const Z = <expr> but I cannot if <expr> contains a return embedded somewhere. The existence of a "return" somewhere in an expression changes the character of the entire expression. I.e. there are two classes of "expressions". Those NOT containing returns (which are equivalent to the notion of "expression" in the languages that Rust was inspired by) and those containing a return somewhere in them which are subject to further rules about wellformedness. My point is that none of this is necessary at all - you don't need to provide type rules for every lexical feature of your language to have a language with a powerful expressive type system (like Rust's).
      - steveklabnik 1y ago
        Okay, I think we are indeed talking past each other and I see what you are saying here. I am not sure that I agree, exactly, but I appreciate your point. I'm going to have to think about it a bit more.
      - 1y ago
efnx 1y ago
Well now we’re just talking about personal preferences, then.
bobbylarrybobby 1y ago
The type of return is !, not (). Meaning there are zero instances of this type (whereas there is one instance of ()). ! can coerce to any type. Also, the type of return is a separate matter from the type of the thing being returned. You obviously can't return Result from a function returning i32. The point of type coercion is that you can yield `return Err(...)` in one branch of a match and have it type check with the other branch(es).
rtpg 1y ago
When discussing well typed-ness, and with more complex languages where you have weird undecideable components, you can end up with a notion of "Well typed" as follows: e: T is well typed _if_ the end result of e would be of type T (end result being hand-wave-y) It's not a guarantee that e is a value of a certain type, but a guarantee that if e is a value in the first place, then it will be a certain type. You sidestep having to prove the halting nature of e. This leaves a nice spot for computation that doesn't complete! let y = return 1 f(y) y could be any type, and it's well typed, because you're never in a secnario where f(y) will be provided a value of the wrong type. Well-typed-ness, by my understanding in more complex type system, is not a guarantee of control flow, but a guarantee that _if_ we evaluate some expression, then it will be fine. And so... you can put `!` as a type in your system, treat return as an expression, and have a simpler semantic model, without really losing anything. Less moving parts, etc.... that's my read of it anyways.