Hacker News Reader

> 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 ().

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.

> "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>.

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).

> For any expression NOT involving "return", I can write, for example:

> const Z = <expr>

> but I cannot if <expr> contains a return embedded somewhere.*

Sure, but that's not special about this case at all. I also can't write 'break' or 'continue' when I'm not inside a loop. When declaring a 'const', I am lexically not inside a function body, so I can't use 'return', which makes sense (the compiler will even tell you, "return statement outside of function body").

Particular statements being allowed in some contexts but not in others is entirely normal.

> My point is that none of this is necessary at all

Maybe it's not necessary, but I like the consistency this provides ("everything has a type"), and I imagine the implementation of the type checker/inferer is more straightforward this way.

Sure, you could define the language such that "a 'return' in a position that expects a typed expression will not affect other type that need to match with it" (or something else, in better, formal language). Or you can just define those statements to have the 'never' type, and not worry about it.

But ok, let's agree that it's not necessary. Then we're just talking about personal preferences, so there's no right or wrong here, and there's no point in arguing.

You can write it just fine if `const Z` is itself nested inside a function definition.

And this isn't really any different from variable references, if you think about it. If you have an expression (x + 1), you can only use it somewhere where there's an `x` in scope. Similarly, you can only use `return` somewhere where there's a function to return from in scope. Indeed, you could even make this explicit when designing the language! A function definition already introduces implicit let-definitions for all arguments in the body. Imagine if we redefined it such that it also introduces "return" as a local, i.e. given:

   fn foo(x: i32, y: i32) -> i32 {
     ...
   }

the body of the function is written as if it had these lines prepended:

   let x = ...;
   let y = ...;
   let return = ...;
   ...

where "return" is a function that does the same thing as the statement. And similarly for break/continue and loops.

The thing that actually makes these different from real variables is that they cannot be passed around as first-class values (e.g. having the function pass its "return" to another function that it calls). Although this could in fact be done, and with Rust lifetime annotations it would even be statically verifiable.

> You can write it just fine if `const Z` is itself nested inside a function definition.

You can't, actually: 'const' is special in that it's not considered by the compiler to be inside a function definition, even if it is (and the compiler will tell you, "return statement outside of function body").

But that doesn't invalidate your point; in a way it supports it: 'return' can only be used in function contexts, just like 'continue' or 'break' can only be used in loop contexts.

You can do this:

   const ONE: i32 = { const fn foolish() -> i32 { return 1 } foolish() };

But yes, your larger point is exactly correct, the constant, even if it happens to be defined inside a function body, is not itself inside a function body and so we obviously can't return from it. It is also not inside an expression we can break out of (Rust allows you to break out of any expression, not just loops). It's a constant, like 5 is a constant, or 'Z' is a constant - this is not C or C++ where "const" means "actually a variable".

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.

The same is true if `return` is a statement, so this doesn't seem to have anything to do with `return` being an expression.

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).

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.

Well now we’re just talking about personal preferences, then.