dart-lang / dart-lang/language

Require the static type of all expressions to be a subtype of their context; push coercions down to satisfy this.

Open
#3,471 5 comments 6 reactions 1 assignee Claimed by @stereotype441 View on GitHub
feature type-inference
Dominant language
TeX
Stars
2.9k
Forks
239
Avg merge
2d 18h
Merged PRs (30d)
14

Description

# Background

Usually, an expression's context type schema describes what the static type of the expression must be (or be coercible to) in order to avoid a compile-time error. For example, in the declaration `int x = f();`, if the static type of `f()` is not either `int` or a type coercible to `int` (i.e., `dynamic`), then a compile-time error will occur; therefore, `f()` is analyzed with a context of `int`.

However, there are two notable exceptions:

- When an assignment is made to a local variable that's undergone type promotion, the _promoted_ type of the variable is used as the context for analyzing the right hand side of the assignment. If the static type of the expression winds up not being a subtype of the promoted type, no compile-time error occurs; instead, the variable is simply demoted.
- When an if-null expression, `e1 ?? e2`, has no context type schema, or its type schema is `dynamic` or `_`, the static type of `e1` is used as the context for analyzing `e2`. If the static type of `e2` winds up not being a subtype of its context, no compile-time error necessarily occurs; instead, LUB is used to compute the static type of the whole if-null expression.

As a result of these two exceptions, we've implemented coercions in a somewhat counter-intuitive way: instead of coercing the type of each expression as necessary to ensure that it's a subtype of its context (or reporting a compile time error if no suitable coercion exists), we've implemented some coercions so that they take effect only at the point of an assignability check. Notably, we do this for the dynamic downcast coercion, and this leads to an unfortunate footgun. Consider:

```dart
String intOrDynamic(bool b, int i, dynamic d) => b ? i : d;
```

This code is accepted without any static errors or warnings. The return type `String` is used as the context type for analyzing the conditional expression `b ? i : d`; this is pushed down into the two branches of the conditional, `i` and `d`. Although `i` has type `int`, which is not assignable to `String`, no error is reported, because there is no assignability check inside a conditional expression. By the same reasoning, analysis of `d` with context `String` does not (yet) produce a dynamic downcast. So the static type of `i` is `int` and the static type of `d` is `dynamic`. Now, the static type of the whole conditional expression is `LUB(int, dynamic)`, which is `dynamic`. At _this_ point, an assignability check is performed, to see if `=> b ? i : d` can be used as the body of a function with return type `String`. Since a coercion exists from `dynamic` to `String` (namely, dynamic downcast), there is no static error.

But it would be really nice if this code had a static error. Because at runtime, it's guaranteed to throw an exception whenever `b` is `true`.

We have often talked about redefining the behavior of conditional expressions so that if either branch of the conditional expression isn't assignable to the context, a compile-time error would be issued. But if we did that, then things would get weird because of the exceptions noted above. For example, this is a valid and reasonable thing to do:

```dart
f(Object o, bool b, double d, String s) {
if (o is int) { // promotes `o` to `int`
...
if (b) {
o = d; // demotes `o` back to `Object`
} else {
o = s; // demotes `o` back to `Object`
}
}
}
```

And it also seems reasonable that we could refactor the "if/else" into a conditional expression, like so:

```dart
f(Object o, bool b, double d, String ) {
if (o is int) { // promotes `o` to `int`
....
o = b ? d : s; // demotes `o` back to `Object`
}
}
```

But if we changed the behavior of conditional expressions so that it was an error if either branch didn't satisfy the context, then this innocent refactor would lead to a surprising compile-time error, because the context for `b ? d : s` is `int`, and neither `double` nor `String` is assignable to `int`.

Similar problems occur with switch expressions.

# Proposal

Change the treatment of assignments to promoted local variables, so that the context for the right hand side of the assignment is the the static (unpromoted) type of the local variable, not its promoted type.

Change the way we implement coercions so that for each expression in the program, a provisional static type is initally computed, using the rules for expression static types that we currently have, and then:

- Let `T` be the provisional static type of the expression.
- Let `R` be the greatest closure of the context type schema with respect to `_`. Or, if the expression has no type schema, let `R` be `dynamic`.
- If `T <: R`, then `T` is the static type of the expression, and no coercion is applied.
- Otherwise, if the expression is a conditional expression, switch expression, or if-null expression, then the static type of the expression is `R` _(See the "soundness" section below for why this is ok to do)_.
- Otherwise, if a coercion exists from type `T` to `U`, and `U <: R`, then that coercion is applied, and the static type of the expression is `U`.
- Otherwise, a compile time error is reported.

_(Note that these bullet points establish the invariant that the static type of *any* expression is a subtype of the greatest closure if its context type schema with respect to `_`.)_

# Consequences

## Different type inference for the right hand side of an assignment to a promoted local variable

Today, when an assignment is made to a promoted local variable, the right hand side is analyzed using the _promoted_ type of the variable as its context. So, for example:

```dart
f(Object o) {
if (o is List) {
...
o = [];
}
}
```

Since `o` is promoted to `List` at the time of the assignment, `[]` is analyzed using a context of `List`, and therefore `[]` is interpreted as `[]`.

With the change, `[]` will be analyzed using a context of `Object` (the unpromoted type of `o`). So `[]` will be interpreted as `[]`.

I'm not sure whether this is better or worse. But I suspect that it will be very rare for it to make a difference in real-world code.

## Better handling of `dynamic` in conditional and switch expressions

Recall the `intOrDynamic` function:

```dart
String intOrDynamic(bool b, int i, dynamic d) => b ? i : d;
```

With the change, the context type `String` is still pushed down into the subexpression `i`. A provisional static type of `int` is computed for `i`. But now, following the bullet points above, we see that:
- `T` is `int`
- `R` is `String`
- `T` is not a subtype of `R`,
- the expression `i` is not a conditional expression, switch expression, or if-null expression,
- and no coercion exists from `T` to `U`, where `U <: R`.

Therefore a compile-time error is issued. The footgun has been fixed!

## Better handling of conditional and switch expressions where LUB produces too big a type.

Consider this code from https://github.com/dart-lang/language/issues/1618:

```dart
PSW foo(bool bar) {
final PSW result = bar ? CNB() : AB();
return result;
}

class CNB extends SW implements PSW { }

class AB extends SW implements PSW { }

class PSW implements W { }

class SW extends W { }

class W { }
```

Today, the conditional expression `bar ? CNB() : AB()` had a static type of `LUB(CNB, AB)`, which is `W`, leading to a compile-time error because `W` is not assignable to `PSW`.

With the change, the type `W` is merely the _provisional_ type of the conditional expression. Then, following the bullet points above:
- `T` is `W`
- `R` is `PSW`
- `T` is not a subtype of `R`
- the expression `bar ? CNB() : AB()` _is_ a conditional expression.

Therefore, the static type of `bar ? CNB() : AB()` is `R` (i.e., `PSW`).

This fully addresses https://github.com/dart-lang/language/issues/1618.

## If-null becomes slightly more restrictive

Consider the following code (which is allowed today):

```dart
List? maybeList = ...;
var somethingToIterate = maybeList ?? Iterable.empty();
for (var i in somethingToIterate) {
...
}
```

With the change, this becomes a compile-time error, because the context type for `Iterable.empty()` is `List?`, and `Iterable` is not a subtype of `List`.

This could definitely be a source of breakage for users, and we should investigate how often it arises in practice.

However, even if it does come up a non-trivial number of times, there are at least three easy fixes:
- Inline the variable `somethingToIterate` (i.e. `for (var i in maybeList ?? Iterable.empty())`). This works because the if-null expression now has a context of `Iterable<_>`, so this context is passed down to `Iterable.empty()` rather than using the static type of `maybeList` as the context.
- Give an explicit type of `Iterable` to `somethingToIterate`. This works for the same reason; the if-null expression now has a context, and that context is not `_` or `dynamic`.
- Add a cast to `maybeList`: `var somethingToIterate = (maybeList as Iterable?) ?? Iterable.empty();`. This works because the static type of the left hand side of the if-null expression is now `Iterable`, and this type is a suitable context for analyzing `Iterable.empty()`.

## Coercions are pushed down into if-null expressions, conditional expressions, and switch expressions.

Consider this code:

```dart
abstract class C {
void call();
}
void Function() f(bool b, C c, void Function() g) => b ? c : g;
```

Today, this produces a compile-time error, because the static type of `b ? c : g` is `LUB(C, void Function())`, which is `Object`, and `Object` is not assignable to `void Function()`.

With this change, the coercion is pushed down to the branches of the conditional. Since the provisional static type of `c` is `C`, which is not a subtype of `void Function()`, `c` is coerced using a `.call` tearoff, and the static type of `c` is `void Function()`. Which means the code is accepted, and interpreted as:

```dart
void Function() f(bool b, C c, void Function() g) => b ? c.call : g;
```

This should fully address https://github.com/dart-lang/language/issues/3363.

## Coercions are pushed down into cascade targets.

This has advantages and disadvantages.

On the advantage side, consider this code:

```dart
int f(dynamic d) => d..foo();
```

Today, the implicit downcast is interpreted as happening _outside_ the cascade, i.e.:

```dart
int f(dynamic d) => (d..foo()) as int;
```

This code is statically accepted, because it is permissible to call any method on a dynamic type. But it's guaranteed to throw an exception at runtime, because the only possible values for `d` which will survive the dynamic downcast are integers, and integers don't have a `foo` method.

With the change, the implicit downcast is interpreted as happening _inside_ the cascade, i.e.:

```dart
int f(dynamic d) => (d as int)..foo();
```

And therefore there will be a compile-time error.

On the disadvantage side, consider this code:

```dart
abstract class C {
void call();
void m();
}
void Function() f(C c) => c..m();
```

Today this is permitted, because the call to `m` happens before the implicit tearoff of `.call`. With the change, it will become a compile-time error.

If the user wants to keep the old behavior, they can always do the `.call` tearoff explicitly:

```dart
void Function() f(C c) => (c..m()).call;
```

# Soundness

As promised, here's why it's sound to treat the static type of a conditional expression, switch expression, or if-null expression as `R` (the greatest closure of the context type schema), even if the provisional static type is not a subtype of `R`.

Recall that the bullet points listed in the "proposal" section establish the invariant that the static type of every expression is a subtype of the greatest closure of its context type schema with respect to `_`.

For conditional expressions and switch expressions, the context type schema is passed down into each branch without alteration. Therefore, thanks to the invariant, the static type of each branch is a subtype of `R`. Since the runtime value of a conditional expression or switch expression is always obtained from one of its branches, if we assume soundness of the subexpressions, then the runtime type of the whole conditional exprssion or switch expression must also be a subtype of `R`. So it does not violate soundness to assign the whole conditional expression or switch expression a static type of `R`.

For an if-null expression `e1 ?? e2`, things are slightly more complicated. First, if the if-null expression has no context, or the context of the if-null expresison is either `_` or `dynamic`, then `R` is a top type, and therefore it does not violate soundness to assign the whole if-null expression a static type of `R`, because every runtime type is a subtype of a top type.

If, on the other hand, the context of the if-null expression is not either `_` or `dynamic`, then:
- Let `S` denote the context type schema for the if-null expression as a whole.
- So `R` is the greatest closure of `S` with respect to `_`.
- `e1` is analyzed using a context of `S?`. Therefore, by the invariant described above, the static type of `e1` is a subtype of `R?`.
- `e2` is analyzed using a context of `S`. Therefore, by the invariant, the static type of `e2` is a subtype of `R`.
- At runtime, if `e1` evaluates to a non-null value, then it will be used as the value for the whole if-null expression. Since `e1` has a static type of `R?`, and we're considering the case where it is not null, it follows, from the assumption of soundness of `e1`, that the runtime type of `e1` is a subtype of `R`, and therefore the runtime type of the whole if-null expression is a subtype of `R`.
- If, on the other hand, `e1` evaluates to `null`, then `e2` will be used as the value for the whole if-null expression. Since `e2` has a static type of `R`, it follows, from the assumption of soundness of `e2`, that the runtime type of `e2` is a subtype of `R`, and therefore the runtime type of the whole if-null expression is a subtype of `R`.
- Thus, in either case, the runtime type of the whole if-null expression is a subtype of `R`. So it does not violate soundness to assign the whole if-null expression a static type of `R`.

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.