-
Notifications
You must be signed in to change notification settings - Fork 1.5k
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
Conditional expressions #911
Merged
zygoloid
merged 22 commits into
carbon-language:trunk
from
zygoloid:proposal-conditional-expressi
Jan 29, 2022
Merged
Changes from all commits
Commits
Show all changes
22 commits
Select commit
Hold shift + click to select a range
a4a52e2
Filling out template with PR 911
zygoloid 852124d
First draft of design.
zygoloid 820c706
Add proposal doc and respond to review comments.
zygoloid 4f4af07
Add 'then' to the keyword list.
zygoloid 933c0bc
Address review comments.
zygoloid 16a99c9
Apply suggestions from code review
zygoloid b4ed0bc
Avoid circular `impl` definition and updates based on discussion with
zygoloid e5bcfb5
Fix ImplicitAs requirement in CommonTypeWith.
zygoloid e0c36f3
Fix another instance of wrong constraints.
zygoloid 2611c92
Update to match latest generics ideas and respond to review comments.
zygoloid 9dc578d
Fix generics syntax.
zygoloid 0a34733
Add Future Work section describing known issues with this proposal's use
zygoloid 7374061
Fix bug in example code.
zygoloid 93c728a
Use a precedence-based model to determine where `if` expressions can
zygoloid e823dc5
More explicitly describe where an `if` expression can appear.
zygoloid 9e2984e
Address review comments.
zygoloid 34ae0f1
Remove special case for lvalue conditional.
zygoloid ed6131a
Address review comments.
zygoloid ab2f418
Apply suggestions from code review
zygoloid a46e1cc
Remove outdated note that is not true of the current design.
zygoloid c611847
Merge branch 'trunk' into proposal-conditional-expressi
zygoloid a99e007
Pre-commit fixes.
zygoloid File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,243 @@ | ||
# `if` expressions | ||
|
||
<!-- | ||
Part of the Carbon Language project, under the Apache License v2.0 with LLVM | ||
Exceptions. See /LICENSE for license information. | ||
SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception | ||
--> | ||
|
||
<!-- toc --> | ||
|
||
## Table of contents | ||
|
||
- [Overview](#overview) | ||
- [Syntax](#syntax) | ||
- [Semantics](#semantics) | ||
- [Finding a common type](#finding-a-common-type) | ||
- [Symmetry](#symmetry) | ||
- [Same type](#same-type) | ||
- [Implicit conversions](#implicit-conversions) | ||
- [Alternatives considered](#alternatives-considered) | ||
- [References](#references) | ||
|
||
<!-- tocstop --> | ||
|
||
## Overview | ||
|
||
An `if` expression is an expression of the form: | ||
|
||
> `if` _condition_ `then` _value1_ `else` _value2_ | ||
|
||
The _condition_ is converted to a `bool` value in the same way as the condition | ||
of an `if` statement. | ||
|
||
> **Note:** These conversions have not yet been decided. | ||
|
||
The _value1_ and _value2_ are implicitly converted to their | ||
[common type](#finding-a-common-type), which is the type of the `if` expression. | ||
|
||
## Syntax | ||
|
||
`if` expressions have very low precedence, and cannot appear as the operand of | ||
any operator, except as the right-hand operand in an assignment. They can appear | ||
in other context where an expression is permitted, such as within parentheses, | ||
as the operand of a `return` statement, as an initializer, or in a | ||
comma-separated list such as a function call. | ||
|
||
The _value1_ and _value2_ expressions are arbitrary expressions, and can | ||
themselves be `if` expressions. _value2_ extends as far to the right as | ||
possible. An `if` expression can be parenthesized if the intent is for _value2_ | ||
to end earlier. | ||
|
||
``` | ||
// OK, same as `if cond then (1 + 1) else (2 + (4 * 6))` | ||
var a: i32 = if cond then 1 + 1 else 2 + 4 * 6; | ||
|
||
// OK | ||
var b: i32 = (if cond then 1 + 1 else 2) + 4 * 6; | ||
``` | ||
|
||
An `if` keyword at the start of a statement is always interpreted as an | ||
[`if` statement](/docs/design/control_flow/conditionals.md), never as an `if` | ||
expression, even if it is followed eventually by a `then` keyword. | ||
|
||
## Semantics | ||
|
||
The converted _condition_ is evaluated. If it evaluates to `true`, then the | ||
converted _value1_ is evaluated and its value is the result of the expression. | ||
Otherwise, the converted _value2_ is evaluated and its value is the result of | ||
the expression. | ||
|
||
## Finding a common type | ||
jonmeow marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
The common type of two types `T` and `U` is `(T as CommonType(U)).Result`, where | ||
`CommonType` is the `Carbon.CommonType` constraint. `CommonType` is notionally | ||
defined as follows: | ||
|
||
``` | ||
constraint CommonType(U:! CommonTypeWith(Self)) { | ||
extend CommonTypeWith(U) where .Result == U.Result; | ||
} | ||
``` | ||
|
||
The actual definition is a bit more complex than this, as described in | ||
[symmetry](#symmetry). | ||
|
||
The interface `CommonTypeWith` is used to customize the behavior of | ||
`CommonType`: | ||
|
||
``` | ||
interface CommonTypeWith(U:! Type) { | ||
let Result:! Type | ||
where Self is ImplicitAs(.Self) and | ||
U is ImplicitAs(.Self); | ||
} | ||
``` | ||
|
||
The implementation `A as CommonTypeWith(B)` specifies the type that `A` would | ||
like to result from unifying `A` and `B` as its `Result`. | ||
|
||
geoffromer marked this conversation as resolved.
Show resolved
Hide resolved
|
||
_Note:_ It is required that both types implicitly convert to the common type. | ||
Some blanket `impl`s for `CommonTypeWith` are provided as part of the prelude. | ||
These are described in the following sections. | ||
|
||
_Note:_ The same mechanism is expected to eventually be used to compute common | ||
types in other circumstances. | ||
|
||
### Symmetry | ||
|
||
The common type of `T` and `U` should always be the same as the common type of | ||
`U` and `T`. This is enforced in two steps: | ||
|
||
- A `SymmetricCommonTypeWith` interface implicitly provides a | ||
`B as CommonTypeWith(A)` implementation whenever one doesn't exist but an | ||
`A as CommonTypeWith(B)` implementation exists. | ||
- `CommonType` is defined in terms of `SymmetricCommonTypeWith`, and requires | ||
that both `A as SymmetricCommonTypeWith(B)` and | ||
`B as SymmetricCommonTypeWith(A)` produce the same type. | ||
|
||
The interface `SymmetricCommonTypeWith` is an implementation detail of the | ||
`CommonType` constraint. It is defined and implemented as follows: | ||
|
||
``` | ||
interface SymmetricCommonTypeWith(U:! Type) { | ||
let Result:! Type | ||
where Self is ImplicitAs(.Self) and | ||
U is ImplicitAs(.Self); | ||
} | ||
match_first { | ||
impl [T:! Type, U:! CommonTypeWith(T)] T as SymmetricCommonTypeWith(U) { | ||
let Result:! Type = U.Result; | ||
} | ||
impl [U:! Type, T:! CommonTypeWith(U)] T as SymmetricCommonTypeWith(U) { | ||
let Result:! Type = T.Result; | ||
} | ||
} | ||
``` | ||
josh11b marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
The `SymmetricCommonTypeWith` interface is not exported, so user-defined `impl`s | ||
can't be defined, and only the two blanket `impl`s above are used. The | ||
`CommonType` constraint is then defined as follows: | ||
|
||
``` | ||
constraint CommonType(U:! SymmetricCommonTypeWith(Self)) { | ||
extend SymmetricCommonTypeWith(U) where .Result == U.Result; | ||
} | ||
``` | ||
|
||
When computing the common type of `T` and `U`, if only one of the types provides | ||
a `CommonTypeWith` implementation, that determines the common type. If both | ||
types provide a `CommonTypeWith` implementation and their `Result` types are the | ||
same, that determines the common type. Otherwise, if both types provide | ||
implementations but their `Result` types differ, there is no common type, and | ||
the `CommonType` constraint is not met. For example, given: | ||
|
||
``` | ||
// Implementation #1 | ||
impl [T:! Type] MyX as CommonTypeWith(T) { | ||
let Result:! Type = MyX; | ||
} | ||
|
||
// Implementation #2 | ||
impl [T:! Type] MyY as CommonTypeWith(T) { | ||
let Result:! Type = MyY; | ||
} | ||
``` | ||
|
||
`MyX as CommonTypeWith(MyY)` will select #1, and `MyY as CommonTypeWith(MyX)` | ||
will select #2, but the constraints on `MyX as CommonType(MyY)` will not be met | ||
because result types differ. | ||
|
||
### Same type | ||
|
||
If `T` is the same type as `U`, the result is that type: | ||
|
||
``` | ||
final impl [T:! Type] T as CommonTypeWith(T) { | ||
let Result:! Type = T; | ||
zygoloid marked this conversation as resolved.
Show resolved
Hide resolved
|
||
} | ||
``` | ||
|
||
_Note:_ This rule is intended to be considered more specialized than the other | ||
rules in this document. | ||
|
||
Because this `impl` is declared `final`, `T.(CommonType(T)).Result` is always | ||
assumed to be `T`, even in contexts where `T` involves a generic parameter and | ||
so the result would normally be an unknown type whose type-of-type is `Type`. | ||
|
||
``` | ||
fn F[T:! Hashable](c: bool, x: T, y: T) -> HashCode { | ||
// OK, type of `if` expression is `T`. | ||
return (if c then x else y).Hash(); | ||
} | ||
``` | ||
|
||
### Implicit conversions | ||
|
||
If `T` implicitly converts to `U`, the common type is `U`: | ||
|
||
``` | ||
impl [T:! Type, U:! ImplicitAs(T)] T as CommonTypeWith(U) { | ||
let Result:! Type = T; | ||
} | ||
``` | ||
|
||
_Note:_ If an implicit conversion is possible in both directions, and no more | ||
specific implementation exists, the constraints on `T as CommonType(U)` will not | ||
be met because `(T as CommonTypeWith(U)).Result` and | ||
`(U as CommonTypeWith(T)).Result` will differ. In order to define a common type | ||
for such a case, `CommonTypeWith` implementations in both directions must be | ||
provided to override the blanket `impl`s in both directions: | ||
|
||
``` | ||
impl MyString as CommonTypeWith(YourString) { | ||
let Result:! Type = MyString; | ||
} | ||
impl YourString as CommonTypeWith(MyString) { | ||
let Result:! Type = MyString; | ||
} | ||
josh11b marked this conversation as resolved.
Show resolved
Hide resolved
|
||
var my_string: MyString; | ||
var your_string: YourString; | ||
// The type of `also_my_string` is `MyString`. | ||
var also_my_string: auto = if cond then my_string else your_string; | ||
``` | ||
|
||
## Alternatives considered | ||
josh11b marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
- [Provide no conditional expression](/proposals/p0911.md#no-conditional-expression) | ||
- Use | ||
[`cond ? expr1 : expr2`, like in C and C++](/proposals/p0911.md#use-c-syntax) | ||
syntax | ||
- Use [`if (cond) expr1 else expr2`](/proposals/p0911.md#no-then) syntax | ||
- Use | ||
[`if (cond) then expr1 else expr2`](/proposals/p0911.md#require-parentheses-around-the-condition) | ||
syntax | ||
- Allow | ||
[`1 + if cond then expr1 else expr2`](/proposals/p0911.md#never-require-enclosing-parentheses) | ||
- [Only require one `impl` to specify the common type if implicit conversions in both directions are possible](/proposals/p0911.md#implicit-conversions-in-both-directions) | ||
- [Introduce special rules for lvalue conditionals](/proposals/p0911.md#support-lvalue-conditionals) | ||
|
||
## References | ||
|
||
- Proposal | ||
[#911: Conditional expressions](https:/carbon-language/carbon-lang/pull/911). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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 find the phrasing "[t]he converted expression is evaluated" a bit awkward or confusing... The conversion happens after the evaluation?
Maybe phrase this as
_condition_ is evaluated and then implicitly converted to bool.
... Dunno, its awkward. But I think it would be good to make it unambiguous that the conversion happens after evaluation.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 think this is a distinction between operationally thinking of conversion as something you do to a value, and denotationally thinking of it as something you do to an expression. In the language of https:/carbon-language/carbon-lang/tree/trunk/docs/design/expressions#conversions-and-casts, we take the latter view: implicit conversion is a process applied to an expression of one type to produce an expression of another type, as part of type-checking. As such, it happens before any evaluation is considered: first we transform
cond
intocond.(ImplicitAs(bool).Convert)()
as part of type-checking, to form the converted condition expression, and then later whenever we evaluate theif
expresssion, we evaluate that converted condition expression. (And similarly for thevalue1
andvalue2
: type-checking converts those, and during evaluation we evaluate the converted version of whichever expression we select.)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 think my challenge as a reader is that the phrase "a converted X is evaluated ..." is very ambiguous between "an X of the 'converted' kind is evaluated" and "after converting X, it is evaluated". They both seem quite plausible interpretations, and there are contexts in which either one would make more sense, and so I often end up confused which one is the one I should be using.
Maybe as a follow-up both here and in the "Conversions and Casts" section the language could switch to some construct that is less ambiguous when read if that makes sense (and such a formulation could be found)?
To be clear, this isn't blocking anything, just a lingering confusion for me as a reader.