Specify null safety: Sections 'Variables' and 'Local Variable Declarations' (#2052)

Integrate the null-safety aware sections about variables and local variable declarations in the the language specification.

Also updates the terminology to talk about 'static X' meaning a member declaration that includes the keyword `static` (or a member whose declaration includes `static`). This means that we avoid having the extremely confusing phrase 'static variable' (meaning a top-level variable or a variable whose declaration includes `static`). The new meaning of 'static variable' is simply a variable whose declaration includes `static`. Eliminated the single occurrence of 'static function' (now using 'static member', which is well defined).

Similarly, updates the terminology to avoid the words 'mutable' and 'immutable' (about variables). The reason for this is that the concept of being immutable is confusing now that we have `late final v;`: That declaration induces a setter, but it is semantically immutable (because it may be initialized, but it will never update the initial value to a different value).

Author: eernstg

specification/dart.sty

@@ -68,6 +68,9 @@
 \def\WITH{\keyword{with}}
 \def\YIELD{\keyword{yield}}
 
+% Used for inline code snippets.
+\newcommand{\code}[1]{\texttt{#1}}
+
 % Used to specify syntactic sugar.
 \def\LET{\keyword{let}}
 \newcommand{\Let}[3]{\code{\LET\,\,{#1}\,=\,{#2}\ \IN\ {#3}}}
@@ -78,8 +81,8 @@
 \newcommand{\LetMany}[5]{%
   \code{\LET\,\,{#1}\,=\,{#2},\ $\cdots$,\ {#3}\,=\,{#4}\ \IN\ {#5}}}
 
-% Used for inline code snippets.
-\def\code#1{\texttt{#1}}
+% Used for inline meta-code snippets
+\newcommand{\metaCode}[1]{{\color{metaColor}\texttt{#1}}}
 
 % `call` has no special lexical status, so we just use \code{}.
 \def\CALL{\code{call}}
@@ -112,6 +115,7 @@
 \definecolor{normativeColor}{rgb}{0,0,0}
 \definecolor{commentaryColor}{rgb}{0.5,0.5,0.5}
 \definecolor{rationaleColor}{rgb}{0.5,0.5,0.5}
+\definecolor{metaColor}{rgb}{0,0,1}
 
 % Environments for different kinds of text.
 \newenvironment{Q}[1]{{\bf{}Upcoming: {#1}}}{}
@@ -132,22 +136,35 @@
 \newcommand{\Case}[1]{\textbf{Case }$\langle\hspace{0.1em}${#1}$\hspace{0.1em}\rangle$\textbf{.}}
 \newcommand{\EndCase}{\mbox{}\hfill$\scriptscriptstyle\Box$\xspace}
 
-\newenvironment{dartCode}[1][!ht] {%
+% Used for source code examples.
+\newenvironment{dartCode}[1][!ht]{%
   \def\@programcr{\@addfield\strut}%
   \let\\=\@programcr%
   \relax\@vobeyspaces\obeylines%
   \ttfamily\color{commentaryColor}%
   \vspace{1em}%
 }{\normalcolor\vspace{1em}}
 
-\newenvironment{normativeDartCode}[1][!ht] {%
+% Used for normative code snippets (mainly desugaring).
+\newenvironment{normativeDartCode}[1][!ht]{%
   \def\@programcr{\@addfield\strut}%
   \let\\=\@programcr%
   \relax\@vobeyspaces\obeylines%
   \ttfamily\color{normativeColor}%
   \vspace{1em}%
 }{\normalcolor\vspace{1em}}
 
+% Used for meta-level code, such as the code transformations used
+% to specify the semantics of "null shorting" in expressions like
+% `a?.b.c`.
+\newenvironment{metaLevelCode}[1][!ht]{%
+  \def\@programcr{\@addfield\strut}%
+  \let\\=\@programcr%
+  \relax\@vobeyspaces\obeylines%
+  \ttfamily\color{metaColor}%
+  \vspace{1em}%
+}{\normalcolor\vspace{1em}}
+
 % Used for comments in a code context.
 \def\comment#1{\textsf{#1}}
 
@@ -157,7 +174,7 @@
 
 % Used for defining occurrence of phrase, with customized index entry.
 \newcommand{\IndexCustom}[2]{%
-  \leavevmode\marginpar{\ensuremath{\diamond}}\emph{#1}\index{#2}}
+  \leavevmode\marginpar{\ensuremath{_{^\vartriangle}}}\emph{#1}\index{#2}}
 
 % Used for the defining occurrence of a local symbol.
 \newcommand{\DefineSymbol}[1]{%
@@ -178,7 +195,11 @@
 
 % Same appearance, but not adding an entry to the index.
 \newcommand{\NoIndex}[1]{%
-  \leavevmode\marginpar{\quad\ensuremath{\diamond}}\emph{#1}}
+  \leavevmode\marginpar{\ensuremath{_{^\vartriangle}}}\emph{#1}}
+
+% Mark a compile-time error in the margin.
+\newcommand{\Error}[1]{%
+  \leavevmode\marginpar{\ensuremath{_{^\ominus}}}{#1}}
 
 % Used to specify comma separated lists of similar symbols.
 \newcommand{\List}[3]{\ensuremath{{#1}_{#2},\,\ldots,\ {#1}_{#3}}}
@@ -190,6 +211,39 @@
 \newcommand{\PairList}[4]{\ensuremath{%
   {#1}_{#3}\ {#2}_{#3},\,\ldots,\ {#1}_{#4}\ {#2}_{#4}}}
 
+% A sequence of labeled arguments with the same label and expression,
+% only differing by subscript.
+% Parameters: Argument label, argument expression, start index,
+% end index.
+%
+% For example, \NamedArgumentList{n}{e}{1}{k} yields approximately
+% "n1: e1, n2: e2, ... nk: ek".
+\newcommand{\NamedArgumentList}[4]{\PairList{#1}{\!\!:\,\,{#2}}{#3}{#4}}
+
+% A sequence of unlabeled and labeled arguments with the same expression and
+% (for all labeled arguments) the same label, only differing by subscript.
+% Parameters: Argument name, number of positional arguments, labeled parameter
+% label, number of labeled arguments.
+%
+% For example, \ArgumentList{a}{n}{x}{k} yields approximately
+% "a1, .. an, xn+1: an+1, .. xn+k: an+k".
+\newcommand{\ArgumentList}[4]{%
+  \List{#1}{1}{#2},\ \NamedArgumentList{#3}{#1}{{#2}+1}{{#2}+{#4}}}
+
+% Used to specify a standard argument list, that is, an argument list
+% which uses the symbols that we prefer to use for that purpose
+% whenever possible.
+%
+% Approximately "a1 .. an, xn+1: an+1 .. xn+k: an+k".
+\newcommand{\ArgumentListStd}{\ArgumentList{a}{n}{x}{k}}
+
+% Used to specify a standard type argument list, that is, a type
+% argument list which uses the symbols we prefer to use for that
+% purpose whenever possible.
+%
+% Approximately "A1 .. Ar".
+\newcommand{\TypeArgumentListStd}{\List{A}{1}{r}}
+
 % Used to specify a list of tuples of the form $(K_j, V_j)$ which are
 % used with collection literals.
 \newcommand{\KeyValueTypeList}[4]{\ensuremath{%
@@ -224,7 +278,11 @@
 \newcommand{\TypeParametersNoBounds}[2]{\ensuremath{%
   {#1}_1\,\EXTENDS\,\ldots,\ \ldots,\ {#1}_{#2}\,\EXTENDS\,\ldots}}
 
-% For consistency, we may as well use this whenever possible.
+% Used to specify a standard type parameter list, that is, a type
+% parameter declaration list which uses the symbols we prefer to use
+% for that purpose whenever possible.
+%
+% Approximately "X1 extends B1, .. Xs extends Bs".
 \newcommand{\TypeParametersStd}{\TypeParameters{X}{B}{s}}
 
 % Used to specify comma separated lists of pairs of symbols
@@ -256,78 +314,140 @@
 
 % Used to specify function type parameter lists with positional optionals.
 % Arguments: Parameter type, number of required parameters,
-% number of optional parameters.
-\newcommand{\FunctionTypePositionalArguments}[3]{%
+%   number of optional parameters.
+%
+% For example, \FunctionTypePositionalParameters{T}{n}{k} yields
+% approximately "T1, .. Tn, [Tn+1, .. Tn+k]".
+\newcommand{\FunctionTypePositionalParameters}[3]{%
   \List{#1}{1}{#2},\ [\List{#1}{{#2}+1}{{#2}+{#3}}]}
 
-\newcommand{\FunctionTypePositionalArgumentsStd}{%
-  \FunctionTypePositionalArguments{T}{n}{k}}
+% Used to specify a standard positional function type, that is, a function
+% type with positional optional parameters which uses the symbols we prefer
+% to use for that purpose whenever possible.
+%
+% Approximately "T1, .. Tn, [Tn+1, .. Tn+k]".
+\newcommand{\FunctionTypePositionalParametersStd}{%
+  \FunctionTypePositionalParameters{T}{n}{k}}
+
+% Used to specify function type parameter lists with named optionals.
+% Arguments: Parameter type, number of required parameters,
+%   name of optional parameters, number of optional parameters.
+%
+% For example \FunctionTypeNamedParameters{T}{n}{x}{k}{r} yields approximately
+% "T1, .. Tn, {rn+1 Tn+1 xn+1, .. rn+k Tn+k xn+k}".
+\newcommand{\FunctionTypeNamedParameters}[5]{%
+  \List{#1}{1}{#2},\ \{\TripleList{#5}{#1}{#3}{{#2}+1}{{#2}+{#4}}\}}
+  
+% Variant of \FunctionTypeNamedParameters that uses the standard symbols,
+% that is, a list of function type parameter declarations with named
+% parameters which uses the symbols that we prefer to use for that purpose
+% whenever possible.
+%
+% Approximately "T1, .. Tn, {rn+1 Tn+1 xn+1, .. rn+k Tn+k xn+k}".
+\newcommand{\FunctionTypeNamedParametersStd}{%
+  \FunctionTypeNamedParameters{T}{n}{x}{k}{r}}
 
 % Used to specify function types with positional optionals:
 % Arguments: Return type, spacer, type parameter name, bound name,
 %   number of type parameters, parameter type, number of required parameters,
 %   number of optional parameters.
+%
+% For example, \FunctionTypePositional{R}{ }{X}{B}{s}{T}{n}{k} yields
+% approximately
+% "R Function<X1 extends B1, .. Xs extends Bs>(T1, .. Tn, [Tn+1, .. Tn+k])".
 \newcommand{\FunctionTypePositional}[8]{%
   \FunctionType{#1}{#2}{#3}{#4}{#5}{%
-    \FunctionTypePositionalArguments{#6}{#7}{#8}}}
+    \FunctionTypePositionalParameters{#6}{#7}{#8}}}
 
 % Same as \FunctionTypePositional except suitable for inline usage,
 % hence omitting the spacer argument.
 \newcommand{\RawFunctionTypePositional}[7]{%
   \RawFunctionType{#1}{#2}{#3}{#4}{%
-    \FunctionTypePositionalArguments{#5}{#6}{#7}}}
+    \FunctionTypePositionalParameters{#5}{#6}{#7}}}
+
+% A variant of \FunctionTypePositional that uses the standard symbols,
+% that is, a function type with positional optional parameters which
+% uses the symbols that we prefer to use for that purpose whenever
+% possible.
+%
+% For example, \FunctionTypePositionalStd{R} yields approximately
+% "R Function<X1 extends B1, .. Xs extends Bs>(T1, T2, .. Tn, [Tn+1 .. Tn+k])".
+\newcommand{\FunctionTypePositionalStd}[1]{%
+  \FunctionTypePositional{#1}{ }{X}{B}{s}{T}{n}{k}}
 
-% Used to specify function type parameter lists with named optionals.
-% Arguments: Parameter type, number of required parameters,
-% name of optional parameters, number of optional parameters.
-\newcommand{\FunctionTypeNamedArguments}[4]{%
-  \List{#1}{1}{#2},\ \{\PairList{#1}{#3}{{#2}+1}{{#2}+{#4}}\}}
+% Same as \FunctionTypePositionalStd except suitable for inline usage,
+% hence omitting the spacer argument.
+\newcommand{\RawFunctionTypePositionalStd}[1]{%
+  \RawFunctionTypePositional{#1}{X}{B}{s}{T}{n}{k}}
 
-\newcommand{\FunctionTypeNamedArgumentsStd}{%
-  \FunctionTypeNamedArguments{T}{n}{x}{k}}
+% Same as \FunctionTypePositionalStd except that it includes a newline, hence
+% suitable for function types that are too long to fit in one line.
+\newcommand{\FunctionTypePositionalStdCr}[1]{%
+  \FunctionTypePositional{#1}{\\}{X}{B}{s}{T}{n}{k}}
 
 % Used to specify function types with named parameters:
 % 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.
+% The name of the `required` symbol is always `r` (because we can't have
+% 10 arguments in a LaTeX command, and `r` is always OK in practice).
+%
+% For example, \FunctionTypeNamed{R}{ }{X}{B}{s}{T}{n}{x}{k} yields
+% approximately "R Function<X1 extends B1, .. Xs extends Bs>(
+%     T1, T2, .. Tn, {rn+1 Tn+1 xn+1, .. rn+k Tn+k xn+k])".
 \newcommand{\FunctionTypeNamed}[9]{%
-  \FunctionType{#1}{#2}{#3}{#4}{#5}{%
-    \FunctionTypeNamedArguments{#6}{#7}{#8}{#9}}}
+  \FunctionType{#1}{#2}{#3}{#4}{#5}{\\
+    \mbox{}\qquad\FunctionTypeNamedParameters{#6}{#7}{#8}{#9}{r}}}
 
-% Same as \FunctionType except suitable for inline usage, hence omitting
+% Same as \FunctionTypeNamed except suitable for inline usage, hence omitting
 % the spacer argument.
 \newcommand{\RawFunctionTypeNamed}[8]{%
   \RawFunctionType{#1}{#2}{#3}{#4}{%
-    \FunctionTypeNamedArguments{#5}{#6}{#7}{#8}}}
+    \FunctionTypeNamedParameters{#5}{#6}{#7}{#8}{r}}}
+
+% A variant of \FunctionTypeNamed that uses the standard symbols,
+% that is, a function type with positional optional parameters which
+% uses the symbols that we prefer to use for that purpose whenever
+% possible.
+%
+% For example, \FunctionTypeNamedStd{R} yields approximately
+% "R Function<X1 extends B1, .. Xs extends Bs>(
+%     T1, T2, .. Tn, {rn+1 Tn+1 xn+1, .. rn+k Tn+k xn+k})".
+\newcommand{\FunctionTypeNamedStd}[1]{%
+  \FunctionTypeNamed{#1}{ }{X}{B}{s}{T}{n}{x}{k}}
+
+% Same as \FunctionTypeNamedStd except suitable for inline usage, hence
+% omitting the spacer argument.
+\newcommand{\RawFunctionTypeNamedStd}[1]{%
+  \RawFunctionTypeNamed{#1}{X}{B}{s}{T}{n}{x}{k}{r}}
+
+% Same as \FunctionTypeNamedStd except that it includes a newline, hence
+% suitable for function types that are too long to fit in one line.
+\newcommand{\FunctionTypeNamedStdCr}[1]{%
+  \FunctionTypeNamed{#1}{\\}{X}{B}{s}{T}{n}{x}{k}}
 
 % Used to specify function types with no optional parameters:
 % Arguments: Return type, spacer, type parameter name, bound name,
 %   number of type parameters, parameter type,
 %   number of parameters (all required).
+%
+% For example, \FunctionTypeAllRequired{R}{ }{X}{B}{s}{T}{n} yields
+% approximately "R Function<X1 extends B1, .. Xs extends Bs>(T1, T2, .. Tn)".
 \newcommand{\FunctionTypeAllRequired}[7]{%
   \FunctionType{#1}{#2}{#3}{#4}{#5}{\List{#6}{1}{#7}}}
 
-\newcommand{\FunctionTypePositionalStd}[1]{%
-  \FunctionTypePositional{#1}{ }{X}{B}{s}{T}{n}{k}}
-
-\newcommand{\RawFunctionTypePositionalStd}[1]{%
-  \RawFunctionTypePositional{#1}{X}{B}{s}{T}{n}{k}}
-
-\newcommand{\FunctionTypeNamedStd}[1]{%
-  \FunctionTypeNamed{#1}{ }{X}{B}{s}{T}{n}{x}{k}}
-
-\newcommand{\RawFunctionTypeNamedStd}[1]{%
-  \RawFunctionTypeNamed{#1}{X}{B}{s}{T}{n}{x}{k}}
-
+% A variant of \FunctionTypeAllRequired that uses the standard symbols,
+% that is, a function type with positional optional parameters which
+% uses the symbols that we prefer to use for that purpose whenever
+% possible.
+%
+% For example, \FunctionTypeAllRequiredStd{R} yields approximately
+% "R Function<X1 extends B1, .. Xs extends Bs>(T1, T2, .. Tn)".
 \newcommand{\FunctionTypeAllRequiredStd}[1]{%
   \FunctionTypeAllRequired{#1}{ }{X}{B}{s}{T}{n}}
 
-\newcommand{\FunctionTypePositionalStdCr}[1]{%
-  \FunctionTypePositional{#1}{\\}{X}{B}{s}{T}{n}{k}}
-
-\newcommand{\FunctionTypeNamedStdCr}[1]{%
-  \FunctionTypeNamed{#1}{\\}{X}{B}{s}{T}{n}{x}{k}}
-
+% Same as \FunctionTypeAllRequiredStd except that it includes a newline, hence
+% suitable for function types that are too long to fit in one line.
 \newcommand{\FunctionTypeAllRequiredStdCr}[1]{%
   \FunctionTypeAllRequired{#1}{\\}{X}{B}{s}{T}{n}}
 
@@ -342,13 +462,13 @@
 
 % Judgment expressing that a subtype relation exists.
 \newcommand{\Subtype}[3]{\ensuremath{{#1}\vdash{#2}\,<:\,{#3}}}
-\newcommand{\SubtypeStd}[2]{\Subtype{\Gamma}{#1}{#2}}
+\newcommand{\SubtypeStd}[2]{\Subtype{\Delta}{#1}{#2}}
 % Subtype judgment where the environment is omitted (NE: "no environment").
 \newcommand{\SubtypeNE}[2]{\ensuremath{{#1}\,<:\,{#2}}}
 
 % Judgment expressing that a supertype relation exists.
 \newcommand{\Supertype}[3]{\ensuremath{{#1}\vdash{#2}\,:>\,{#3}}}
-\newcommand{\SupertypeStd}[2]{\Supertype{\Gamma}{#1}{#2}}
+\newcommand{\SupertypeStd}[2]{\Supertype{\Delta}{#1}{#2}}
 
 % Judgment expressing that an assignability relation exists.
 \newcommand{\AssignableRelationSymbol}{\ensuremath{\Longleftrightarrow}}
@@ -394,6 +514,56 @@
   \ensuremath{{#2}}%
 }
 
+\newcommand{\FlattenName}{\metavar{flatten}}
+\newcommand{\Flatten}[1]{\ensuremath{\FlattenName(\code{#1})}}
+
+\newcommand{\NominalTypeDepthName}{\metavar{nominalTypeDepth}}
+\newcommand{\NominalTypeDepth}[1]{%
+  \ensuremath{\NominalTypeDepthName(\code{#1})}}
+
+\newcommand{\TopMergeTypeName}{\metavar{topMergeType}}
+\newcommand{\TopMergeType}[2]{%
+  \ensuremath{\TopMergeTypeName(\code{{#1},\,\,{#2}})}}
+
+\newcommand{\NonNullTypeName}{\metavar{nonNullType}}
+\newcommand{\NonNullType}[1]{\ensuremath{\NonNullTypeName(\code{#1})}}
+
+\newcommand{\IsTopTypeName}{\metavar{isTopType}}
+\newcommand{\IsTopType}[1]{\ensuremath{\IsTopTypeName(\code{#1})}}
+
+\newcommand{\IsObjectTypeName}{\metavar{isObjectType}}
+\newcommand{\IsObjectType}[1]{\ensuremath{\IsObjectTypeName(\code{#1})}}
+
+\newcommand{\IsBottomTypeName}{\metavar{isBottomType}}
+\newcommand{\IsBottomType}[1]{\ensuremath{\IsBottomTypeName(\code{#1})}}
+
+\newcommand{\IsNullTypeName}{\metavar{isNullType}}
+\newcommand{\IsNullType}[1]{\ensuremath{\IsNullTypeName(\code{#1})}}
+
+\newcommand{\IsMoreTopTypeName}{\metavar{isMoreTopType}}
+\newcommand{\IsMoreTopType}[2]{%
+  \ensuremath{\IsMoreTopTypeName(\code{{#1},\,\,{#2}})}}
+
+\newcommand{\IsMoreBottomTypeName}{\metavar{isMoreBottomType}}
+\newcommand{\IsMoreBottomType}[2]{%
+  \ensuremath{\IsMoreBottomTypeName(\code{{#1},\,\,{#2}})}}
+
+\newcommand{\NormalizedTypeOfName}{\metavar{normalizedType}}
+\newcommand{\NormalizedTypeOf}[1]{%
+  \ensuremath{\NormalizedTypeOfName(\code{#1})}}
+
+\newcommand{\FutureValueTypeOfName}{\metavar{futureValueType}}
+\newcommand{\FutureValueTypeOf}[1]{%
+  \ensuremath{\FutureValueTypeOfName(\code{#1})}}
+
+\newcommand{\UpperBoundTypeName}{\metavar{standardUpperBound}}
+\newcommand{\UpperBoundType}[2]{%
+  \ensuremath{\UpperBoundTypeName(\code{{#1},\,\,{#2}})}}
+
+\newcommand{\LowerBoundTypeName}{\metavar{standardLowerBound}}
+\newcommand{\LowerBoundType}[2]{%
+  \ensuremath{\LowerBoundTypeName(\code{{#1},\,\,{#2}})}}
+
 % ----------------------------------------------------------------------
 % Support for hash valued Location Markers