WIP

Author: eernstg

specification/dart.sty

@@ -322,10 +322,10 @@
 % Arguments: Return type, spacer, type parameter name, bound name,
 %   number of type parameters, parameter type, number of required parameters,
 %   name of optional parameters, number of optional parameters,
-%   name of `required` symbol.
+% The name of `required` symbol is always `r` (can't take 10 parms!!).
 \newcommand{\FunctionTypeNamed}[9]{%
   \FunctionType{#1}{#2}{#3}{#4}{#5}{\\
-    \mbox{}\qquad\FunctionTypeNamedArguments{#6}{#7}{#8}{#9}{#10}}}
+    \mbox{}\qquad\FunctionTypeNamedArguments{#6}{#7}{#8}{#9}{r}}}
 
 % Same as \FunctionType except suitable for inline usage, hence omitting
 % the spacer argument.
@@ -347,7 +347,7 @@
   \RawFunctionTypePositional{#1}{X}{B}{s}{T}{n}{k}}
 
 \newcommand{\FunctionTypeNamedStd}[1]{%
-  \FunctionTypeNamed{#1}{ }{X}{B}{s}{T}{n}{x}{k}{r}}
+  \FunctionTypeNamed{#1}{ }{X}{B}{s}{T}{n}{x}{k}}
 
 \newcommand{\RawFunctionTypeNamedStd}[1]{%
   \RawFunctionTypeNamed{#1}{X}{B}{s}{T}{n}{x}{k}{r}}
@@ -359,10 +359,10 @@
   \FunctionTypePositional{#1}{\\}{X}{B}{s}{T}{n}{k}}
 
 \newcommand{\FunctionTypeNamedStdCr}[1]{%
-  \FunctionTypeNamed{#1}{\\}{X}{B}{s}{T}{n}{x}{k}{r}}
+  \FunctionTypeNamed{#1}{\\}{X}{B}{s}{T}{n}{x}{k}}
 
 \newcommand{\FunctionTypeNamedStdArgCr}[1]{%
-  \FunctionTypeNamedArgCr{#1}{ }{X}{B}{s}{T}{n}{x}{k}{r}}
+  \FunctionTypeNamedArgCr{#1}{ }{X}{B}{s}{T}{n}{x}{k}}
 
 \newcommand{\FunctionTypeAllRequiredStdCr}[1]{%
   \FunctionTypeAllRequired{#1}{\\}{X}{B}{s}{T}{n}}

specification/dartLangSpec.tex

@@ -20689,9 +20689,6 @@ \subsection{Subtypes}
 \newcommand{\SrnRightTop}{2}
 \newcommand{\SrnLeftTop}{3}
 \newcommand{\SrnBottom}{4}
-%\newcommand{\SrnRightObjectOne}{} Redundant
-%\newcommand{\SrnRightObjectTwo}{} Redundant
-%\newcommand{\SrnRightObjectThree}{} Redundant
 \newcommand{\SrnRightObjectFour}{5}
 \newcommand{\SrnNullOne}{6}
 \newcommand{\SrnNullTwo}{7}
@@ -21302,7 +21299,8 @@ \subsection{Type Nullability}
 Nullable types are types which are
 definitively known to include the null object,
 regardless of the value of any type variables.
-This is equivalent to the syntactic criterion that $T$ is any of:
+If $T'$ is the transitive alias expansion (\ref{typedef}) of $T$
+then this is equivalent to the syntactic criterion that $T'$ is any of:
 
 \begin{itemize}[itemsep=-0.5ex]
 \item \VOID.
@@ -21324,7 +21322,8 @@ \subsection{Type Nullability}
 Non-nullable types are types which are definitively known to
 \emph{not} include the null object,
 regardless of the value of any type variables.
-This is equivalent to the syntactic criterion that $T$ is any of:
+If $T'$ is the transitive alias expansion (\ref{typedef}) of $T$
+then this is equivalent to the syntactic criterion that $T$ is any of:
 
 \begin{itemize}[itemsep=-0.5ex]
 \item \code{Never}.
@@ -21691,21 +21690,23 @@ \subsection{Type Normalization}
 
   \noindent
   then $T_r$ is
-  \FunctionTypePositional{R_0}{ }{X}{B}{s}{R}{n}{k}
+  \FunctionTypePositional{T'\!_0}{ }{X}{B'\!}{s}{T'\!}{n}{k}
 
   \noindent
-  where $R_i$ is \NormalizedTypeOf{$T_i$} for $i \in 0 .. n+k$.
+  where $T'\!_i$ is \NormalizedTypeOf{$T_i$} for $i \in 0 .. n+k$
+  and $B'\!_i$ is \NormalizedTypeOf{$B_i$} for $i \in 1 .. s$.
 \item If $T_u$ is of the form
   \FunctionTypeNamedStd{T_0}
 
   \noindent
   where $r_j$ is either \REQUIRED{} or empty
   then $T_r$ is
   \noindent
-  \FunctionTypeNamed{R_0}{ }{X}{B}{s}{R}{n}{x}{k}{r}
+  \FunctionTypeNamed{T'\!_0}{ }{X}{B'\!}{s}{T'\!}{n}{x}{k}
 
   \noindent
-  where $R_i$ is \NormalizedTypeOf{$T_i$} for $i \in 0 .. n+k$.
+  where $T'\!_i$ is \NormalizedTypeOf{$T_i$} for $i \in 0 .. n+k$
+  and $B'\!_i$ is \NormalizedTypeOf{$B_i$} for $i \in 0 .. s$.
 \end{itemize}
 
 \commentary{%
@@ -22043,8 +22044,8 @@ \subsection{Standard Upper Bounds and Standard Lower Bounds}
 which is defined as follows.
 Assume that $P_1$ and $P_2$ are two formal parameter type declarations
 with declared type $T_1$ respectively $T_2$,
-such that both are positional or both are named,
-with the same name \DefineSymbol{n}.
+such that both are positional,
+or both are named and have the same name \DefineSymbol{n}.
 Then \UpperBoundType{$P_1$}{$P_2$} (respectively \LowerBoundType{$P_1$}{$P_2$})
 is the formal parameter declaration $P$,
 with the following proporties:
@@ -22063,7 +22064,8 @@ \subsection{Standard Upper Bounds and Standard Lower Bounds}
   }
 \item
   $P$ is named if $P_1$ and $P_2$ are named.
-  In this case, the name of $P$ is $n$.
+  In this case, the name of $P$ is $n$
+  (\commentary{which is also the name of $P_1$ and $P_2$}).
   $P$ is marked with the modifier \REQUIRED{}
   if both $P_1$ and $P_2$ have this modifier
   (respectively, if either $P_1$ or $P_2$ has this modifier).
@@ -22242,22 +22244,25 @@ \subsection{Standard Upper Bounds and Standard Lower Bounds}
 
   \noindent
   \code{$T_1$\,\FUNCTION<$X_1$\,\EXTENDS\,$B_{11}$,\,\ldots,\,$X_m$\,%
-    \EXTENDS\,$B_{1m}$>($P_{11}$,\,\ldots,\,$P_{1k}$)}
+    \EXTENDS\,$B_{1m}$>($P_{11}$,\,\ldots[\ldots\,$P_{1k}$])}
 
   \noindent
   \code{$T_2$\,\FUNCTION<$X_1$\,\EXTENDS\,$B_{21}$,\,\ldots,\,$X_m$\,%
-    \EXTENDS\,$B_{2m}$>($P_{21}$,\,\ldots,\,$P_{2l}$)}
+    \EXTENDS\,$B_{2m}$>($P_{21}$,\,\ldots[\ldots\,$P_{2l}$])}
 
   \noindent
   such that each $B_{1i}$ and $B_{2i}$ are types with the same canonical syntax,
-  and both have the same number of required positional parameters.
+  and both $U_1$ or $U_2$ have
+  the same number of required positional parameters.
+  In the case where $U_1$ or $U_2$ has no optional positional parameters,
+  the brackets are omitted.
   Let $q$ be $\metavar{min}(k, l)$,
   let $T_3$ be \UpperBoundType{$T_1$}{$T_2$},
-  let $B_{3i}$ be $B_{1i}$, and
+  let $B_{3i}$ be $B_{1i}$, and finally
   let $P_{3i}$ be \LowerBoundType{$P_{1i}$}{$P_{2i}$}.
-  Then \DefEquals{\UpperBoundType{$U_1$}{$U_2$}}{%
+  Then \DefEqualsNewline{\UpperBoundType{$U_1$}{$U_2$}}{%
     \code{$T_3$\,\FUNCTION<$X_1$\,\EXTENDS\,$B_{31}$,\,\ldots,\,$X_m$\,%
-      \EXTENDS\,$B_{3m}$>($P_{31}$,\,\ldots,\,$P_{3q}$)}}.
+      \EXTENDS\,$B_{3m}$>($P_{31}$,\,\ldots[\ldots\,$P_{3q}$])}}.
 
   \commentary{%
     This case includes non-generic function types by allowing $m$ to be zero.%
@@ -22315,8 +22320,11 @@ \subsection{Standard Upper Bounds and Standard Lower Bounds}
 %%
 %% TODO(eernst), for review: Why do we not have a rule for
 %% \UpperBoundType{T1 Function(P1..Pm, [...])}{T2 Function(P1..Pk, {...}}}
-%% = T3 Function(R1..Rk), where the left operand has at least k parameters,
-%% plus the converse?
+%% = T3 Function(R1..Rk), where the left operand has at least k parameters
+%% and every named parameter of the right operand is optional (plus the
+%% same rule with operands swapped)?
+%% Motivation: Some expressions of type `Function` would then have a more
+%% precise type, and programs would be safer (a tiny bit, at least).
 %%
 \item
   \DefEquals{\UpperBoundType{$S_1$ \FUNCTION<\ldots>(\ldots)}{%
@@ -22679,7 +22687,7 @@ \subsubsection{The Standard Upper Bound of Distinct Interface Types}
 $\{\;T\;|\;T\,\in\,M\;\wedge\;\NominalTypeDepth{$T$}\,=\,n\,\}$
 for any natural number $n$.
 Let $q$ be the largest number such that $M_q$ has cardinality one.
-Such a number must exist because $M_0$ is $\{\code{Object?}\}$.
+Such a number must exist because $M_0$ is $\{\code{Object}\}$.
 The least upper bound of $I$ and $J$ is then the sole element of $M_q$.
 
 
@@ -22912,7 +22920,7 @@ \subsection{Least and Greatest Closure of Types}
     the least closure of $S$ with respect to $L$ is
 
     \noindent
-    \FunctionTypeNamed{U_0}{ }{X}{B}{s}{U}{n}{x}{k}{r}
+    \FunctionTypeNamed{U_0}{ }{X}{B}{s}{U}{n}{x}{k}
 
     \noindent
     where
@@ -22927,7 +22935,7 @@ \subsection{Least and Greatest Closure of Types}
     the greatest closure of $S$ with respect to $L$ is
 
     \noindent
-    \FunctionTypeNamed{U_0}{ }{X}{B}{s}{U}{n}{x}{k}{r}
+    \FunctionTypeNamed{U_0}{ }{X}{B}{s}{U}{n}{x}{k}
 
     \noindent
     where $U_0$ is the greatest closure of $T_0$ with respect to $L$,
@@ -22983,15 +22991,17 @@ \subsection{Types Bounded by Types}
 \LMLabel{typesBoundedByTypes}
 
 \LMHash{}%
-For a given type $T_0$, we introduce the notion of a
-\IndexCustom{$T_0$ bounded type}{type!T0 bounded}:
-$T_0$ itself is $T_0$ bounded;
-if $B$ is $T_0$ bounded and
+For a given type $T$, we introduce the notion of a
+% `T bounded` at the end should have been `$T$ bounded`, but makeindex
+% seems to be unable to allow math mode in that position.
+\IndexCustom{$T$ bounded type}{type!T bounded}:
+$T$ itself is $T$ bounded;
+if $B$ is $T$ bounded and
 $X$ is a type variable with bound $B$
-then $X$ is $T_0$ bounded;
-finally, if $B$ is $T_0$ bounded and
+then $X$ is $T$ bounded;
+finally, if $B$ is $T$ bounded and
 $X$ is a type variable
-then $X \& B$ is $T_0$ bounded.
+then $X \& B$ is $T$ bounded.
 
 \LMHash{}%
 In particular, a
@@ -23005,11 +23015,11 @@ \subsection{Types Bounded by Types}
 \LMHash{}%
 A
 \IndexCustom{function-type bounded type}{type!function-type bounded}
-is a type $T$ which is $T_0$ bounded where $T_0$ is a function type
+is a type $S$ which is $T$ bounded where $T$ is a function type
 (\ref{functionTypes}).
-A function-type bounded type $T$ has an
+A function-type bounded type $S$ has an
 \Index{associated function type}
-which is the unique function type $T_0$ such that $T$ is $T_0$ bounded.
+which is the unique function type $T$ such that $S$ is $T$ bounded.
 
 
 \subsection{Class Building Types}
@@ -23070,7 +23080,7 @@ \subsection{Interface Types}
 are interface types,
 and so are
 \code{Future<$T$>}, \code{Stream<$T$>}, \code{Iterable<$T$>},
-\code{List<$T$>}, \code{Map<$S$,\,\,$T$}, and \code{Set<$T$>},
+\code{List<$T$>}, \code{Map<$S$,\,\,$T$>}, and \code{Set<$T$>},
 for any $S$ and $T$.%
 }
 
@@ -23196,8 +23206,13 @@ \subsection{Type Null}
 \code{Null} is a subtype of all types of the form \code{$T$?},
 and of all types $S$ such that \futureOrBase{S} is
 a top type or a type of the form \code{$T$?}.
-The only non-trivial subtypes of \code{Null} are
-\code{Never} and subtypes of \code{Never}
+The only subtypes of \code{Null} are
+other types that contain the null object and no other objects,
+e.g., \code{Null?},
+the empty type,
+i.e., \code{Never} and subtypes of \code{Never},
+and types that could be either,
+e.g., a type variable with bound \code{Null}
 (\ref{subtypeRules}).%
 }
 
@@ -23723,22 +23738,10 @@ \subsection{Type Void}
 \commentary{%
 The type \VOID{} is a top type
 (\ref{superBoundedTypes}),
-so \VOID{} and \code{Object} are subtypes of each other
+so \VOID{} and \code{Object?} are subtypes of each other
 (\ref{subtypes}),
 which also implies that any object can be
-the value of an expression of type \VOID.
-%
-Consequently, any instance of type \code{Type} which reifies the type \VOID{}
-must compare equal (according to the \lit{==} operator \ref{equality})
-to any instance of \code{Type} which reifies the type \code{Object}
-(\ref{dynamicTypeSystem}).
-It is not guaranteed that \code{identical(\VOID, Object)} evaluates to
-the \TRUE{} object.
-In fact, it is not recommended that implementations strive to achieve this,
-because it may be more important to ensure that diagnostic messages
-(including stack traces and dynamic error messages)
-preserve enough information to use the word `void' when referring to types
-which are specified as such in source code.%
+the value of an expression of type \VOID.%
 }
 
 \LMHash{}%
@@ -23876,7 +23879,7 @@ \subsection{Type Void}
 }
 
 \begin{dartCode}
-\FOR{} (Object x in <\VOID>[]) \{\} // \comment{Error.}
+\FOR{} (Object? x in <\VOID>[]) \{\} // \comment{Error.}
 \AWAIT{} \FOR{} (int x \IN{} new Stream<\VOID{}>.empty()) \{\} // \comment{Error.}
 \FOR{} (\VOID{} x \IN{} <\VOID{}>[]) \{\ldots\} // \comment{OK.}
 \FOR (\VAR{} x \IN{} <\VOID{}>[]) \{\ldots\} // \comment{OK, type of x inferred.}
@@ -24185,9 +24188,11 @@ \subsection{Definite Assignment}
 (\commentary{%
 e.g., as an expression, or as the left hand side of an assignment%
 }),
-the variable has a status as being
-\IndexCustom{definitely assigned}{local variable!definitely assigned} or
-\IndexCustom{definitely unassigned}{local variable!definitely unassigned}.
+the variable can be
+\IndexCustom{definitely assigned}{local variable!definitely assigned},
+and it can be
+\IndexCustom{definitely unassigned}{local variable!definitely unassigned},
+and it can be neither.
 
 \commentary{%
 The precise flow analysis which determines this status at each location
@@ -24440,15 +24445,16 @@ \subsection{Type Promotion}
 
 %% 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 I've specified the latter. This is also more consistent
-%% with the approach used with `==`.
+%% `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 type $T$ at $\ell$
+where $v$ has static type $T?$ at $\ell$
 promotes the type of $v$
-to \NonNullType{$T$} in the \TRUE{} continuation,
+to $T$ in the \TRUE{} continuation,
 and to \code{Null} in the \FALSE{} continuation.
 
 \commentary{%