Skip to content
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

Eliminate the notion of "bound resolution" from inference.md. #4013

Open
wants to merge 2 commits into
base: inference_spec_13
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 1 addition & 22 deletions resources/type-system/inference.md
Original file line number Diff line number Diff line change
Expand Up @@ -969,27 +969,6 @@ with respect to `L` under constraints `C0`
- If for `i` in `0...m`, `Mi` is a subtype match for `Ni` with respect to `L`
under constraints `Ci`.

## Bound resolution

For any type `T`, the _bound resolution_ of `T` is a type `U`, defined by the
following recursive process:

- If `T` is a type variable `X`, then let `B` be the bound of `X`. Then let `U`
be the bound resolution of `B`.

- Otherwise, if `T` is a promoted type variable `X&B`, then let `U` be the bound
resolution of `B`.

- Otherwise, let `U` be `T`.

_The point of bound resolution of `T` is to find a non-type-variable type which
is a (minimal) supertype of `T`._

_Note that the spec notions of __dynamic__ boundedness and __Function__
boundedness can be defined in terms of bound resolution, as follows: a type is
__dynamic__ bounded iff its bound resolution is __dynamic__, and a type is
__Function__ bounded iff its bound resolution is __Function__._

# Expression inference

Expression inference is a recursive process of elaborating an expression in Dart
Expand Down Expand Up @@ -1602,7 +1581,7 @@ static type `T`, where `m` and `T` are determined as follows:

- If `T_0` is `void`, there is a compile-time error.

- Let `U_0` be the [bound resolution](#Bound-resolution) of `T_0`.
- Let `U_0` be the unique type such that `T_0` is `U_0` bounded.

- If `U_0` is `dynamic` or `Never`, or `U_0` is `Function` and `id` is `call`,
then:
Expand Down
8 changes: 8 additions & 0 deletions specification/dartLangSpec.tex
Original file line number Diff line number Diff line change
Expand Up @@ -13039,6 +13039,7 @@ \subsubsection{Binding Actuals to Formals}
\LMHash{}%
For a given type $T_0$, we introduce the notion of a
\IndexCustom{$T_0$ bounded type}{type!T0 bounded}:
If $T_0$ is neither a type variable nor an intersection type, then
$T_0$ itself is $T_0$ bounded;
if $B$ is $T_0$ bounded and
$X$ is a type variable with bound $B$
Expand All @@ -13054,6 +13055,13 @@ \subsubsection{Binding Actuals to Formals}
Similarly for a
\IndexCustom{\FUNCTION{} bounded type}{type!function bounded}.

\commentary{%
Since it is illegal for a type parameter to be a supertype of its own
bound, it follows that for any type $T$, there exists exactly one type
$T_0$ for which $T$ is $T_0$ bounded. $T_0$ can be regarded as a
non-type-variable type which is a (minimal) supertype of $T$.%
}

\LMHash{}%
A
\IndexCustom{function-type bounded type}{type!function-type bounded}
Expand Down