Specify null safety subtyping #3515
Conversation
eernstg
force-pushed
the
specify_null_safety_subtyping_dec23
branch
from
082c391
to
a9f4886
Compare
| which means that this seemingly expensive step can be confined to some extent.% | ||
| } | ||
| \commentary{% | ||
| Note that this rule is admissible, and can be safely elided if desired.% |
There was a problem hiding this comment.
Define "admissible". It's a term of art not used elsewhere in the specification, so we cannot assume the reader to be familiar with it.
eernstg
force-pushed
the
specify_null_safety_subtyping_dec23
branch
from
a9f4886
to
0fd9980
Compare
eernstg
force-pushed
the
specify_null_safety_subtyping_dec23
branch
from
0fd9980
to
84e6d38
Compare
eernstg
force-pushed
the
specify_null_safety_subtyping_dec23
branch
from
84e6d38
to
4fcf76e
Compare
eernstg
force-pushed
the
specify_null_safety_subtyping_dec23
branch
from
4fcf76e
to
b7cdb30
Compare
eernstg
force-pushed
the
specify_null_safety_subtyping_dec23
branch
from
b7cdb30
to
bf98431
Compare
|
Based on the output from Front matterOnly comments. @@ -21633,128 +21631,188 @@Section 'Subtypes': Now mentions intersection types. Figure 'Subtype rules': Changed a lot. Subsection 'Meta-Variables': Slightly changes presentation of Subsection 'Subtype Rules': Introduces the 'canonical syntax' of a Subsection 'Being a Subtype': Extensively rewritten. Subsubsection 'Informal subtype rule descriptions': Rewritten extensively. Subsection 'Additional Subtyping Concepts': Extensively rewritten. Section 'Function Types': Last paragraph modified. Section 'Type Function': Rewritten. @@ -22482,7 +22498,7 @@Just the title of section 'Type dynamic' was adjusted, for consistency Section 'Type FutureOr': Just adding missing Section 'Type void': Removed commentary that reiterated an obsolete Subsection 'Void Soundness': Example updated, plus body text about the @@ -23324,156 +23324,238 @@Section 'Appendix: Algorithmic Subtyping': Updated to use the |
| if $T_1$ is \code{FutureOr<$S$>} for some $S$, | ||
| then the query is true if{}f \SubtypeNE{\code{Null}}{S}. | ||
| \item | ||
| if $T_1$ is \code{$S$?} for some $S$ then the query is true. |
There was a problem hiding this comment.
The case where
| \item | ||
| \textbf{Left Top:} | ||
| if $T_0$ is \DYNAMIC{} or \VOID{} | ||
| then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{\code{Object?}}{T_1}. |
There was a problem hiding this comment.
I think it should be 'iff' rather than 'if', so I changed it.
It could be implied that it works the same with 'if' because it was already stated that it is never necessary to try subsequent cases when a syntactic match has been determined, but many rules further down use 'iff' so it seems consistent to do it here as well.
| \item | ||
| \textbf{Left Promoted Variable:} | ||
| If $T_0$ is a promoted type variable \code{$X_0$\,\&\,$S_0$} | ||
| then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S_0}{T_1}. |
There was a problem hiding this comment.
In 'subtyping.md' there is no 'If', and the second line is just 'and S0 <: T1'. However, that seems to make it less obvious that if T0 is a promoted type variable X0 & S0 but S0 <: T1 cannot be proven, then we do have a known false outcome, rather than a non-matching rule.
| \item | ||
| \textbf{Left Type Variable Bound:} | ||
| $T_0$ is a type variable $X_0$ with bound $B_0$ | ||
| then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{B_0}{T_1}. |
There was a problem hiding this comment.
Similar to the previous rule. A few more rules below got the same treatment.
| $T_0$ is a function type and $T_1$ is \FUNCTION. | ||
| \item | ||
| \textbf{Record Type/Record:} | ||
| $T_0$ is a record type and $T_1$ is \RECORD. |
There was a problem hiding this comment.
This one is far into the future (that is, it comes with a version which is much higher than 2.13), so perhaps we should omit it (comment it out)?
Note that records are only mentioned here in the appendix, they do not occur in the subtype rules figure.
| \item | ||
| If $T_0$ is \code{($V_0$, \ldots, $V_n$, \{$V_{n+1} d_{n+1}$, \ldots, $V_m d_m$\})} | ||
| and $T_1$ is \code{($S_0$, \ldots, $S_n$, \{$S_{n+1} d_{n+1}$, \ldots, $S_m d_m$\})} | ||
| then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{V_i}{S_i} for each $i \in 0 .. m$. |
There was a problem hiding this comment.
Again a record type: Could be commented out for now.
| then the subtyping does not hold | ||
| (\commentary{% | ||
| i.e., the result of the subtyping query is known to be false% | ||
| }). |
There was a problem hiding this comment.
Like a few other rules, I believe 'Right Object' is admissible, but not required.
|
I tried to use |
|
I added a section about 'being the same type', and adjusted the text such that the thing previously known as 'canonical syntax' (now renamed to 'explicitly resolved syntax') is encapsulated in this section. Also, alpha equivalence has been made part of this 'being the same type' section. |
This PR contains the null-safety updates from #2605 (the overall null-safety PR) that are concerned with subtyping. The intention is that we process and land this PR, and #2605 will then be made smaller when it is rebased over this one, thus allowing us to deal with the null-safety update in smaller portions.