4 ms·
The case at the beginning, where we know our pattern is irrefutable but the compiler doesn't (let (x, 2) = (1, 1+1)) ,is something the compiler could easily pro
by arijun 3y ago
The case at the beginning, where we know our pattern is irrefutable but the compiler doesn't (let (x, 2) = (1, 1+1)) ,is something the compiler could easily prove (as long as the irrefutably could be proven locally as it is here). At first, I struggled to think of why that capability would ever be helpful. In the end, though, I came up with this example, which can (and does) come up:
fn infallible() -> Result<u8, !>{
Ok(1)
}
fn match_infallible(){
let Ok(x) = infallible();
}
The compiler here knows the `infallible` function will always return an `Ok` because of the return type. Here you could just `unwrap` the result, but what if it was inside a tuple, or something similar?
- couchand 3y agoThe latter is shown to be type-based static analysis, even though it "looks like" there's a runtime component: the Never plugs one of only two holes in Result, so it statically becomes equivalent to a newtype. The former can't be restricted to type analysis (without something like dependent types I think?). You're right that we could apply constant folding to check in this case. My understanding is that the Rust design philosophy is to skip things like this because of the potential to produce surprising results upon refactoring.
- arijun 3y agoMy point was that both are static, but you’re right that one being done at the type checking stage probably makes a big difference in the feasibility. > the potential to produce surprising results That’s actually the big reason for that capability. If you do let result: Result<_,!> = … let ok(fine) = result , if result ever changes from infallible to fallible, you get a compile error rather than the runtime error you would get with unwrap. In fact, when looking it up, it turns out that specific case was a big part of the motivation for the “!” type in the first place! I think the above code probably compiles in nightly because of that.