From 3711897b85a759321fa4ab7d9f150fea0014eb04 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Wed, 25 May 2022 19:09:25 +0200 Subject: [PATCH] WIP --- specification/dart.sty | 10 +-- specification/dartLangSpec.tex | 122 +++++++++++++++++---------------- 2 files changed, 69 insertions(+), 63 deletions(-) diff --git a/specification/dart.sty b/specification/dart.sty index cfa1af1e1d..d4763f14c2 100644 --- a/specification/dart.sty +++ b/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}} diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index d3bc51dabd..fd4a2784e2 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -20710,9 +20710,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} @@ -21323,7 +21320,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. @@ -21345,7 +21343,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}. @@ -21712,10 +21711,11 @@ \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} @@ -21723,10 +21723,11 @@ \subsection{Type Normalization} 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{% @@ -22064,8 +22065,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: @@ -22084,7 +22085,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). @@ -22263,22 +22265,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.% @@ -22336,8 +22341,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)}{% @@ -22700,7 +22708,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$. @@ -22933,7 +22941,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 @@ -22948,7 +22956,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$, @@ -23004,15 +23012,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 @@ -23026,11 +23036,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} @@ -23091,7 +23101,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$.% } @@ -23217,8 +23227,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}).% } @@ -23744,22 +23759,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{}% @@ -23897,7 +23900,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.} @@ -24206,9 +24209,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 @@ -24461,15 +24466,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{%