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

Can we promote through record fields? #2503

Open
eernstg opened this issue Sep 20, 2022 · 4 comments
Open

Can we promote through record fields? #2503

eernstg opened this issue Sep 20, 2022 · 4 comments
Labels
question Further information is requested records Issues related to records.

Comments

@eernstg
Copy link
Member

eernstg commented Sep 20, 2022

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?

@eernstg eernstg added question Further information is requested records Issues related to records. labels Sep 20, 2022
@stereotype441
Copy link
Member

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.

@munificent munificent changed the title For promotion, do we lift automatic 'type of interest'-ness and similar properties? Can we promote through record fields? May 18, 2023
@lrhn
Copy link
Member

lrhn commented May 19, 2023

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
Copy link
Member

nex3 commented Jun 27, 2023

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
Copy link
Member

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());
  }
}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
question Further information is requested records Issues related to records.
Projects
None yet
Development

No branches or pull requests

5 participants