From b9279cb22bf8b4b57aa79ce494c5444483efb3d2 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Wed, 1 Jun 2022 11:23:50 +0200 Subject: [PATCH] Review response --- specification/dartLangSpec.tex | 78 ++++++++++++++++++---------------- 1 file changed, 42 insertions(+), 36 deletions(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index a1c5184174..39397a962e 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -13704,7 +13704,7 @@ \subsubsection{Ordinary Invocation} Otherwise, let $d$ be the result of getter lookup for $m$ in $T$ with respect to $L$, and let $F$ be the return type of $d$. -(\commentary{ +(\commentary{% Since \code{$T$.$m$} exists we cannot have a failure in both lookups.% }) If the getter return type $F$ is an interface type @@ -13728,7 +13728,7 @@ \subsubsection{Ordinary Invocation} \LMHash{}% It is a compile-time error to invoke an instance method on a type literal that is immediately followed by the token `.' (a period). -\commentary{ +\commentary{% For instance, \code{int.toString()} is an error.% } @@ -20316,13 +20316,13 @@ \subsection{Type Aliases} it is a compile-time error if $T$ is not regular-bounded, and it is a compile-time error if any type occurring in $T$ is not well-bounded. -\commentary{ +\commentary{% This means that the bounds declared for the formal type parameters of a generic type alias must be such that when they are satisfied, the bounds that pertain to the body are also satisfied, and a type occurring as a subterm of the body can violate its bounds, -but only if it is a correct super-bounded type. +but only if it is a correct super-bounded type.% } \LMHash{}% @@ -22363,7 +22363,7 @@ \subsection{Standard Upper Bounds and Standard Lower Bounds} \DefEquals{\UpperBoundType{$T_1$}{$T_2$}}{T_2}, if \SubtypeNE{T_1}{T_2}. - \commentary{ + \commentary{% In this and in the following cases, both types must be interface types.% } \item @@ -22620,7 +22620,7 @@ \subsection{Standard Upper Bounds and Standard Lower Bounds} \DefEquals{\LowerBoundType{$T_1$}{$T_2$}}{\code{Never}}, otherwise. \end{itemize} -\rationale{ +\rationale{% The rules defining \UpperBoundTypeName{} and \LowerBoundTypeName{} are somewhat redundant in that they explicitly specify a lot of pairs of symmetric cases. @@ -24412,6 +24412,7 @@ \subsection{Type Promotion} } \LMHash{}% +\BlindDefineSymbol{\ell, v}% Let $\ell$ be a location, and let $v$ be a local variable which is in scope at $\ell$. Assume that $\ell$ occurs after the declaration of $v$. @@ -24435,34 +24436,33 @@ \subsection{Type Promotion} \LMHash{}% In particular, -a check of the form \code{$v$\,\,==\,\,\NULL}, -\code{\NULL\,\,==\,\,$v$}, -or \code{$v$\,\,\IS\,\,Null} +an expression of the form \code{$v$\,\,==\,\,\NULL} or +\code{\NULL\,\,==\,\,$v$} where $v$ has type $T$ at $\ell$ promotes the type of $v$ -to \code{Null} in the \TRUE{} continuation, -and to \NonNullType{$T$} in the \FALSE{} continuation. - -%% TODO(eernst), for review: The null safety spec says that `T?` is -%% promoted to `T`, but implementations _do_ promote `X extends int?` to -%% `X & int`. So we may be able to specify something which will yield -%% slightly more precise types, and which is more precisely the implemented -%% behavior. -\LMHash{}% -A check of the form \code{$v$\,\,!=\,\,\NULL}, -\code{\NULL\,\,!=\,\,$v$}, -or \code{$v$\,\,\IS\,\,$T$} -where $v$ has static type $T?$ at $\ell$ +to \NonNullType{$T$} in the \FALSE{} continuation; +and an expression of the form \code{$v$\,\,!=\,\,\NULL} or +\code{\NULL\,\,!=\,\,$v$} +where $v$ has static type $T$ at $\ell$ +promotes the type of $v$ +to \NonNullType{$T$} in the \TRUE{} continuation. + +\LMHash{}% +Similarly, a type test of the form \code{$v$\,\,\IS\,\,$T$} promotes the type of $v$ to $T$ in the \TRUE{} continuation, -and to \code{Null} in the \FALSE{} continuation. +and a type check of the form \code{$v$\,\,\AS\,\,$T$} +promotes the type of $v$ +to $T$ in the continuation where the expression evaluated to an object +(\commentary{that is, it did not throw}). \commentary{% The resulting type of $v$ may be the obvious one, e.g., \code{$v$\,\,=\,\,1} may promote $v$ to \code{int}, but it may also give rise to a demotion -(changing the type of $v$ to a supertype of the type of $v$ at $\ell$), -and it may have no effect on the type of $v$ +(changing the type of $v$ to a supertype of the type of $v$ at $\ell$ +and potentially promoting it to some other type of interest). +It may also have no effect on the type of $v$ (e.g., when the static type of $e$ is not a type of interest). These details will be specified in a future version of this specification. @@ -24624,15 +24624,20 @@ \section*{Appendix: Algorithmic Subtyping} the one which is specified in Fig.~\ref{fig:subtypeRules}. It shows that Dart subtyping relationships can be decided with good performance. +This section is not normative. \LMHash{}% In this algorithm, types are considered to be the same when they have the same canonical syntax (\ref{theCanonicalSyntaxOfTypes}). +\commentary{% +For example, \SubtypeStd{\code{C}}{\code{C}} does not hold if +the two occurrences of \code{C} refer to declarations in different libraries.% +} The algorithm must be performed such that the first case that matches is always the case which is performed. The algorithm produces results which are both positive and negative -(\commentary{ +(\commentary{% that is, in some situations the subtype relation is determined to be false% }), which is important for performance because @@ -24644,16 +24649,18 @@ \section*{Appendix: Algorithmic Subtyping} \begin{itemize} \item \textbf{Reflexivity:} - if $T_0$ and $T_1$ are the same type then \SubtypeNE{T_0}{T_1} + if $T_0$ and $T_1$ are the same atomic type then \SubtypeNE{T_0}{T_1}. \commentary{% - Note that this check is necessary as the base case for primitive types, + This check is necessary as the base case for primitive types, and type variables, but not for composite types. In particular, a structural equality check is admissible, but not required here. - Pragmatically, non-constant time identity checks here are - counter-productive. - So this rule should only be used when $T$ is atomic.% + Non-constant time identity checks here are counter-productive + because the following rules will yield the same result anyway, + so we may just perform a full traversal of a large structure twice + for no reason. + Hence, this rule is only used when the given type is atomic.% } \item \textbf{Right Top:} @@ -24663,7 +24670,7 @@ \section*{Appendix: Algorithmic Subtyping} if $T_0$ is \DYNAMIC{} or \VOID{} then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{\code{Object?}}{T_1}. \item - \textbf{Left Bottom:} + \textbf{Bottom:} if $T_0$ is \code{Never} then \SubtypeNE{T_0}{T_1}. \item \textbf{Right Object:} @@ -24716,7 +24723,7 @@ \section*{Appendix: Algorithmic Subtyping} or a promoted type variables \code{$X_0$\,\&\,$S_0$} and $T_1$ is $X_0$ then \SubtypeNE{T_0}{T_1}. - \commentary{ + \commentary{% Note that this rule is admissible, and can be safely elided if desired.% } \item @@ -24799,7 +24806,7 @@ \section*{Appendix: Algorithmic Subtyping} for $i \in 0 .. q$. \item \SubtypeNE{U_0[Z_0/X_0, \ldots, Z_k/X_k]}{U_1[Z_0/Y_0, \ldots, Z_k/Y_k]}. \item $B_{0i}[Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i}[Z_0/Y_0, \ldots, Z_k/Y_k]$ - have the same canonical syntax, for $i \in 0 .. k$. + are subtypes of each other, for $i \in 0 .. k$. \end{itemize} \item \textbf{Named Function Types:} @@ -24840,8 +24847,7 @@ \section*{Appendix: Algorithmic Subtyping} \SubtypeNE{U_0[Z_0/X_0, \ldots, Z_k/X_k]}{U_1[Z_0/Y_0, \ldots, Z_k/Y_k]}. \item $B_{0i}[Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i}[Z_0/Y_0, \ldots, Z_k/Y_k]$ - have the same canonical syntax, - for each $i \in 0 .. k$. + are subtypes of each other, for each $i \in 0 .. k$. \end{itemize} \commentary{%