Skip to content

Commit

Permalink
Specify null safety: Sections 'Variables' and 'Local Variable Declara…
Browse files Browse the repository at this point in the history 
…tions' (#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).
  • Loading branch information
@eernstg
eernstg committed Jul 19, 2023
1 parent 35c9062 commit af27cfb
Show file tree
Hide file tree
Showing 2 changed files with 896 additions and 313 deletions.
258 changes: 214 additions & 44 deletions specification/dart.sty
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}}}
Expand All @@ -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}}
Expand Down Expand Up @@ -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}}}{}
Expand All @@ -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}}

Expand All @@ -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]{%
Expand All @@ -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}}}
Expand All @@ -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{%
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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}}

Expand All @@ -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}}
Expand Down Expand Up @@ -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

Expand Down

0 comments on commit af27cfb

Please sign in to comment.