Can we promote through record fields?

[eernstg]

Consider the following example:

void main() {
  (int?, bool) pair = (42, true);
  pair.$0.isEven; // OK?
}

The rule would be that we can specify an arbitrary record structure (here \X, Y. (X?, Y)) and perform pointwise operations on it (transforming \X, Y. (X?, Y) to \X, Y. (X, Y)), and declaring that the latter is a 'type of interest' because it is a structurally lifted version of the standard rule that makes T a type of interest during initialization of a local variable with declared type T?. This allows us to promote from (int?, bool) to (int, bool), from (int?, (bool?, List<String>?)) to (int, (bool, List<String>?)), etc.

A similar phenomenon arises with intersection types, where we are immediately promoting a type which is a type variable X to an intersection type X & T, because it was initialized by an expression of type X & T.

void f<X>(X x) {
  if (x is int) {
    var y = x; // Inferred type of `y` is `X`, and `y` is immediately promoted to `X & int`.
    x = y; // OK.
    int i = y; // OK.
  }
}

Are we going to apply similar promotions based on "lifted" types of interest?

void f<X>(X x) {
  if (x is int) {
    var r = (x, true);
    X y = r.$0; // OK.
    int i = r.$0; // OK?
  }
}

We could proceed as usual (in some lifted sense) and erase the type of the record literal from (X & int, bool) to (X, bool). However, it is actually sound to maintain that the record has the type (X & int, bool), because the run-time type of the record is computed from the run-time types of the field values, and the actual object denoted by x at this point is known to have a type S such that S <: int and S <: X.

But it's a potentially deep violation of the current rules that we even consider a type like (X & int, bool), because an intersection type does not otherwise occur as a subterm of any other type.

In any case, lifting initializer based promotions to record types seems to be a non-trivial exercise.

@natebosch, @lrhn, @munificent, @leafpetersen, @jakemac53, @kallentu, @stereotype441, WDYT?

[stereotype441]

Consider the following example:

void main() {
  (int?, bool) pair = (42, true);
  pair.$0.isEven; // OK?
}

The rule would be that we can specify an arbitrary record structure (here \X, Y. (X?, Y)) and perform pointwise operations on it (transforming \X, Y. (X?, Y) to \X, Y. (X, Y)), and declaring that the latter is a 'type of interest' because it is a structurally lifted version of the standard rule that makes T a type of interest during initialization of a local variable with declared type T?. This allows us to promote from (int?, bool) to (int, bool), from (int?, (bool?, List<String>?)) to (int, (bool, List<String>?)), etc.

This seems reasonable to me. We already have the technology to track types of interest and promotions for private class fields (soon to be enabled as part of #2020); extending this to record fields seems like a no-brainer.

A similar phenomenon arises with intersection types, where we are immediately promoting a type which is a type variable X to an intersection type X & T, because it was initialized by an expression of type X & T.

void f<X>(X x) {
  if (x is int) {
    var y = x; // Inferred type of `y` is `X`, and `y` is immediately promoted to `X & int`.
    x = y; // OK.
    int i = y; // OK.
  }
}

Are we going to apply similar promotions based on "lifted" types of interest?

void f<X>(X x) {
  if (x is int) {
    var r = (x, true);
    X y = r.$0; // OK.
    int i = r.$0; // OK?
  }
}

We could proceed as usual (in some lifted sense) and erase the type of the record literal from (X & int, bool) to (X, bool). However, it is actually sound to maintain that the record has the type (X & int, bool), because the run-time type of the record is computed from the run-time types of the field values, and the actual object denoted by x at this point is known to have a type S such that S <: int and S <: X.

But it's a potentially deep violation of the current rules that we even consider a type like (X & int, bool), because an intersection type does not otherwise occur as a subterm of any other type.

Personally wouldn't have any problem with this. It doesn't create any soundness problems, and it's really consistent with my mental model of records (which is that they're just extremely lightweight agglomerations of values that otherwise would have been stored in separate variables).

In any case, lifting initializer based promotions to record types seems to be a non-trivial exercise.

I don't have time to prototype it right now, but my intuition is that this would actually be a fairly straightforward extension of what flow analysis is already capable of doing. I'll add it to my list to explore in the coming weeks.

[lrhn]

I think allowing X&T as a component type of a record is safe. It's stable and covariant, so it's basically a value.
We just have to be careful to erase the intersection when necessary, and make sure code is ready to see it.

It's a little weird to allow that, and not, say FutureOr<X&T> or X&T Function(), but the former quickly leads to Future<X&T>, which has the type parameter occurring contravariantly in catchError, and I'm not even sure what that means. (But most likely it's impossible to call catchError with a valid argument.)

[nex3]

Porting over another motivating example from #3160 that came up in some real-world code:

void function(int? arg1, int? arg2) {
  switch ((arg1, arg2)) {
    case (null, null): print("both null");
    case (var first, null): print(first.abs());
    case (null, var second): print(second.abs());
  }
}

Specifically, promoting through record fields makes it much nicer to construct a tuple to match against.

[natebosch]

You can force promotion if null is checked in the pattern.

void function(int? arg1, int? arg2) {
  switch ((arg1, arg2)) {
    case (null, null): print("both null");
    case (var first?, null): print(first.abs());
    case (null, var second?): print(second.abs());
  }
}