Initial efforts at specifying inference in function bodies and initializers #3803
Conversation
…lizers. This is just the beginning of my effort; I'm sending it around to get feedback on the style and general approach I'm taking. What's included here: - Some overview information, including some text about soundness guarantees (I want to include informal proofs of soundness as non-normative text along with the inference algorithm, so I need to define some terms). - Details about coercions (not complete). - Inference for the following expression types: `null`, numbers, boolean literals, string literals (including interpolation), symbol literals, `throw`, `this`, logical boolean expressions, and `await`.
There was a problem hiding this comment.
This is a great start, and I think most of the way there. I am not convinced that trying to specify the runtime semantics and do the informal soundness proof inline is going to be tractable, but I'm open to being convinced otherwise. I'd suggest doing a couple of interesting cases around 1) places where coercions occur, and 2) non-local semantics (e.g. method invocations) to try to pressure test the approach here. Overall though, I think this looks great!
| @@ -970,6 +970,391 @@ with respect to `L` under constraints `C0` | |||
| under constraints `Ci`. | |||
|
|
|||
|
|
|||
| # Body inference | |||
There was a problem hiding this comment.
I think I would probably suggest phrasing this as "expression inference" which is what most of this is, possibly followed separately by sections on "statement inference" and "block inference" etc.
| that constitute method bodies and initializer expressions (expressions, | ||
| statements, patterns, and collection elements) to coresponding artifacts in the | ||
| compiled output (referred to as "compilation artifacts"). The precise form of | ||
| compilation artifacts is not dictated by the specification; instead they are |
There was a problem hiding this comment.
I don't quite know what this sentence is saying. What does it mean to be "specified in terms of their runtime behavior"?
| specified in terms of their runtime behavior. | ||
|
|
||
| When executed, a compilation artifact may behave in one of three ways: it may | ||
| complete normally, complete with an exception, or fail to complete at all |
There was a problem hiding this comment.
I'm not entirely sure about using "complete" here, because it is fairly overloaded in the spec and elsewhere. Maybe just say "it may evaluate to a value, it may throw an exception, or it may diverge"?
| ## Expression artifacts | ||
|
|
||
| Some compilation artifacts, typically those associated with expressions in the | ||
| source code, have the property that when they complete normally, there will be |
There was a problem hiding this comment.
Again, I think the "complete normally" terminology is going to be confusing, since it is used elsewhere in the spec already.
| resulting value will be an instance of `T`. This guarantee is known as | ||
| _tear-off soundness_. | ||
|
|
||
| - It is guaranteed that if a future is an instance of the type `Future<T>`, and |
There was a problem hiding this comment.
This doesn't feel like something that should need to be special cased, does it really?
| - Let `m` be an expression artifact whose runtime behavior is to complete with a | ||
| value that is the target of the current instance member invocation. | ||
|
|
||
| _Expression soundness follows from the fact that within a class, enum, mixin, or |
There was a problem hiding this comment.
This doesn't seem quite coherent to me. I know this is non-normative and informal, but maybe worth rewording at least a bit? The reasons I say it's not entirely coherent, is that it's trying to base this off of the (static?) type of the receiver of the member invocation that resulted in the code reaching a reference to this. But that static type could be dynamic, or a supertype of T. I think the informal soundness argument here (and this is probably the most subtle and easy to get wrong soundness argument in all of OO programming) is something like "the static interface type T of the class in which the member containing the reference to this was defined is, by soundness, a supertype of the runtime type of the instance on which that member was invoked". Or something. Without working through a proof it's hard to even talk about.
resources/type-system/inference.md
Outdated
| context `bool`, and then coercing the result to type `bool`. | ||
|
|
||
| - Let `m_2` be the result of performing expression type inference on `e_2`, in | ||
| context `bool`, and then coercring the result to type `bool`. |
| - Let `m` be an expression artifact whose runtime behavior is as follows: | ||
|
|
||
| - Execute expression artifact `m_1`, and let `o_1` be the resulting value. _By | ||
| expression soundness, `o_1` will be an instance of the type `T_1`._ |
There was a problem hiding this comment.
Technically, "the runtime type of o_1 will be a subtype of T_1", since T_1 may be something like dynamic. (I'm ignoring extension types - to be precise we'd have to account for extension type erasure here).
|
|
||
| - Define `o_2` as follows: | ||
|
|
||
| - If `o_1` is a subtype of `Future<T>`, then let `o_2` be `o_1`. |
There was a problem hiding this comment.
If the runtime type of o_1 is a ....
|
|
||
| - If `o_1` is a subtype of `Future<T>`, then let `o_2` be `o_1`. | ||
|
|
||
| - Otherwise, let `o_2` be the result of creating a new object using the |
There was a problem hiding this comment.
I don't think this is exactly right. I don't have the runtime semantics loaded into my head right now, I'd have to chase them down, but at a minimum you have to account for dynamic. I think the runtime semantics are maybe something like o_2 = (o_1 is Future<T>) ? o_1 : Future.value(o_1 as T)?
Thanks Leaf! I've already made some easy fixes based on a few of your comments. I'm going to go ahead and land this now and then iterate on the rest. |
This is just the beginning of my effort; I'm sending it around to get feedback on the style and general approach I'm taking.
What's included here:
Some overview information, including some text about soundness guarantees (I want to include informal proofs of soundness as non-normative text along with the inference algorithm, so I need to define some terms).
Details about coercions (not complete).
Inference for the following expression types:
null, numbers, boolean literals, string literals (including interpolation), symbol literals,throw,this, logical boolean expressions, andawait.Thanks for your contribution! Please replace this text with a description of what this PR is changing or adding and why, list any relevant issues, and review the contribution guidelines below.
Contribution guidelines:
dart format.Note that many Dart repos have a weekly cadence for reviewing PRs - please allow for some latency before initial review feedback.