Change in dart/sdk[master]: Transferred signature specificity and least upper bounds from 81263
0 views
Skip to first unread message
Erik Ernst (Gerrit)
Nov 20, 2018, 12:26:54 PM11/20/18
to rev...@dartlang.org, Leaf Petersen, Lasse R.H. Nielsen
This CL contains parts that were moved out of CL 81263: New section 'Signature Specificity of Types', and the updates performed in section 'Least Upper Bounds'.
To view, visit change 84908. To unsubscribe, or for help writing mail filters, visit settings.
Erik Ernst (Gerrit)
Nov 20, 2018, 12:26:55 PM11/20/18
to Leaf Petersen, rev...@dartlang.org, Lasse R.H. Nielsen
Erik Ernst would like Leaf Petersen to review this change.
Transferred signature specificity and least upper bounds from 81263
Change-Id: If83dba2cb500979f9a1c7589b5aeceed00c6f061
---
M docs/language/dart.sty
M docs/language/dartLangSpec.tex
M docs/language/informal/extreme-upper-lower-bounds.md
3 files changed, 379 insertions(+), 42 deletions(-)
diff --git a/docs/language/dart.sty b/docs/language/dart.sty
index 0aede6b..eebc0a1 100644
--- a/docs/language/dart.sty
+++ b/docs/language/dart.sty
@@ -84,6 +84,11 @@
\newcommand{\argumentList}[1]{\metavar{{#1}s}}
\newcommand{\parameterList}[1]{\metavar{{#1}s}}
+% Colors used for for different kinds of text.
+\definecolor{normativeColor}{rgb}{0,0,0}
+\definecolor{commentaryColor}{rgb}{0.6,0.6,0.6}
+\definecolor{rationaleColor}{rgb}{0.6,0.6,0.6}
+
\newenvironment{Q}[1]{{\bf #1}}{}
\newenvironment{rationale}[1]{{\it #1}}{}
\newenvironment{commentary}[1]{{\sf #1}}{}
@@ -100,9 +105,17 @@
\def\@programcr{\@addfield\strut}%
\let\\=\@programcr%
\relax\@vobeyspaces\obeylines%
- \ttfamily%
+ \ttfamily\color{commentaryColor}%
\vspace{1em}
-}{\vspace{1em}}
+}{\normalcolor\vspace{1em}}
+
+\newenvironment{normativeDartCode}[1][!ht] {
+ \def\@programcr{\@addfield\strut}%
+ \let\\=\@programcr%
+ \relax\@vobeyspaces\obeylines%
+ \ttfamily\color{normativeColor}%
+ \vspace{1em}
+}{\normalcolor\vspace{1em}}
% Used for comments in a code context.
\def\comment#1{\textsf{#1}}
@@ -121,6 +134,103 @@
\newcommand{\NoIndex}[1]{
\leavevmode\marginpar{\ensuremath{\diamond}}\emph{#1}}
+% Used to specify comma separated lists of similar symbols.
+\newcommand{\List}[3]{\ensuremath{{#1}_{#2},\,\ldots,\ {#1}_{#3}}}
+
+% Used to specify comma separated lists of pairs of similar symbols,
+% as needed, e.g., for declarations of formal parameters.
+% Parameters: Name of first part of pair, name of second part,
+% index at start, index at end.
+\newcommand{\PairList}[4]{\ensuremath{%
+ {#1}_{#3}\ {#2}_{#3},\,\ldots,\ {#1}_{#4}\ {#2}_{#4}}}
+
+% Used to specify comma separated lists of triples of similar symbols,
+% as needed, e.g., for declarations of formal parameters with defaults.
+% Parameters: Name of first part of triple, name of second part,
+% name of third part, index at start, index at end.
+\newcommand{\TripleList}[5]{\ensuremath{%
+ {#1}_{#4}\ {#2}_{#4}\ {#3}_{#4},\,\ldots,\ {#1}_{#5}\ {#2}_{#5}\ {#3}_{#5}}}
+
+% Used to abbreviate \EXTENDS{} in function types.
+\newcommand{\FunctionTypeExtends}{\ensuremath{\triangleleft}}
+
+% Used to specify comma separated lists of pairs of symbols
+% separated by \EXTENDS{}, as needed for type parameter declarations.
+% Parameters: Type parameter name, bound name, number of type parameters.
+\newcommand{\TypeParameters}[3]{\ensuremath{%
+ {#1}_1\,\EXTENDS\,{#2}_1,\,\ldots,\ %
+ {#1}_{#3}\,\EXTENDS\,{#2}_{#3}}}
+
+% For consistency, we may as well use this whenever possible.
+\newcommand{\TypeParametersStd}{\TypeParameters{X}{B}{s}}
+
+% Used to specify comma separated lists of pairs of symbols
+% separated by \EXTENDS{}, as needed for type parameter declarations.
+% Parameters: Type parameter name, bound name, number of type parameters.
+\newcommand{\FTTypeParameters}[3]{\ensuremath{%
+ {#1}_1\FunctionTypeExtends{#2}_1,\,\ldots,\ %
+ {#1}_{#3}\FunctionTypeExtends{#2}_{#3}}}
+
+% Used to specify function types: Same syntax as in source.
+% Arguments: Return type, formal parameter declarations.
+\newcommand{\FunctionTypeSimple}[2]{\code{\ensuremath{#1}\ \FUNCTION({#2})}}
+
+% Used to specify function types: Same syntax as in source.
+% Arguments: Return type, spacer, type parameter name, bound name,
+% number of type parameters, formal parameter declarations.
+\newcommand{\FunctionType}[6]{\leavevmode\par\noindent\code{%
+ \ensuremath{#1}{#2}\FUNCTION<\FTTypeParameters{#3}{#4}{#5}>({#6})}}
+
+% 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.
+\newcommand{\FunctionTypePositional}[8]{%
+ \FunctionType{#1}{#2}{#3}{#4}{#5}{\List{#6}{1}{#7},\ %
+ [\List{#6}{{#7}+1}{{#7}+{#8}}]}}
+
+% 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.
+\newcommand{\FunctionTypeNamed}[9]{%
+ \FunctionType{#1}{#2}{#3}{#4}{#5}{\List{#6}{1}{#7},\ %
+ \{\PairList{#6}{#8}{{#7}+1}{{#7}+{#9}}\}}}
+
+% 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).
+\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{\FunctionTypeNamedStd}[1]{%
+ \FunctionTypeNamed{#1}{ }{X}{B}{s}{T}{n}{x}{k}}
+
+\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}}
+
+\newcommand{\FunctionTypeAllRequiredStdCr}[1]{%
+ \FunctionTypeAllRequired{#1}{\\}{X}{B}{s}{T}{n}}
+
+\newcommand{\MoreSignatureSpecificSymbol}{\ensuremath{\preceq}}
+\newcommand{\NotMoreSignatureSpecificSymbol}{\ensuremath{\not\preceq}}
+\newcommand{\LessSignatureSpecificSymbol}{\ensuremath{\succeq}}
+
+\newcommand{\MoreSignatureSpecific}[2]{%
+ \ensuremath{{#1}\MoreSignatureSpecificSymbol{#2}}}
+\newcommand{\NotMoreSignatureSpecific}[2]{%
+ \ensuremath{{#1}\NotMoreSignatureSpecificSymbol{#2}}}
+
% ----------------------------------------------------------------------
% Support for hash valued Location Markers
diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex
index ecc249e..184ee9f 100644
--- a/docs/language/dartLangSpec.tex
+++ b/docs/language/dartLangSpec.tex
@@ -7,6 +7,7 @@
\usepackage{hyperref}
\usepackage{lmodern}
\usepackage[T1]{fontenc}
+\usepackage[fleqn]{amsmath}
\usepackage{makeidx}
\makeindex
\title{Dart Programming Language Specification\\
@@ -3398,6 +3399,176 @@
The member that is inherited is $m_x$, if it exists.
+\subsubsection{Signature Specificity of Types}
+\LMLabel{signatureSpecificityOfTypes}
+
+\LMHash{}%
+This section specifies a partial order on types that is needed
+in order to disambiguate the choice between several types that
+only differ by being or containing different top types
+(\ref{superBoundedTypes}).
+
+\commentary{
+For instance, it is needed when a conditional expression
+(\ref{conditional})
+contains a second and third operand that only differ
+in the choice of different top types at certain positions.
+It should be noted that it is important to make this choice
+in order to have a well-defined static analysis of programs,
+but every one of these choices is sound.
+This means that there are no soundness considerations in the
+design of this partial order, it just needs to be useful
+from a software engineering perspective.
+}
+
+\LMHash{}%
+We specify what it means for a type $S$ to be more
+\IndexCustom{signature specific}{signature specificity}
+than another type $T$, denoted by `\MoreSignatureSpecificSymbol'.
+This relation is a partial order which refines the subtype relation:
+Whenever \MoreSignatureSpecific{S}{T} holds, $S <: T$ also holds.
+
+% We refine the subtype relation because we wish to avoid the confusion
+% associated with the usage of different terms denoting the same type. For
+% instance, we do _not_ consider the type FutureOr<T> to denote a union
+% type that would be subject to normalization, we actually consider
+% `FutureOr<void>` to be different from `FutureOr<Future<void>>`, etc.
+
+\rationale{
+There are cases where we have both $S <: T$ and $T <: S$,
+even though we should not consider $S$ and $T$ to be the same type.
+}
+
+\commentary{
+In particular, consider the case where an expression $e_1$
+has static type \code{Object}, $e_2$ has static type \DYNAMIC{},
+and $b$ has static type \code{bool}.
+In that case,
+\code{($b$ ? $e_1$ : $e_2$).notAMemberOfObject()}
+would be a compile-time error
+if we consider the conditional expression to have type \code{Object},
+but it would be accepted silently (and may or may not fail at run time)
+if we consider it to have type \DYNAMIC{}.
+In other words, the two typings are subtypes of each other,
+but we cannot ignore the difference.
+}
+
+\rationale{
+So we introduce this notion of
+one type being more signature specific than another one,
+such that ambiguities in this area will have a
+simple and well-defined resolution.
+In the case where developers wish to resolve a particular
+ambiguity differently,
+they can use type casts, introduce declarations, or modify them.
+
+Note that the definition of being a correct override
+(\ref{correctMemberOverrides})
+relies on subtypes only,
+which makes it possible to use an overriding declaration to choose
+\emph{any} method signature among
+all those which are equivalent according to `$<:$',
+but distinct with respect to `\MoreSignatureSpecificSymbol'.
+}
+
+%% ----------------------------------------------------------------------
+%% TODO(eernst): The following will be made precise when subtyping.md
+%% is integrated.
+
+\LMHash{}%
+For the relation `\MoreSignatureSpecificSymbol',
+all the rules that pertain to `$<:$' apply as well,
+except for the following:
+\begin{align*}
+ &T <: \DYNAMIC{}%
+ \text{, for all $T$: No corresponding `\MoreSignatureSpecificSymbol' rule.}\\
+ &T <: \code{Object}%
+ \text{, for all $T$: No corresponding `\MoreSignatureSpecificSymbol' rule.}\\
+ &T <: \code{FutureOr<$T$>}%
+ \text{, for all $T$: No corresponding `\MoreSignatureSpecificSymbol' rule.}\\
+ &\code{FutureOr<$S$>} <: T%
+ \text{, for all $S$, $T$ where $S <: T$ and $\code{Future<$S$>} <: T$:}\\
+ &\qquad\text{No corresponding `\MoreSignatureSpecificSymbol' rule.}
+\end{align*}
+Instead, the following rules are added:
+\begin{align*}
+ &\MoreSignatureSpecific{T}{\DYNAMIC}\mbox{, for all }T \not= \VOID.\\
+ &\MoreSignatureSpecific{T}{\code{Object}}%
+ \mbox{, for all }T \not\in \{\VOID, \DYNAMIC\}.\\
+ &\MoreSignatureSpecific{\code{FutureOr<$S$>}}{T}%
+ \text{, for all $S$ and all $T \not= \code{Future<Null>}$ such that}\\
+ &\qquad\text{\MoreSignatureSpecific{S}{T} and
+ \MoreSignatureSpecific{\code{Future<$S$>}}{T}.}\\
+ &\MoreSignatureSpecific{T}{\code{FutureOr<$T$>}}%
+ \text{, for each $T$ which is not a top type.}\\
+\end{align*}
+
+% Note that we can show `Future<Null> == FutureOr<Null>` where `==` means that we
+% have both `<:` and `:>`, but this does not give rise to an infinite set of
+% equalities: If we admit general union types we can show the generalized result that
+%
+% FO^k<N> == F^k<N> | F^{k-1}<N> | ... | F<N> | N
+%
+% where `FO` means `FutureOr`, `F` means `Future`, and `N` means `Null`, but we cannot
+% express the type on the right hand side in Dart, so there is no need to disambiguate
+% `FO^k<N>` and any other syntactic type. So we need only cover the case `k = 1`, which
+% is what we do with the `FutureOr<S> < T` rule above.
+
+\commentary{
+This ensures that the set of top types is totally ordered by
+`\MoreSignatureSpecificSymbol',
+and it resolves the ambiguity around \code{FutureOr<Null>}.
+It also means that all the subtype relationships that do not involve a top type
+(\ref{superBoundedTypes})
+are carried over as `\MoreSignatureSpecificSymbol' relationships,
+and types involving both top types and non-top types are ordered accordingly.
+The following are examples of where the difference between `$<:$' and
+`\MoreSignatureSpecificSymbol'
+matters:
+}
+
+{ % Need to use the signature-specificity relation many times: abbreviate.
+ \def\L{\LessSignatureSpecificSymbol}
+ \def\M{\MoreSignatureSpecificSymbol}
+ \color{commentaryColor}
+ \begin{align*}
+ &\NotMoreSignatureSpecific{\VOID}{\code{FutureOr<$T$>}}\mbox{, for any top type $T$}\\
+ &\NotMoreSignatureSpecific{\DYNAMIC}{\code{FutureOr<$T$>}}\mbox{, for any top type $T$}\\
+ &\NotMoreSignatureSpecific{\code{Object}}{\code{FutureOr<$T$>}}\mbox{, for any top type $T$}\\
+ &\\
+ &\VOID\L\DYNAMIC\L\code{Object}\L\\
+ &\code{FutureOr<\VOID>}\L\code{FutureOr<\DYNAMIC>}\L\code{FutureOr<\code{Object}>}\L\\
+ &\code{FutureOr<FutureOr<\VOID>{}>}\L\\
+ &\code{FutureOr<FutureOr<\DYNAMIC>{}>}\L\\
+ &\code{FutureOr<FutureOr<\code{Object}>{}>}\L\ldots\\
+ &\\
+ &\code{FutureOr<$T$>}\L\code{Future<$T$>}\mbox{, for any type $T$}\\
+ &\code{FutureOr<$T$>}\L T\mbox{, for any non-top type $T$}\\
+ &\\
+ &\NotMoreSignatureSpecific{\code{FutureOr<Null>}}{\code{Future<Null>}}\text{, but}\\
+ &\MoreSignatureSpecific{\code{Future<Null>}}{\code{FutureOr<Null>}}\\
+ &\\
+ &\code{num}\M\code{Object}\M\DYNAMIC\M\VOID\\
+ &\code{List<num>}\M\code{List<Object>}\M%
+ \code{List<\DYNAMIC>}\M\code{List<\VOID>}\\
+ &\code{Object \FUNCTION(\DYNAMIC)}\M\code{\VOID{} \FUNCTION(\code{Object})}\\
+ &\ldots\text{ and similarly for all other ``normal'' types}
+ \end{align*}
+}
+
+\commentary{
+Returning to the software engineering perspective,
+the chosen ordering strives to consider more structure to be more specific
+(e.g., \MoreSignatureSpecific{\code{FutureOr<\VOID>}}{\VOID})
+and it considers a statically checked result to be more specific than
+a dynamically checked one
+(e.g., \MoreSignatureSpecific{\code{Object}}{\DYNAMIC}),
+and it considers a value which can be used as more specific than a value
+which should be discarded
+(e.g., \MoreSignatureSpecific{\DYNAMIC}{\VOID}).
+}
+
+
\section{Mixins}
\LMLabel{mixins}
@@ -12006,18 +12177,45 @@
\subsubsection{Least Upper Bounds}
\LMLabel{leastUpperBounds}
-% TODO(eernst): This section has been updated to take generic functions
-% into account, but no other changes have been performed. Hence, we still
-% need to update this section to use Dart 2 rules for LUB.
+\LMHash{}%
+This section defines the \Index{least upper bound} and
+the \Index{greatest lower bound} of two types.
+
+\LMHash{}%
+For any two top types $S$ and $T$
+(\ref{superBoundedTypes})
+where
+\MoreSignatureSpecific{S}{T}
+(\ref{signatureSpecificityOfTypes}),
+the least upper bound of $S$ and $T$ is $T$,
+and the greatest lower bound of $S$ and $T$ is $S$.
+\commentary{
+This is unambiguous and always defined because
+`\MoreSignatureSpecificSymbol'
+is a total order on top types.
+}
+%
+For any two types $S$ and $T$ where $S$ is not a top type and $T$ is a top type,
+the least upper bound of $S$ and $T$ is $T$,
+and the greatest lower bound of $S$ and $T$ is $S$.
+%
+The least upper bound of \code{Future<Null>} and \code{FutureOr<Null>} is
+\code{FutureOr<Null>},
+and their greatest lower bound is
+\code{Future<Null>}.
+%
+The least upper bound of $\bot$ and any type $T$ is $T$,
+and their greatest lower bound is $\bot$.
\LMHash{}%
% does this diverge in some cases?
-Given two interfaces $I$ and $J$,
+Given two interfaces $I$ and $J$ which are not top types
+(\ref{superBoundedTypes}),
let $S_I$ be the set of superinterfaces of $I$,
let $S_J$ be the set of superinterfaces of $J$
and let $S = (\{I\} \cup S_I) \cap (\{J\} \cup S_J)$.
Furthermore,
-we define $S_n = \{T | T \in S \wedge depth(T) = n\}$ for any finite $n$
+we define $S_n = \{T \;|\; T \in S \wedge depth(T) = n\}$ for any finite $n$
where $depth(T)$ is the number of steps in the longest inheritance path
from $T$ to \code{Object}.
%TODO(lrn): Specify that "inheritance path" is a path in the superinterface graph.
@@ -12026,11 +12224,15 @@
The least upper bound of $I$ and $J$ is the sole element of $S_q$.
\LMHash{}%
-The least upper bound of \DYNAMIC{} and any type $T$ is \DYNAMIC{}.
-The least upper bound of \VOID{} and any type $T \ne \DYNAMIC{}$ is \VOID{}.
-The least upper bound of $\bot$ and any type $T$ is $T$.
-Let $U$ be a type variable with upper bound $B$.
-The least upper bound of $U$ and a type $T \ne \bot$ is the least upper bound of $B$ and $T$.
+Let $X$ be a type variable with upper bound $B$.
+The least upper bound of $X$ and a type $T \ne \bot$ is the least upper bound of $B$ and $T$.
+
+\commentary{
+For example,
+the least upper bound of \VOID{} and any type $T$ is \VOID{};
+the least upper bound of \DYNAMIC{} and any type $T \not= \VOID$ is \DYNAMIC{};
+and the least upper bound of \code{int} and \code{double} is \code{num}.
+}
\LMHash{}%
The least upper bound operation is commutative and idempotent,
@@ -12039,53 +12241,74 @@
% Function types
\LMHash{}%
-The least upper bound of a function type and an interface type $T$ is the least upper bound of \FUNCTION{} and $T$.
+The least upper bound of a function type and an interface type $T$
+is the least upper bound of \FUNCTION{} and $T$.
+The greatest lower bound of a function type and an interface type $T$
+is \code{Null}.
+
+\LMHash{}%
Let $F$ and $G$ be function types.
If $F$ and $G$ differ in their number of required parameters,
-then the least upper bound of $F$ and $G$ is \FUNCTION{}.
+or in the number of formal type parameters,
+or in any bound for a formal type parameter,
+the least upper bound of $F$ and $G$ is \FUNCTION{}
+and the greatest lower bound of $F$ and $G$ is \code{Null}.
Otherwise:
\begin{itemize}
-\item If
-
-\code{$F = $ <$X_1\ B_1, \ldots,\ X_s\ B_s$>($T_1, \ldots,\ T_r,\ $[$T_{r+1}, \ldots,\ T_n$]) $ \rightarrow T_0$} and
-
-\code{$G = $ <$X_1\ B_1, \ldots,\ X_s\ B_s$>($S_1, \ldots,\ S_r,\ $[$S_{r+1}, \ldots,\ S_k$]) $ \rightarrow S_0$}
+\item If $F$ and $G$ are, respectively,
+\FunctionTypePositional{T_0}{ }{X}{B}{s}{T}{n}{k_1}
+\FunctionTypePositional{S_0}{ }{X}{B}{s}{S}{n}{k_2}
\noindent
-where $k \le n$ then the least upper bound of $F$ and $G$ is
-
-\code{<$X_1\ B_1, \ldots,\ X_s\ B_s$>($L_1, \ldots,\ L_r,\ $[$L_{r+1}, \ldots,\ L_k$]) $ \rightarrow L_0$}
+and $k_1 \le k_2$ then the least upper bound of $F$ and $G$ is
+\FunctionTypePositional{U_0}{ }{X}{B}{s}{U}{n}{k_1}
\noindent
-where $L_i$ is the least upper bound of $T_i$ and $S_i, i \in 0 .. k$.
-\item If
+where $U_0$ is the least upper bound of $T_0$ and $S_0$,
+and $U_i$ is the greatest lower bound of $T_i$ and $S_i, i \in 1 .. n + k_1$;
+and the greatest lower bound of $F$ and $G$ is
+\FunctionTypePositional{V_0}{ }{X}{B}{s}{V}{n}{k_2}
-\code{$F = $ <$X_1\ B_1, \ldots,\ X_s\ B_s$>($T_1, \ldots,\ T_r,\ $[$T_{r+1}, \ldots,\ T_n$]) $ \rightarrow T_0$},
+\noindent
+where $V_0$ is the greatest lower bound of $T_0$ and $S_0$,
+and $U_i$ is the least upper bound of $T_i$ and $S_i, i \in 1 .. n + k_1$,
+and $U_i$ is $S_i$ for $i \in n + k_1 + 1 .. n + k_2$.
-\code{$G = $ <$X_1\ B_1, \ldots,\ X_s\ B_s$>($S_1, \ldots,\ S_r,\ $\{ \ldots{} \}) $ \rightarrow S_0$}
+\item If $F$ and $G$ are, respectively,
+\FunctionType{T_0}{ }{X}{B}{s}{\List{T}{1}{n},\ [\ldots]}
+\FunctionType{S_0}{ }{X}{B}{s}{\List{S}{1}{n},\ \{\ldots\}}
\noindent
then the least upper bound of $F$ and $G$ is
-
-\code{<$X_1\ B_1, \ldots,\ X_s\ B_s$>($L_1, \ldots,\ L_r$) $ \rightarrow L_0$}
+\FunctionType{U_0}{ }{X}{B}{s}{\List{U}{1}{n}}
\noindent
-where $L_i$ is the least upper bound of $T_i$ and $S_i, i \in 0 .. r$.
-\item If
+where $U_0$ is the least upper bound of $T_0$ and $S_0$,
+and $U_i$ is the greatest lower bound of $T_i$ and $S_i, i \in 1 .. n$.
+The greatest lower bound of $F$ and $G$ is \code{Null}.
+\item If $F$ and $G$ are, respectively,
+\FunctionTypeNamed{T_0}{ }{X}{B}{s}{T}{n}{x}{k_1}
+\FunctionTypeNamed{S_0}{ }{X}{B}{s}{S}{n}{y}{k_2}
-\code{$F = $ <$X_1\ B_1, \ldots,\ X_s\ B_s$>($T_1, \ldots,\ T_r,\ $\{$T_{r+1}\ p_{r+1}, \ldots,\ T_f\ p_f$\}) $ \rightarrow T_0$},
-
-\code{$G = $ <$X_1\ B_1, \ldots,\ X_s\ B_s$>($S_1, \ldots,\ S_r,\ $\{$S_{r+1}\ q_{r+1}, \ldots,\ S_g\ q_g$\}) $ \rightarrow S_0$}
-
+\noindent
then let
-$\{x_m, \ldots, x_n\} = \{p_{r+1}, \ldots, p_f\} \cap \{q_{r+1}, \ldots, q_g\}$
-and let $X_j$ be the least upper bound of the types of $x_j$ in $F$ and
-$G, j \in m .. n$.
+$\{\List{z}{n+1}{n+k}\} = \{\List{x}{n+1}{n+k_1}\} \cap \{\List{y}{n+1}{n+k_2}\}$,
+let $U_0$ be the least upper bound of $T_0$ and $S_0$,
+let $U_j$ be the greatest lower bound of $T_j$ and $S_j$, for $j \in 1 .. n$,
+and let $U_j$ be the greatest lower bound of
+the types of $z_j$ in $F$ and $G$ for $j \in n + 1 .. n + k$.
Then the least upper bound of $F$ and $G$ is
+\FunctionTypeNamed{U_0}{ }{X}{B}{s}{U}{n}{z}{k}.
-\code{<$X_1\ B_1, \ldots,\ X_s\ B_s$>($L_1, \ldots,\ L_r,\ $\{$X_m\ x_m, \ldots,\ X_n\ x_n$\}) $ \rightarrow L_0$}
-
-where $L_i$ is the least upper bound of $T_i$ and $S_i, i \in 0 .. r$
+Similarly, let
+$\{\List{w}{n+1}{n+k}\} = \{\List{x}{n+1}{n+k_1}\} \cup \{\List{y}{n+1}{n+k_2}\}$,
+let $V_0$ be the greatest lower bound of $T_0$ and $S_0$,
+let $V_j$ be the least upper bound of $T_j$ and $S_j$, for $j \in 1 .. n$,
+and let $V_j$ be the least upper bound of
+the types of $z_j$ in $F$ and $G$ for $j \in n + 1 .. n + k$,
+using the type which is present when $z_j$ occurs only in $F$ or only in $G$.
+Then the greatest lower bound of $F$ and $G$ is
+\FunctionTypeNamed{V_0}{ }{X}{B}{s}{V}{n}{z}{k}.
\end{itemize}
\commentary{
diff --git a/docs/language/informal/extreme-upper-lower-bounds.md b/docs/language/informal/extreme-upper-lower-bounds.md
index 982dc4d..63d639e 100644
--- a/docs/language/informal/extreme-upper-lower-bounds.md
+++ b/docs/language/informal/extreme-upper-lower-bounds.md
@@ -2,9 +2,10 @@
**Owner**: eernst@
-**Status**: Implemented.
+**Status**: This document is now background material.
+For normative text, please consult the language specification.
-**Version**: 0.2 (2018-05-22)
+**Version**: 0.3 (2018-11-20)
This document is a Dart 2 feature specification which specifies how to
@@ -245,6 +246,9 @@
## Updates
+* Nov 20th 2018, version 0.3: Marked as background, new normative text
+ on this topic has been added to the language specification.
+
* May 22nd 2018, version 0.2: Adjusted to use `Object < dynamic < void`
as a "subtyping micro-structure" (which produces a simpler set of
rules) and mention the rules from version 0.1 merely as a possible
To view, visit change 84908. To unsubscribe, or for help writing mail filters, visit settings.
Erik Ernst (Gerrit)
Nov 21, 2018, 4:47:39 AM11/21/18
to rev...@dartlang.org, Leaf Petersen, Lasse R.H. Nielsen
Transferred the discussion about topics affected by this CL from 81263, attaching them as review comments to the same line of the same change as they were attached to in 81263.
1 comment:
File docs/language/dartLangSpec.tex:
Patch Set #2, Line 3479:
For the relation `\MoreSignatureSpecificSymbol',Discussion at this point transferred from CL 81263:
----------------------------------------------------------------------
Leaf Petersen:I don't understand what all of this section is about. I think we'll have to discuss this offline. In particular, I don't see why we need to duplicate the subtyping, nor why we need to involve the non-top types. The only use that I see of this relation is to relate top types, so why include non-top types in the relation?
Lasse R.H. Nielsen:
I'm assuming it's to apply the top-type specialization recursively.
If we say that Object <:: dynamic, then we also want List<Object> <:: List<dynamic>, and covariantly on function types, etc.(I think it's better to write it out than say "like that relation, except these many things").
Erik Ernst:
Exactly, if the relation is only defined on top types then we can't make a distinction for other types containing top types.
Also, I'd like to handle the ambiguity among `FutureOr<Null>` and `Future<Null>`, so it's not just top types.
So the intention is to define a partial order (let's call it `<<:`) on all types such that
`S <<: T => S <: T`, that is, a refinement of subtyping.Being a partial order, we never have `S <<: T /\ T <<: S /\ S != T`. In other words, `<<:` is never ambiguous, but it may determine that `S` and `T` are unrelated.
Next, I'd want `(S <: T /\ T <\: S) => S <<: T`. That is, `<:` and `<<:` coincide in every case where `<:` can make a decision.
For `S == T` we easily get `S <: T /\ T <: S` and similarly `S <<: T /\ T <<: S`.
In the remaining cases, we have `S <: T /\ T <: S /\ S != T`, and this is exactly the case where we'd like to detect that there is a difference between `S` and `T` even though they are "the same type according to the subtype relation". And I'd like to get a decision from `<<:` about which one of `S` and `T` is more signature specific in a way that follows "naturally" from the behavior of `<<:` on top types.
The definition given here is intended to satisfy these properties.
Leaf Petersen:
Sorry, I still don't understand the point of this. I was expecting it to be used for LUB/GLB (and that's what it looks like below), but for that you don't need to duplicate the whole subtype relation. I agree with your characterization of a partial order above, but I don't know why we want or need this particular partial order.
Erik Ernst:
I think we'd ideally need a refinement of the subtype rules as a whole because we wouldn't otherwise be able to tell whether `(b ? <Object>[null] : <dynamic>[null])[0].whateverYouWant(42)` is an error. Similarly, we'd need a refinement of the subtype rules as a whole in order to specify member signature conflict resolution.
However, the latter has been revised to say that we use the textual order of the direct superinterface clauses, which is what the implementations currently do.
So least upper bound was the only remaining place where we used this disambiguation device.
The behavior of current implementations matches what I specified for top types at top level (the signature specificity relation was adjusted precisely to match that behavior).
However, in the case where the two branches have types that differ only by having different top types as subterms in certain locations it chooses the type from the second branch (and ignores the first branch entirely). I guess they are just detecting that the two branches have types `S` and `T` such that `S <: T` and `T <: S`, and then they report the type `T` for the conditional expression as a whole, no questions asked.
That's not particularly consistent, but given that we're in "just specify whatever they do now" mode, I'll make adjustments in 84908 to do that.
So we'll take textual order in `implements` for class interfaces, and we will take reverse textual order for `?:`. Let's hope that we don't have one more construct like that, because then we won't be able to maintain the balance. ;-)
Note that I haven't touched the text about how to compute the least upper bound of two interface types: We've discussed discussing how to do that in a better way, but never dived into any detailed models, so I thought the safe bet would be to leave that completely as-is.
To view, visit change 84908. To unsubscribe, or for help writing mail filters, visit settings.
Erik Ernst (Gerrit)
Sep 10, 2021, 4:35:01 AM9/10/21
to rev...@dartlang.org, Leaf Petersen, Lasse R.H. Nielsen
Erik Ernst abandoned this change.
Abandoned
We never did this.
To view, visit change 84908. To unsubscribe, or for help writing mail filters, visit settings.
Reply all
Reply to author
Forward
0 new messages