Open stereotype441 opened 10 months ago
@dart-lang/language-team As discussed in today's language team meeting. Let me know what you think!
The one thing this will not allow, that I've wanted, is an aspirational context for the expression of an as
cast.
It would be nice if 1 as double
didn't throw, because it knows that you want a double
. That can only work if we have aspirational contexts.
(But it might just be trying to mash two different functionalities into one operator. The "completely unlimited unrelated cast" that it does today, and a more static kind of "I want this type" signal.)
Otherwise I think it's a good simplification.
Both promoted variable assignment and ??
changes are likely to be breaking.
On the other hand, using the unpromoted variable type should get rid of intersection types as context types, which is an added bonus. The difficulty is that the breakage of that won't be at the assignment itself, that'll likely still work, it'll just demote the variable and cause a later failure. That makes it harder to find and fix automatically.
The ??
issue is real, but I expect most occurrences of someList ?? Iterable.empty()
to have a context type, likely occurring directly on a for
/in
with a context type of Iterable<_>
.
(Which means that it becomes Iterable<dynamic>
today, and nobody notices the implicit dynamic?)
I think we should try to implement this, to see how much it breaks.
This is amazing! I'd certainly support trying out how breaking this is, and doing it even in the case where there is some breakage.
It's a highly desirable property of this proposal that it simplifies so many things, and that it includes #1618 and #3363.
One thing came to mind, in bullet 2 of the second rule of the proposal:
Let
R
be the greatest closure of the context type schema with respect to_
. Or, if the expression has no type schema, letR
bedynamic
.
IIUC then it makes no difference at all that we use dynamic
here rather than any other top type: The next bullet says that "if T <: R
" then the type of the expression is T
, and that's always true for any top type including dynamic
. So there's no need to worry about having a larger number of expressions of type dynamic
if we adopt these rules. On the other hand, it seems likely that we could just as well say "..., let R
be Object?
", just to practice a good habit. ;-)
(OK, we'd probably need to say "_
or Object?
" near the end in the section about ??
as well.)
The main reason to hesitate would be that this proposal will cause promoted variables to be demoted more often. You might even say that a promoted variable appears to wish to return to its unpromoted status because of the preference given to context types during type inference. That sounds like changing the user experience from the current level, and moving it down a notch. That could be a source of serious disappointment.
It would be nice if we could rely on the following migration scenario: We introduce the new rules, some promoted variables get demoted, and then there are errors about those variables later on, and developers will undo all the changes that matter because they'll change things like v = []
to v = <T>[]
to avoid the demotion. This is a good scenario because the breakage occurs at compile time.
However, it's perfectly possible that there are no errors when v
is used later on, if v
is a List<dynamic>
after the change. So we can't really hope for compile-time-only breakage.
Maybe we should link this change (at least in terms of migration advice) with some 'strict-...' options, to catch locations where the type dynamic
suddenly pops up? Perhaps it would be useful to have a lint that flags variable demotions?
(As usual, it might be useful to have differential analysis, flagging locations where we have variable demotions that didn't occur with the pre-change rules, but that's probably much more work.)
I'm starting work on this. I plan to do a prototype first, then see how much breakage it causes inside google3. Once I have that information we can re-assess whether we want to change course.
I filed an issue here to explore a corner of this that I believe is not covered above.
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 off()
is not eitherint
or a type coercible toint
(i.e.,dynamic
), then a compile-time error will occur; therefore,f()
is analyzed with a context ofint
.However, there are two notable exceptions:
e1 ?? e2
, has no context type schema, or its type schema isdynamic
or_
, the static type ofe1
is used as the context for analyzinge2
. If the static type ofe2
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:
This code is accepted without any static errors or warnings. The return type
String
is used as the context type for analyzing the conditional expressionb ? i : d
; this is pushed down into the two branches of the conditional,i
andd
. Althoughi
has typeint
, which is not assignable toString
, no error is reported, because there is no assignability check inside a conditional expression. By the same reasoning, analysis ofd
with contextString
does not (yet) produce a dynamic downcast. So the static type ofi
isint
and the static type ofd
isdynamic
. Now, the static type of the whole conditional expression isLUB(int, dynamic)
, which isdynamic
. 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 typeString
. Since a coercion exists fromdynamic
toString
(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
istrue
.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:
And it also seems reasonable that we could refactor the "if/else" into a conditional expression, like so:
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
isint
, and neitherdouble
norString
is assignable toint
.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:
T
be the provisional static type of the expression.R
be the greatest closure of the context type schema with respect to_
. Or, if the expression has no type schema, letR
bedynamic
.T <: R
, thenT
is the static type of the expression, and no coercion is applied.R
(See the "soundness" section below for why this is ok to do).T
toU
, andU <: R
, then that coercion is applied, and the static type of the expression isU
.(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:
Since
o
is promoted toList<int>
at the time of the assignment,[]
is analyzed using a context ofList<int>
, and therefore[]
is interpreted as<int>[]
.With the change,
[]
will be analyzed using a context ofObject
(the unpromoted type ofo
). So[]
will be interpreted as<dynamic>[]
.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 expressionsRecall the
intOrDynamic
function:With the change, the context type
String
is still pushed down into the subexpressioni
. A provisional static type ofint
is computed fori
. But now, following the bullet points above, we see that:T
isint
R
isString
T
is not a subtype ofR
,i
is not a conditional expression, switch expression, or if-null expression,T
toU
, whereU <: 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:
Today, the conditional expression
bar ? CNB() : AB()
had a static type ofLUB(CNB, AB)
, which isW
, leading to a compile-time error becauseW
is not assignable toPSW
.With the change, the type
W
is merely the provisional type of the conditional expression. Then, following the bullet points above:T
isW
R
isPSW
T
is not a subtype ofR
bar ? CNB() : AB()
is a conditional expression.Therefore, the static type of
bar ? CNB() : AB()
isR
(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):
With the change, this becomes a compile-time error, because the context type for
Iterable.empty()
isList<int>?
, andIterable
is not a subtype ofList
.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:
somethingToIterate
(i.e.for (var i in maybeList ?? Iterable.empty())
). This works because the if-null expression now has a context ofIterable<_>
, so this context is passed down toIterable.empty()
rather than using the static type ofmaybeList
as the context.Iterable<int>
tosomethingToIterate
. This works for the same reason; the if-null expression now has a context, and that context is not_
ordynamic
.maybeList
:var somethingToIterate = (maybeList as Iterable<int>?) ?? Iterable.empty();
. This works because the static type of the left hand side of the if-null expression is nowIterable<int>
, and this type is a suitable context for analyzingIterable.empty()
.Coercions are pushed down into if-null expressions, conditional expressions, and switch expressions.
Consider this code:
Today, this produces a compile-time error, because the static type of
b ? c : g
isLUB(C, void Function())
, which isObject
, andObject
is not assignable tovoid Function()
.With this change, the coercion is pushed down to the branches of the conditional. Since the provisional static type of
c
isC
, which is not a subtype ofvoid Function()
,c
is coerced using a.call
tearoff, and the static type ofc
isvoid Function()
. Which means the code is accepted, and interpreted as: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:
Today, the implicit downcast is interpreted as happening outside the cascade, i.e.:
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 afoo
method.With the change, the implicit downcast is interpreted as happening inside the cascade, i.e.:
And therefore there will be a compile-time error.
On the disadvantage side, consider this code:
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: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 ofR
.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 ofR
. So it does not violate soundness to assign the whole conditional expression or switch expression a static type ofR
.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_
ordynamic
, thenR
is a top type, and therefore it does not violate soundness to assign the whole if-null expression a static type ofR
, 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
_
ordynamic
, then:S
denote the context type schema for the if-null expression as a whole.R
is the greatest closure ofS
with respect to_
.e1
is analyzed using a context ofS?
. Therefore, by the invariant described above, the static type ofe1
is a subtype ofR?
.e2
is analyzed using a context ofS
. Therefore, by the invariant, the static type ofe2
is a subtype ofR
.e1
evaluates to a non-null value, then it will be used as the value for the whole if-null expression. Sincee1
has a static type ofR?
, and we're considering the case where it is not null, it follows, from the assumption of soundness ofe1
, that the runtime type ofe1
is a subtype ofR
, and therefore the runtime type of the whole if-null expression is a subtype ofR
.e1
evaluates tonull
, thene2
will be used as the value for the whole if-null expression. Sincee2
has a static type ofR
, it follows, from the assumption of soundness ofe2
, that the runtime type ofe2
is a subtype ofR
, and therefore the runtime type of the whole if-null expression is a subtype ofR
.R
. So it does not violate soundness to assign the whole if-null expression a static type ofR
.