Did I say opposite? How this "influencing control flow" is change the type system?
I've already answered this question: in Rust type ! plays 2 roles now: as !never and as !any , which corresponds to Haskell types Void and a. No more, no less. Any counter-examples?
I already gave one: if cond { 42i32 } else { panic!(); } (notice the ;). The else branch has no last expression in the block, so it would be "returning" (), which is obviously the wrong type. However since the block contains an expression of type ! (the panic!()), the compiler is able to infer that it will never "return" normally, so it doesn't matter that it doesn't have a last expression.
If you're not convinced of the else branch containing only panic!() you can also consider this (note that the ; after println!() is also required!):
if cond {
42i32
} else {
panic!();
println!();
}
(I'll get back to the technical topic in a moment, but first I'd like to say: You asked a question, and I answered it, and now you say you don't care about the answer. That feels rather impolite.)
I'm sorry for my English.
I wanted to say: we do not care about "how", but we care about "what".
For me !.into() == <T>!:: == !any , because it has the same result: the type is fluid.
Nice try! 
Yes, this is also an error, because rust sometimes uses () as synonym to ! (I call it "unit"!). (I do not suggest to change this, but yeah, () is a bit magical too)
but no, you are wrong. Here is a proof:
// ERROR: error[E0308]: `if` and `else` have incompatible types
let x = if true {42i32} else {panic!(); 3i64};
(Thanks for clarifying!)
What we're saying is that ! always means !never. As you say, it sometimes results in something fluid [or, something that looks fluid to the programmer]. But that's just one of the possible uses of !never.
If I'm understanding your terms correctly, here's how you should interpret panic!(): panic!() immediately produces a !never; in-context, you need an !any, so Rust implicitly calls absurd to convert from !never to !any.
Do you see any contradiction?
What do you mean "it is also an error"? Either way, it has been allowed on stable since a long time, so whatever you're proposing must keep that behavior.
I did specify that you cannot have a trailing expression. And I don't see how what proves my example is wrong, you didn't show an equivalent in Haskell, so as far as I can see it does show a behavior that isn't present in Haskell and that your types cannot handle. I'm happy to be proven wrong, but not by changing my example.
Exactly rust do what you've described!
But is any math proof, that doing such transformation everywhere on ! type it is impossible to create invalid calculations?
I gave the example of opposite: nonsense function which compiles now on Rust
fn id_nonsense<T>(x: !) -> T { x }
Yes. You can never have an instance of !, so the conversion is always valid.
I meant a "type error". But yes, it was long ago in stable version, and we must keep this behavior.
When I asked you about counter-example how "control flow" changes type system, I meant specifically how it changes ! never-type. But you showed me example how the "control flow" changes () unit type.
So, yes, good example of () as !any type, and no, ! in your example play role of !any type, not a third one.
Could you clarify exactly what the semantic difference between how "!any" and "!never`" behave? (Not the difference between when you should use one or the other.)
If I've understood correctly, the only difference is that "!any" implicitly converts by-value to any type, but !never doesn't. (Maybe "!any" contributes to static reachability analysis and "!never" doesn't.)
If this is accurate, then what is the benefit of providing both as primitive language types? "!any" must be because of the coercions, but IIUC the whole point of "!never" being separate is that it should behave identically to enum Void {}.
Splitting ! isn't going to assist in (partial) stabilization earlier, because we already did — std::convert::Infallible is a canonical empty enum without any coercions (but with intent stated to unify with ! and provide coercions in the future).
() is never treated as !.
What actually happens is that the type of a block without a trailing expression is usually () but there is an exception to the rule: if one of the block's expression statements is of type ! then the type of the whole block is ! instead.
Rust Reference is inaccurate about this.
This is the exact rule when () is implicitly converted into ! (!any) type
Yes, correct. Maybe !never could be implicitly converted !any
Because exists situations, when is an ambiguity which role to use (mostly in generics)
!never is Void type and is std::convert::Infallible type.
I just clarify in which situation which role is used.
!any for "return"-type( -> !any), and !never for rest of situations (and more complex rules for generics)
Does everyone agree that an empty enum defined as enum Void { } (aka. "!never") should not have the same implicit coercions as ! (aka. "!any"), the return type of diverging functions? You could still match on it with no arms to get ! (and by extension, anything else), but it shouldn't happen implicitly.
Apparently you can already bind values with type ! even on stable, with just a pinch of type aliasing:
trait Ret { type Ret; }
impl<T> Ret for fn() -> T { type Ret = T; }
type Any = <fn() -> ! as Ret>::Ret;
fn foo() -> Result<String, i32> {
let x: Any = todo!();
if x {
Ok(x)
} else {
Err(x)
}
}
It makes sense that the above code wouldn't compile without explicitly asking for x: Any, because type-checking would become less useful on incomplete code such as the above. While let x = todo!() could be any one of bool, String or i32, it's diagnostically useful that it can't be all of them.
I suppose you could define it like that, but it would be pointless.
Instead of one step (a block like this implicitly has type !), you would have two implicit steps (a block like this implicitly generates () which then implicitly gets converted to !), and you would also need to define this () to ! conversion which makes no sense logically. Much easier to skip the () step.
If you think about it, the contradiction is having a value of type !.
Of course it is, the whole point of never is that it never exists. If it existed, it would be unsound. I don't understand why you are so worried about strictly type checking code that never runs. I've played with this in the past before, and any code that follows a never value is usually just a ud2 instruction.
This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.