-
Notifications
You must be signed in to change notification settings - Fork 564
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 all commits
4cfa363
2f39743
5eef4bc
8b6a6da
d56f184
90ef10f
d582def
eb381b7
e097e7e
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,56 @@ | ||
| r[divergence] | ||
| # Divergence | ||
|
|
||
| r[divergence.intro] | ||
| If an expression diverges, then nothing after that expression will execute. 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 --- where divergence indicates that the block itself will never finish executing. | ||
|
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. Is the following a correct definition of a diverging expression? And then I would expect a rule below to explain which expressions are diverging. That can just be a list linking to the other relevant rules in their respective chapters. However, reading through this, I'm unable to come up a clear definition of what is diverging. Is it possible to come up with a list of what is diverging?
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. That is imo correct, and close to what I originally had before I changed it based on Niko's review. I did originally have a list, which TC asked me to remove: #2067 (comment)
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. (though, that list is not entirely accurate, I've since realized, because a block expression can be diverging but not have a type of |
||
|
|
||
| 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(loop {})` produces a type of `Option<!>`). | ||
|
|
||
| > [!NOTE] | ||
| > Though `!` is considered an uninhabited type, a type being uninhabited is not sufficient for it to diverge. | ||
| > | ||
| > ```rust,compile_fail,E0308 | ||
| > # #![ feature(never_type) ] | ||
| > # fn make<T>() -> T { loop {} } | ||
| > enum Empty {} | ||
| > fn diverging() -> ! { | ||
| > // This has a type of `!`. | ||
| > // So, the entire function is considered diverging | ||
| > make::<!>(); | ||
| > } | ||
| > fn not_diverging() -> ! { | ||
| > // This type is uninhabited. | ||
| > // However, the entire function is not considered diverging | ||
| > make::<Empty>(); | ||
| > } | ||
| > ``` | ||
| r[divergence.fallback] | ||
| ## Fallback | ||
| If a type to be inferred is only unified with diverging expressions, then that type will be inferred to be `!`. | ||
| > [!EXAMPLE] | ||
| > ```rust,compile_fail,E0277 | ||
| > fn foo() -> i32 { 22 } | ||
| > match foo() { | ||
| > // ERROR: The trait bound `!: Default` is not satisfied. | ||
| > 4 => Default::default(), | ||
| > _ => return, | ||
| > }; | ||
| > ``` | ||
| > [!EDITION-2024] | ||
| > Before the 2024 edition, the type was inferred to instead be `()`. | ||
| > [!NOTE] | ||
| > Importantly, type unification may happen *structurally*, so the fallback `!` may be part of a larger type. The > following compiles: | ||
| > ```rust | ||
| > fn foo() -> i32 { 22 } | ||
| > // This has the type `Option<!>`, not `!` | ||
| > match foo() { | ||
| > 4 => Default::default(), | ||
| > _ => Some(return), | ||
| > }; | ||
| > ``` | ||
| <!-- TODO: This last point should likely should be moved to a more general "type inference" section discussing generalization + unification. --> | ||
| 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)](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. | ||||||||||||||||||
|
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. This gives an exception for divergence, but doesn't explicitly say that the type of the block is the never type if the block diverges. I'm wondering if something like the following might clear that up?
Suggested change
I'm guessing this logic comes from somewhere in However, there's some things in there about
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. I like your wording, but yeah, this is a good point about This fails because the type of the block is The type of the block ends up being the LUB of all the break (or return for fns) types, and the final expression (which depends on whether the block is diverging, whether it is |
||||||||||||||||||
|
|
||||||||||||||||||
| ```rust | ||||||||||||||||||
| # fn fn_call() {} | ||||||||||||||||||
|
|
@@ -63,6 +63,51 @@ assert_eq!(5, five); | |||||||||||||||||
| > [!NOTE] | ||||||||||||||||||
| > As a control flow expression, if a block expression is the outer expression of an expression statement, the expected type is `()` unless it is followed immediately by a semicolon. | ||||||||||||||||||
|
|
||||||||||||||||||
| r[expr.block.type.diverging] | ||||||||||||||||||
| A block is itself considered to be [diverging](../divergence.md) if all reachable control flow paths contain a [diverging expression](../divergence.md), unless that expression is a [place expression](../expressions.md#r-expr.place-value.place-memory-location) that is not read from. | ||||||||||||||||||
|
|
||||||||||||||||||
| ```rust,no_run | ||||||||||||||||||
| # #![ feature(never_type) ] | ||||||||||||||||||
| # fn make<T>() -> T { loop {} } | ||||||||||||||||||
| fn no_control_flow() -> ! { | ||||||||||||||||||
| // There are no conditional statements, so this entire function body is diverging. | ||||||||||||||||||
| loop {} | ||||||||||||||||||
| } | ||||||||||||||||||
|
|
||||||||||||||||||
| fn control_flow_diverging() -> ! { | ||||||||||||||||||
| // All paths are diverging, so this entire function body is diverging. | ||||||||||||||||||
| if true { | ||||||||||||||||||
| loop {} | ||||||||||||||||||
| } else { | ||||||||||||||||||
| loop {} | ||||||||||||||||||
| } | ||||||||||||||||||
| } | ||||||||||||||||||
|
|
||||||||||||||||||
| fn control_flow_not_diverging() -> () { | ||||||||||||||||||
| // Some paths are not diverging, so this entire block is not diverging. | ||||||||||||||||||
| if true { | ||||||||||||||||||
| () | ||||||||||||||||||
| } else { | ||||||||||||||||||
| loop {} | ||||||||||||||||||
| } | ||||||||||||||||||
| } | ||||||||||||||||||
|
|
||||||||||||||||||
| struct Foo { | ||||||||||||||||||
| x: !, | ||||||||||||||||||
| } | ||||||||||||||||||
|
Comment on lines
+95
to
+97
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. Can this be rewritten to use an empty enum to avoid the need for nightly features? For example:
Suggested change
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. |
||||||||||||||||||
|
|
||||||||||||||||||
| fn diverging_place_read() -> ! { | ||||||||||||||||||
| let foo = Foo { x: make() }; | ||||||||||||||||||
| // A read of a place expression produces a diverging block | ||||||||||||||||||
| let _x = foo.x; | ||||||||||||||||||
| } | ||||||||||||||||||
| fn diverging_place_not_read() -> () { | ||||||||||||||||||
| let foo = Foo { x: make() }; | ||||||||||||||||||
| // Asssignment to `_` means the place is not read | ||||||||||||||||||
| let _ = foo.x; | ||||||||||||||||||
| } | ||||||||||||||||||
| ``` | ||||||||||||||||||
|
|
||||||||||||||||||
| r[expr.block.value] | ||||||||||||||||||
| Blocks are always [value expressions] and evaluate the last operand in value expression context. | ||||||||||||||||||
|
|
||||||||||||||||||
|
|
||||||||||||||||||
| Original file line number | Diff line number | Diff line change | ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
|
@@ -73,6 +73,31 @@ let y = if 12 * 15 > 150 { | |||||||||||||||
| assert_eq!(y, "Bigger"); | ||||||||||||||||
| ``` | ||||||||||||||||
|
|
||||||||||||||||
| r[expr.if.diverging] | ||||||||||||||||
| An `if` expression diverges if either the condition expression diverges or if all arms diverge. | ||||||||||||||||
|
|
||||||||||||||||
| ```rust,no_run | ||||||||||||||||
| fn diverging_condition() -> ! { | ||||||||||||||||
| // Diverges because the condition expression diverges | ||||||||||||||||
| if loop {} { | ||||||||||||||||
| () | ||||||||||||||||
| } else { | ||||||||||||||||
| () | ||||||||||||||||
| }; | ||||||||||||||||
| // The semicolon above is important: | ||||||||||||||||
| // The type of the `if` statement is `()`, despite being diverging. | ||||||||||||||||
|
Comment on lines
+87
to
+88
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. This is pretty subtle because you need to understand the rules for how an elided final expression works. I'm wondering if a little extra commentary could help here.
Suggested change
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 accurate. |
||||||||||||||||
| } | ||||||||||||||||
| fn diverging_arms() -> ! { | ||||||||||||||||
| // Diverges because all arms diverge | ||||||||||||||||
| if true { | ||||||||||||||||
| loop {} | ||||||||||||||||
| } else { | ||||||||||||||||
| loop {} | ||||||||||||||||
| } | ||||||||||||||||
| } | ||||||||||||||||
| ``` | ||||||||||||||||
|
|
||||||||||||||||
| r[expr.if.let] | ||||||||||||||||
| ## `if let` patterns | ||||||||||||||||
|
|
||||||||||||||||
|
|
||||||||||||||||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -56,7 +56,7 @@ r[items.fn.signature] | |
| Functions may declare a set of *input* [*variables*][variables] as parameters, through which the caller passes arguments into the function, and the *output* [*type*][type] of the value the function will return to its caller on completion. | ||
|
|
||
| r[items.fn.implicit-return] | ||
| If the output type is not explicitly stated, it is the [unit type]. | ||
| If the output type is not explicitly stated, it is the [unit type]. However, if the block expression is not [diverging](../divergence.md), then the output type is instead [`!`](../types/never.md). | ||
|
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. In talking over this PR in the office hours, @ehuss and I puzzled over this rule. Presumably the not is misplaced, but even with that removed, we weren't clear on how to assign meaning to this given, of course: fn f() {
loop {} // Diverging expression.
}
let _ = || -> ! { f() }; //~ ERROR mismatched types
let _: fn() -> ! = f; //~ ERROR mismatched types
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. Ah, this is a good catch. Indeed, the additional language is not correct for the function signature. What I had in mind when writing this was that when type checking the function body the implicit return is I think it was motivated by this example. I guess, maybe there is an equivalent statement missing about the implicit "final type" of a block (which is by default
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. Should this change be reverted, then?
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. Well, probably. But I wonder if there should be some additional text added somewhere that the type of the function block may not actually be the return type of the function, but rather must be coercible into the return type of the function. |
||
|
|
||
| r[items.fn.fn-item-type] | ||
| When referred to, a _function_ yields a first-class *value* of the corresponding zero-sized [*function item type*], which when called evaluates to a direct call to the function. | ||
|
|
||
Uh oh!
There was an error while loading. Please reload this page.