Update flatten definition #2713
Conversation
|
Visit the preview URL for this PR (updated for commit 4f450ab): https://dart-specification--pr2713-specify-flatten-inte-jhd4ajan.web.app (expires Tue, 20 Dec 2022 17:13:14 GMT) 🔥 via Firebase Hosting GitHub Action 🌎 Sign: 6941ecd630c4f067ff3d02708a45ae0f0a42b88a |
| \item if $S$ has future type $U$ | ||
| then \DefEquals{\flatten{T}}{\code{\flatten{U}}}. | ||
| \item otherwise, | ||
| \DefEquals{\flatten{T}}{\code{\flatten{X}}}. |
There was a problem hiding this comment.
... which falls back to case-analysis on the bound of X, which means we use the bound, even on a promoted type variable, if it's promoted to a non-future-value-having type.
I'd say \DefEquals{\flatten{T}}{\code{X}} to be consistent with what we have now.
Example:
- Have
<X extends FutureOr<Object?>>andX o = ...; - Promote
otoX & Objectbyo is Object. - Do
await o. X&Objecthas no future value type, so we fall back on flatten(X)Xhas future typeObject?.- So
await o, withoof typeX & Object, has typeObject?.
It's not unsound, because a result type of Object? never is, but I'm not absolutely sure it's what we want.
(Not entirely sure it isn't either. But I want to be sure either way.)
There was a problem hiding this comment.
we fall back on flatten(
X)
Yes flatten(X & Object) is flatten(X), because Object does not have a future type.
But X has future type FutureOr<Object?> so flatten(X) is Object?. So await o will await o and get the Object?, statically typed as Object?, which is sound.
I guess you're saying that if the developer tests explicitly for o is Object then we're supposed to forget that we know that anything-X is a Future<Object?> as well.
It is not obvious to me that this would be the natural behavior. I tend to think it's OK to find the future type in the type variable in the case where the other operand of the intersection type doesn't have any.
specification/dartLangSpec.tex
Outdated
| or \code{FutureOr<$S$>?} bounded | ||
| then the future type of $T$ is \code{Future<$S$>?} | ||
| respectively \code{FutureOr<$S$>?}. | ||
| \item Otherwise, $T$ has no future type. |
There was a problem hiding this comment.
Does not seem to account for X? or (X & B)? (if that exists), because those are not bounded by anything but themselves (they are not type variables or promoted type variables, they just contain some, so the last two clauses of "is-S-bounded" do not apply), and they have no super-interfaces.
Maybe:
- If
TimplementsFuture<S>for someS,Thas future typeFuture<S>. - Otherwise, if
TisFutureOr<S>for someS,Thas future typeFuture<S>. - Otherwise, if
TisBbounded for someBandBhas future typeF, so doesT. - Otherwise, if
TisR?andRhas future typeF,Thas future typeF?. - Otherwise
Thas no future type.
There was a problem hiding this comment.
X? is handled by the first case in flatten, X? does not have a future type of its own.
(X & B)? cannot occur, intersection types are designed to be top-level only.
About the rulesets:
If
TimplementsFuture<S>for someS,Thas future typeFuture<S>.
This is my first item.
Otherwise, if
TisFutureOr<S>for someS,Thas future typeFuture<S>.
This is different, but flatten would take those two different intermediate results to the same end result.
Otherwise, if
TisBbounded for someBandBhas future typeF, so doesT.
This is somewhat redundant: It may include a usage of the first item, but it would then already be covered by the first item.
Otherwise, if
TisR?andRhas future typeF,Thas future typeF?.
I could use this to make the third item simpler, but it would only be applicable in some cases after having applied item 2.
Otherwise T has no future type.
OK, I don't see any discrepancies so we could use one or the other definition, but it's not obvious to me that this one is simpler to reason about.
specification/dartLangSpec.tex
Outdated
| or \code{FutureOr<$S$>?} bounded | ||
| then the future type of $T$ is \code{Future<$S$>?} | ||
| respectively \code{FutureOr<$S$>?}. | ||
| \item Otherwise, $T$ has no future type. |
There was a problem hiding this comment.
X? is handled by the first case in flatten, X? does not have a future type of its own.
(X & B)? cannot occur, intersection types are designed to be top-level only.
About the rulesets:
If
TimplementsFuture<S>for someS,Thas future typeFuture<S>.
This is my first item.
Otherwise, if
TisFutureOr<S>for someS,Thas future typeFuture<S>.
This is different, but flatten would take those two different intermediate results to the same end result.
Otherwise, if
TisBbounded for someBandBhas future typeF, so doesT.
This is somewhat redundant: It may include a usage of the first item, but it would then already be covered by the first item.
Otherwise, if
TisR?andRhas future typeF,Thas future typeF?.
I could use this to make the third item simpler, but it would only be applicable in some cases after having applied item 2.
Otherwise T has no future type.
OK, I don't see any discrepancies so we could use one or the other definition, but it's not obvious to me that this one is simpler to reason about.
| \item if $S$ has future type $U$ | ||
| then \DefEquals{\flatten{T}}{\code{\flatten{U}}}. | ||
| \item otherwise, | ||
| \DefEquals{\flatten{T}}{\code{\flatten{X}}}. |
There was a problem hiding this comment.
we fall back on flatten(
X)
Yes flatten(X & Object) is flatten(X), because Object does not have a future type.
But X has future type FutureOr<Object?> so flatten(X) is Object?. So await o will await o and get the Object?, statically typed as Object?, which is sound.
I guess you're saying that if the developer tests explicitly for o is Object then we're supposed to forget that we know that anything-X is a Future<Object?> as well.
It is not obvious to me that this would be the natural behavior. I tend to think it's OK to find the future type in the type variable in the case where the other operand of the intersection type doesn't have any.
|
@lrhn, I landed this. Let's take another iteration in a new PR, if needed. |
The definition of flatten needed yet another revision in order to cover intersection types properly.