-
Notifications
You must be signed in to change notification settings - Fork 563
Add a chapter on divergence #2067
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Changes from 3 commits
84a8e30
2403b18
a9d8264
966e4b3
31f840e
375350a
f9cf9f5
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change | ||||
|---|---|---|---|---|---|---|
| @@ -0,0 +1,37 @@ | ||||||
| r[divergence] | ||||||
| # Divergence | ||||||
|
|
||||||
| r[divergence.intro] | ||||||
| Divergence is the state where a particular section of code could never be encountered at runtime. Importantly, while there are certain language constructs that immediately produce a _diverging expression_ of the type [`!`](./types/never.md), divergence can also propogate to the surrounding block. | ||||||
|
|
||||||
| Any expression of type [`!`](./types/never.md) is a _diverging expression_, but there are also diverging expressions which are not of type `!` (e.g. `Some(panic!())`). | ||||||
|
||||||
| Any expression of type [`!`](./types/never.md) is a _diverging expression_, but there are also diverging expressions which are not of type `!` (e.g. `Some(panic!())`). | |
| Any expression of type [`!`](./types/never.md) is a _diverging expression_, but there are also diverging expressions which are not of type `!` (e.g. `Some(panic!())` with type `Option<!>`). |
also: should this set of expressions be enumerated?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I got confused at first by the second half of this sentence. Can you expand on the
e.g.by specifying the expressions type? I'm assuming it isOption<!>
Suggested change
Any expression of type!is a diverging expression, but there are also diverging expressions which are not of type!(e.g.Some(panic!())).
Any expression of type!is a diverging expression, but there are also diverging expressions which are not of type!(e.g.Some(panic!())with typeOption<!>).
I can expand on this, but I think this exact suggestion is not actually correct; Some(panic!()) will only end up with a type of Option<!> if the inner variable is unconstrained.
also: should this set of expressions be enumerated?
See #2067 (comment). I had this before but TC suggested to remove it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I got confused at first by the second half of this sentence. Can you expand on the
e.g.by specifying the expressions type? I'm assuming it isOption<!>
Suggested change
Any expression of type!is a diverging expression, but there are also diverging expressions which are not of type!(e.g.Some(panic!())).
Any expression of type!is a diverging expression, but there are also diverging expressions which are not of type!(e.g.Some(panic!())with typeOption<!>).I can expand on this, but I think this exact suggestion is not actually correct;
Some(panic!())will only end up with a type ofOption<!>if the inner variable is unconstrained.
Actually, I think this is right/fine (and I'm going to change it to Some(loop {}). It does produce a type of Option<!>, but there is also never-to-any coercions that are talked about elsewhere.
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It feels that we might need to say more here to guard against too simple a reading. We say, 1) not all diverging expressions have type ! (e.g. Some(panic!())), and 2) if a type to be inferred is only unified with diverging expressions, then the type will be inferred to be !.
However, of course, this does not compile:
trait Tr: Sized {
fn m() -> Self { loop {} }
}
impl<T> Tr for T {}
fn f() -> u8 { 0 }
fn g() -> ! {
match f() {
0 => Tr::m(),
// ^^^^^^^ There's a type to be inferred here.
_ => Some(panic!()),
// ^^^^^^^^^^^^^^ This is a diverging expression.
} // ERROR: Mismatched types.
}What might we be able to say to tease this apart?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
is this addressed by the bit about type unification happening structurally below at https://github.com/rust-lang/reference/pull/2067/files#diff-11f5e85172f632195dd6a9a80daa852911fd3d66e788177a3bb39f6c5d7f21cfR27 ?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's a good observation. I've tried to be a little nuanced in my wording - for example, in the list of expression that I removed from your review, I had the wording "the following language constructs unconditonally produce a diverging expression of the type !". There also still is the wording "Any expression of type ! is a diverging expression, but there are also diverging expressions which are not of type !"
| Original file line number | Diff line number | Diff line change | ||||
|---|---|---|---|---|---|---|
|
|
@@ -44,7 +44,7 @@ r[expr.block.result] | |||||
| Then the final operand is executed, if given. | ||||||
|
|
||||||
| r[expr.block.type] | ||||||
| The type of a block is the type of the final operand, or `()` if the final operand is omitted. | ||||||
| Except in the case of divergence (see below), the type of a block is the type of the final operand, or `()` if the final operand is omitted. | ||||||
|
||||||
| Except in the case of divergence (see below), the type of a block is the type of the final operand, or `()` if the final operand is omitted. | |
| Except in the case of divergence [(see below)](block-expr.md#r-expr.block.type.diverging), the type of a block is the type of the final operand, or `()` if the final operand is omitted. |
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
place expression could also use a link: expressions.html#r-expr.place-value.place-memory-location
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You and I had talked about this. We had both thought, "maybe it's worth using the nightly never type to express this more clearly." I had mentioned I'd need to talk it over with @ehuss. In that discussion, @ehuss made a good point: why not just use functions? I.e., for the expression whose type we want to demonstrate, we can make that the trailing expression of a function that returns !. E.g.:
fn no_control_flow() -> ! {
loop {}
}That does seem likely the best approach. Sound right to you?
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This compiles and produces an infinite loop.
But then, so does:
let foo = Foo { x: make() };
let diverging_place_not_read: () = {
let _: () = {
// Asssignment to something other than `_` means?
let _x = foo.x;
};
};Is there a way to demonstrate this such that let _ = .. produces distinct compile-time or runtime behavior from let _x = ..?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
To answer the question posed, this compiles:
trait RetId { type Ty; }
impl<T> RetId for fn() -> T { type Ty = T; }
struct S<T> {
x: T,
}
fn f(x: S<<fn() -> ! as RetId>::Ty>) -> ! {
let _x = x.x; // OK.
}But this does not:
fn f(x: S<<fn() -> ! as RetId>::Ty>) -> ! {
let _ = x.x; // ERROR: Mismatched types.
}This is one, though, where it's not immediately coming to mind how to express this without either the never type or the never type hack.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here's one way. (Of course, this is really just another instantiation of the never type hack.)
fn phantom_call<T>(_: impl FnOnce(T) -> T) {}
let _ = phantom_call(|x| -> ! {
let _x = x; // OK.
});
let _ = phantom_call(|x| -> ! {
let _ = x; // ERROR: Mismatched types.
});There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's interesting how it really does need the ! type to be ascribed for this to work. I.e., it doesn't work with:
struct W<T>(T);
let x = W(loop {});
let _ = || -> ! {
let _x = x.0; // ERROR.
};Any thoughts about the reason for that?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's interesting how it really does need the
!type to be ascribed for this to work. I.e., it doesn't work with:struct W<T>(T); let x = W(loop {}); let _ = || -> ! { let _x = x.0; // ERROR. };Any thoughts about the reason for that?
This one nearly stumped me, because I had my mind set that this was a closure thing. But then I realized, this also fails:
let _: ! = {
let _x = x.0;
};The important bit to remember here is that x.0 is an inference var which does not produce divergence (only place expressions that produce types of ! do). The "expectation" value of the block (either as the block's type, or the closure's return value) does not constrain that inference variable.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Makes sense, thanks. (And yes, the only purpose of the closure in the examples is to be able to ascribe the type without nightly features.)
Coincidentally, prompted by lcnr apropos of lcnr's work, I was just looking at something else today with a similar flavor:
trait Tr: Sized {
fn abs(self) -> i32 { 0 }
}
impl Tr for i32 {}
fn main() {
let x = -42;
let y: i32 = x.abs();
assert!(y != x.abs()); // Surprising, but true.
}
traviscross marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -96,6 +96,27 @@ Every binding in each `|` separated pattern must appear in all of the patterns i | |
| r[expr.match.binding-restriction] | ||
| Every binding of the same name must have the same type, and have the same binding mode. | ||
|
|
||
| r[expr.match.type] | ||
| The type of the overall `match` expression is the [least upper bound](../type-coercions.md#r-coerce.least-upper-bound) of the individual match arms. | ||
|
Comment on lines
+99
to
+100
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. If we're inlining the rule about determining the type based on the LUB for match, from https://doc.rust-lang.org/1.90.0/reference/type-coercions.html#r-coerce.least-upper-bound.intro, probably we'd need to do that for the other rules there also (and then either remove the list from there or convert it to an admonition or index).
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. As an aside, looking into this rule is what prompted me to file: |
||
|
|
||
| r[expr.match.empty] | ||
| If there are no match arms, then the `match` expression is diverging and the type is [`!`](../types/never.md). | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. does this require a diverging scrutinee expression to compile? probably worth adding an example either way
Member
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is a good question! The answer is (subtly) no. Take the following: fn make<T>() -> T { loop {} }
enum Empty {}
fn diverging_match_no_arms() -> ! {
let e: Empty = make();
match e {}
}
Adding this as an example. |
||
|
|
||
| r[expr.match.conditional] | ||
| If either the scrutinee expression or all of the match arms diverge, then the entire `match` expression also diverges. | ||
|
|
||
| > [!NOTE] | ||
| > Even if the entire `match` expression diverges, its type may not be [`!`](../types/never.md). | ||
| > | ||
| >```rust,compile_fail,E0004 | ||
| > let a = match true { | ||
| > true => Some(panic!()), | ||
| > false => None, | ||
| > }; | ||
| > // Fails to compile because `a` has the type `Option<!>`. | ||
| > match a {} | ||
| >``` | ||
|
|
||
| r[expr.match.guard] | ||
| ## Match guards | ||
|
|
||
|
|
||
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We try to keep the number of top-level chapters contained. Looking at it, perhaps most of what's here that can't be inlined on the pages for each expression would make sense appearing in the Expressions chapter (e.g., we talk about place and value expressions there -- the verbiage about when a place expression is diverging might make sense near that) and in the Never type chapter.