mirror of
https://github.com/dart-lang/sdk
synced 2024-11-02 06:20:13 +00:00
Bounds of a generic type alias ensure the body is regular-bounded
The analyzer enforces the rule that when a generic type alias F has
formal type parameters X1..Xm with bounds B1..Bm, if we assume that
X1..Xm are types satisfying the corresponding bounds then it must be
the case that every type which occurs in the body of F must be
regular-bounded.
In other words, the bounds on the left hand side of `=` must imply
the bounds applicable to every type on the right hand side.
---------- NEW TEXT ----------
I just discovered that it is _not_ possible to skip the check on
every super-bounded parameterized type based on a generic type
alias: It is certainly possible to have a type which is correctly
super-bounded according to the type parameter bounds on the left
hand side of `=` in the type alias declaration, and still have a
right hand side where some types are not well-bounded. Consider the
following declarations:
class B<Y1 extends Y2, Y2, Y3 extends num> {}
typedef F<X extends num> = B<num, Object, X> Function();
According to the declarations to the left of `=`, `F<Object>`
is a correct super-bounded type, because it is not
regular-bounded (`Object <\: num`), and `F<Null>` is regular-bounded
(`Null <: num`).
Also, when the declared bound of `X` is satisfied, we are
guaranteed that each type on the right hand side is regular-bounded
(if parameterized, it receives type arguments that satisfy all
the specified bounds).
But consider the result of applying `F` to `Object`:
B<num, Object, Object> Function();
That's not a type where all subterms which are types are
well-bounded:
B<num, Object, Object> is not regular-bounded because
`Object <\: num` (third type argument).
B<num, Object, Object> is not super-bounded because
B<num, Null, Null> is not regular-bounded because
`num <\: Null` (violating `Y1 extends Y2`).
So there is no way we can prove that this check can be skipped,
because we have a pretty simple counter-example!
I'm currently adjusting the text to re-introduce the check.
---------- OLD TEXT, NOT VALID ----------
This must be specified, because it justifies the _removal_ of a
requirement that we had in the feature specification
super-bounded-types.md: It was required for every application of a
generic type alias F to a list of actual type arguments <T1..Tk>
such that the resulting parameterized type F<T1..Tk> was
super-bounded that both the parameterized type F<T1..Tk> and every
type in the resulting type [T1/X1..Tk/Xk]U (where U is the body of
F and X1..Xk are its formal type parameters) be well-bounded.
But when the bounds of F imply satisfaction of the bounds of all
types that occur in the body of F, it's trivially true that all
types in the resulting type are regular-bounded for the result
of substituting Null for covariant top types and Object for
contravariant Null for every super-bounded F<T1..Tk>. I'm looking
into a proof sketch for the result that this implies that any
well-bounded generic type alias application yields a type that
contains only well-bounded types.
This would be a very welcome simplification (because it was an
inconvenient complication that we had to check both the left hand
side and the right hand side of a type alias whenever we
encountered a super-bounded type expressed via a type alias), and
I believe that it will also make the tools run faster (because they
can now skip all those checks of every type that occurs in the body
for every super-bounded usage of a type alias.
Change-Id: Icd70649ebaed41b193aeb0cb6f08d06aed0ee5bd
Reviewed-on: https://dart-review.googlesource.com/c/79743
Reviewed-by: Leaf Petersen <leafp@google.com>
Reviewed-by: Lasse R.H. Nielsen <lrn@google.com>
This commit is contained in:
Erik Ernst
parent
6efc58f069
commit
57f895c7a4
2 changed files with 103 additions and 37 deletions
|
|
@ -63,6 +63,10 @@
|
|||
% - Eliminate all references to checked and production mode, Dart 2 does
|
||||
% not have modes.
|
||||
% - Integrate feature specification on noSuchMethod forwarders.
|
||||
% - Specify that bound satisfaction in generic type alias type parameters
|
||||
% must imply bound satisfaction everywhere in the body.
|
||||
% - Specify that super-bounded generic type alias applications must trigger
|
||||
% a well-boundedness check on all types occurring in the denoted type.
|
||||
%
|
||||
% 2.0
|
||||
% - Don't allow functions as assert test values.
|
||||
|
|
@ -3538,11 +3542,6 @@ It is a compile-time error if $m \not= l$.
|
|||
It is a compile-time error if $T$ is not well-bounded
|
||||
(\ref{superBoundedTypes}).
|
||||
|
||||
\commentary{
|
||||
That is, if the number of type arguments is wrong,
|
||||
or one or more of the upper bounds has been violated.
|
||||
}
|
||||
|
||||
\LMHash{}
|
||||
Otherwise, said parameterized type \code{C<$T_1, \ldots,\ T_m$>} denotes an application of the generic class declared by $G$ to the type arguments $T_1, \ldots, T_m$.
|
||||
This yields a class $C'$ whose members are equivalent to those of a class declaration which is obtained from the declaration of $G$ by replacing each occurrence of $X_j$ by $T_j$.
|
||||
|
|
@ -3553,22 +3552,35 @@ Other properties of $C'$ such as the subtype relationships are specified elsewhe
|
|||
}
|
||||
|
||||
\LMHash{}
|
||||
A {\em generic type alias} introduces a mapping from actual type argument lists to types.
|
||||
Consider a generic type alias declaration $G$ named \code{F} with formal type parameter declarations
|
||||
A {\em generic type alias}
|
||||
introduces a mapping from actual type argument lists to types.
|
||||
Consider a generic type alias declaration $G$ named \code{F}
|
||||
with formal type parameter declarations
|
||||
$X_1\ \EXTENDS\ B_1, \ldots,\ X_m\ \EXTENDS\ B_m$,
|
||||
and right hand side $T$,
|
||||
and the parameterized type $S$ of the form \code{F<$T_1, \ldots,\ T_l$>}.
|
||||
%% TODO(eernst): 'right hand side' works only for a type alias using `=`.
|
||||
%% Explain what "the right hand side" means for an old-style declaration.
|
||||
and right hand side $T$.
|
||||
|
||||
\LMHash{}
|
||||
Under the assumption that $X_1,\ \ldots,\ X_m$ are types such that
|
||||
$X_j <: B_j$, for all $j \in 1 .. m$,
|
||||
it is a compile-time error if any type in $T$ is not regular-bounded.
|
||||
|
||||
\commentary{
|
||||
This means that the bounds declared for
|
||||
the formal type parameters of a generic type alias
|
||||
must be such that when they are satisfied,
|
||||
the bounds that pertain to any type in the body must also be satisfied.
|
||||
}
|
||||
|
||||
\LMHash{}
|
||||
Let $G$, \code{F}, and $X_1,\ \ldots,\ X_m$ be as defined above,
|
||||
let $T_1,\ \ldots,\ T_l$ be types,
|
||||
and let $S$ be the parameterized type \code{F<$T_1, \ldots,\ T_l$>}.
|
||||
It is a compile-time error if $m \not= l$.
|
||||
It is a compile-time error if $S$ is not well-bounded
|
||||
(\ref{superBoundedTypes}).
|
||||
|
||||
\commentary{
|
||||
That is, if the number of type arguments is wrong,
|
||||
or one or more of the upper bounds has been violated.
|
||||
}
|
||||
|
||||
\LMHash{}
|
||||
Otherwise, said parameterized type
|
||||
\code{F<$T_1, \ldots,\ T_m$>}
|
||||
|
|
@ -3577,10 +3589,38 @@ $T_1, \ldots, T_m$.
|
|||
This yields the type
|
||||
$[T_1/X_1, \ldots, T_m/X_m]T$.
|
||||
|
||||
\rationale{
|
||||
The requirement that satisfaction of the bounds on
|
||||
the formal type parameters of a generic type alias $G$
|
||||
must imply satisfaction of all bounds pertaining to
|
||||
every type that occurs in the body of $G$
|
||||
limits the expressive power of generic type aliases.
|
||||
However, it would require the constraints on formal type parameters
|
||||
to be expressed in a much more powerful language
|
||||
if we were to allow a significantly larger set of types
|
||||
to be expressed using a generic type alias.
|
||||
}
|
||||
|
||||
\commentary{
|
||||
A generic type alias does not correspond to any entities at run time,
|
||||
it is only an alias for an existing type.
|
||||
Hence, we may consider it as syntactic sugar which is eliminated before the program runs.
|
||||
For example, consider the following code:
|
||||
}
|
||||
|
||||
\begin{dartCode}
|
||||
\CLASS{} A<X \EXTENDS{} \VOID{} \FUNCTION(num)> \{\}
|
||||
\TYPEDEF{} F<Y> = A<\VOID{} \FUNCTION(Y)> \FUNCTION(); // \comment{compile-time error}
|
||||
\end{dartCode}
|
||||
|
||||
\commentary{
|
||||
There is no way to specify a bound on \code{Y} in the declaration of \code{F}
|
||||
which will ensure that all bounds on the right hand side are respected.
|
||||
This is because the actual requirement is that \code{Y} must be
|
||||
a \emph{supertype} of \code{num},
|
||||
but Dart does not support lower bounds for type parameters.
|
||||
The type \code{A<\VOID{} \FUNCTION(U)> \FUNCTION()}
|
||||
can still be specified explicitly
|
||||
for every \code{U} which satisfies the bounds declared by \code{A}.
|
||||
So the types can be expressed,
|
||||
they just cannot be abbreviated using a generic type alias.
|
||||
}
|
||||
|
||||
\LMHash{}
|
||||
|
|
@ -3768,13 +3808,13 @@ if{}f one of the following conditions is true:
|
|||
for some $j \in 1 .. n$.
|
||||
|
||||
\item $T$ is of the form \code{$G$<$S_1, \ldots,\ S_n$>}
|
||||
where $G$ denotes a parameterized type alias such that
|
||||
where $G$ denotes a generic type alias such that
|
||||
$j \in 1 .. n$,
|
||||
the formal type parameter corresponding to $S_j$ is covariant,
|
||||
and $S$ occurs in a covariant position in $S_j$.
|
||||
|
||||
\item $T$ is of the form \code{$G$<$S_1, \ldots,\ S_n$>}
|
||||
where $G$ denotes a parameterized type alias such that
|
||||
where $G$ denotes a generic type alias such that
|
||||
$j \in 1 .. n$,
|
||||
the formal type parameter corresponding to $S_j$ is contravariant,
|
||||
and $S$ occurs in a contravariant position in $S_j$.
|
||||
|
|
@ -3816,13 +3856,13 @@ if{}f one of the following conditions is true:
|
|||
for some $j \in 1 .. n$.
|
||||
|
||||
\item $T$ is of the form \code{$G$<$S_1, \ldots,\ S_n$>}
|
||||
where $G$ denotes a parameterized type alias such that
|
||||
where $G$ denotes a generic type alias such that
|
||||
$j \in 1 .. n$,
|
||||
the formal type parameter corresponding to $S_j$ is covariant,
|
||||
and $S$ occurs in a contravariant position in $S_j$.
|
||||
|
||||
\item $T$ is of the form \code{$G$<$S_1, \ldots,\ S_n$>}
|
||||
where $G$ denotes a parameterized type alias such that
|
||||
where $G$ denotes a generic type alias such that
|
||||
$j \in 1 .. n$,
|
||||
the formal type parameter corresponding to $S_j$ is contravariant,
|
||||
and $S$ occurs in a covariant position in $S_j$.
|
||||
|
|
@ -3834,7 +3874,7 @@ if{}f one of the following conditions is true:
|
|||
|
||||
\begin{itemize}
|
||||
\item $T$ is of the form \code{$G$<$S_1,\ \ldots,\ S_n$>}
|
||||
where $G$ denotes a generic class or a parameterized type alias,
|
||||
where $G$ denotes a generic class or a generic type alias,
|
||||
and $S$ occurs in an invariant position in $S_j$ for some $j \in 1 .. n$.
|
||||
|
||||
\item $T$ is of the form
|
||||
|
|
@ -3860,7 +3900,7 @@ if{}f one of the following conditions is true:
|
|||
for some $i \in 1 .. m$.
|
||||
|
||||
\item $T$ is of the form \code{$G$<$S_1, \ldots,\ S_n$>}
|
||||
where $G$ denotes a parameterized type alias,
|
||||
where $G$ denotes a generic type alias,
|
||||
$j \in 1 .. n$,
|
||||
the formal type parameter corresponding to $S_j$ is invariant,
|
||||
and $S$ occurs in $S_j$.
|
||||
|
|
@ -3919,9 +3959,16 @@ and so are \code{FutureOr<\VOID>} and \code{FutureOr<FutureOr<\DYNAMIC>{}>}.
|
|||
|
||||
\LMHash{}
|
||||
Every type which is not a parameterized type is {\em regular-bounded}.
|
||||
|
||||
\commentary{
|
||||
In particular, every non-generic class and every function type
|
||||
is a regular-bounded type.
|
||||
}
|
||||
|
||||
\LMHash{}
|
||||
Let $T$ be a parameterized type of the form
|
||||
\code{$G$<$S_1, \ldots,\ S_n$>}
|
||||
where $G$ denotes a generic class or a parameterized type alias.
|
||||
where $G$ denotes a generic class or a generic type alias.
|
||||
Let
|
||||
\code{$X_1\ \EXTENDS\ B_1, \ldots,\ X_n\ \EXTENDS\ B_n$}
|
||||
be the formal type parameter declarations of $G$.
|
||||
|
|
@ -3931,14 +3978,14 @@ $[S_1/X_1, \ldots,\ S_n/X_n]B_j$,
|
|||
for all $j \in 1 .. n$.
|
||||
|
||||
\commentary{
|
||||
This means that each actual type argument satisfies the declared upper
|
||||
bound for the corresponding formal type parameter.
|
||||
This means that regular-bounded types are those types
|
||||
that do not violate their type parameter bounds.
|
||||
}
|
||||
|
||||
\LMHash{}
|
||||
Let $T$ be a parameterized type of the form
|
||||
\code{$G$<$S_1, \ldots,\ S_n$>}
|
||||
where $G$ denotes a generic class or a parameterized type alias.
|
||||
where $G$ denotes a generic class or a generic type alias.
|
||||
$T$ is {\em super-bounded} if{}f the following conditions are both true:
|
||||
|
||||
\begin{itemize}
|
||||
|
|
@ -3953,6 +4000,11 @@ $T$ is {\em super-bounded} if{}f the following conditions are both true:
|
|||
It is then required that
|
||||
\code{$G$<$S'_1, \ldots,\ S'_n$>}
|
||||
is regular-bounded.
|
||||
%
|
||||
Moreover, if $G$ denotes a generic type alias with body $U$,
|
||||
it is required that every type that occurs as a subterm of
|
||||
$[S_1/X_1, \ldots,\ S_n/X_n]U$
|
||||
is well-bounded (defined below).
|
||||
\end{itemize}
|
||||
|
||||
\commentary{
|
||||
|
|
@ -3979,7 +4031,7 @@ when it is used in any of the following ways:
|
|||
\item $T$ is an immediate subterm of a redirecting factory constructor
|
||||
signature
|
||||
(\ref{redirectingFactoryConstructors}).
|
||||
\item $T$ is an immediate subterm of an \EXTENDS{} clause
|
||||
\item $T$ is an immediate subterm of an \EXTENDS{} clause of a class
|
||||
(\ref{superclasses}),
|
||||
or it occurs as an element in the type list of an \IMPLEMENTS{} clause
|
||||
(\ref{superinterfaces}),
|
||||
|
|
@ -4017,6 +4069,9 @@ even though the upper bound on the type variable \code{X} is \code{num}.
|
|||
\rationale{
|
||||
Super-bounded types enable the expression of informative common supertypes
|
||||
of some sets of types whose common supertypes would otherwise be much less informative.
|
||||
}
|
||||
|
||||
\commentary{
|
||||
For example, consider the following class:
|
||||
}
|
||||
|
||||
|
|
@ -4026,7 +4081,7 @@ For example, consider the following class:
|
|||
\}
|
||||
\end{dartCode}
|
||||
|
||||
\rationale{
|
||||
\commentary{
|
||||
Without super-bounded types,
|
||||
there is no type $T$ which makes \code{C<$T$>} a common supertype of
|
||||
all types of the form \code{C<$S$>}
|
||||
|
|
@ -4037,12 +4092,14 @@ then that variable must use \code{Object} or another top type
|
|||
as its type annotation,
|
||||
which means that a member like \code{next} is not known to exist
|
||||
(which is what we mean by saying that the type is `less informative').
|
||||
}
|
||||
|
||||
\rationale{
|
||||
We could introduce a notion of recursive (infinite) types, and express
|
||||
the least upper bound of all types of the form \code{C<$S$>} as
|
||||
some syntax whose meaning could be approximated by
|
||||
\code{C<C<C<C<$\ldots$>$\!$>$\!$>$\!$>}.
|
||||
|
||||
%
|
||||
However, we expect that any such concept in Dart would incur a significant cost
|
||||
on developers and implementations in terms of added complexity and subtlety,
|
||||
so we have chosen not to do that.
|
||||
|
|
@ -4063,7 +4120,7 @@ at the point where the unfolding ends:
|
|||
If \code{c} has type \code{C<C<\DYNAMIC>{}>}
|
||||
then \code{c.next.next} has type \DYNAMIC{}
|
||||
and \code{c.next.next.whatever} has no compile-time error,
|
||||
but if \code{c} has type \code{C<C<\VOID>{}>} then
|
||||
but if \code{c} has type \code{C<C<\VOID>{}>} then already
|
||||
\code{Object x = c.next.next;} is a compile-time error.
|
||||
It is thus possible for developers to get a more or less strict treatment
|
||||
of expressions whose type proceeds beyond the given finite unfolding.
|
||||
|
|
|
|||
|
|
@ -2,10 +2,14 @@
|
|||
|
||||
**Author**: eernst@.
|
||||
|
||||
**Version**: 0.7 (2018-06-01).
|
||||
**Version**: 0.8 (2018-10-16).
|
||||
|
||||
**Status**: Background material.
|
||||
The language specification has the normative text on this topic.
|
||||
Note that the rules have changed, which means that
|
||||
**this document cannot be used as a reference**, it can only be
|
||||
used to get an overview of the ideas; please refer to the language
|
||||
specification for all technical details.
|
||||
|
||||
**This document** is an informal specification of the support in Dart 2 for
|
||||
using certain generic types where the declared bounds are violated. The
|
||||
|
|
@ -31,9 +35,9 @@ void foo<X extends List<num>>(X x) {
|
|||
...
|
||||
}
|
||||
```
|
||||
cannot be invoked with `foo<List<dynamic>>('Hello!')`, nor can the type
|
||||
cannot be invoked with `foo<List<dynamic>>([])`, nor can the type
|
||||
argument be inferred to `List<dynamic>` in an invocation like
|
||||
`foo('Hello!')`. But `C<void> x = new C<int>();` is OK, and so is
|
||||
`foo([])`. But `C<void> x = new C<int>();` is OK, and so is
|
||||
`x is C<Object>`.
|
||||
|
||||
|
||||
|
|
@ -194,9 +198,11 @@ a `C<S>` (where `S` can be anything), but we could also pass it where a
|
|||
|
||||
Finally, if we choose to use `C<void>` and so on then we will not even be
|
||||
able to access the object where the type information ends: we cannot use
|
||||
the value of an expression like `c0.next` at all without an explicit
|
||||
cast. This means that we cannot pass `c0.next` as an argument to a function
|
||||
that accepts a `C<S>` (for any `S`) without an explicit cast.
|
||||
the value of an expression like `c0.next` without an explicit
|
||||
cast (OK, `void v = c0.next;` is accepted, but it is mostly impossible to
|
||||
use the value of an expression of type `void`). This means that we cannot
|
||||
pass `c0.next` as an argument to a function that accepts a `C<S>`
|
||||
(for any `S`) without an explicit cast.
|
||||
|
||||
In summary, the choice of `dynamic`, `Object`, and `void` offers a range of
|
||||
approaches to the lack of typing information, but the amount of information
|
||||
|
|
@ -581,6 +587,9 @@ class types like `C<C<dynamic>>` that we have already argued are useful.
|
|||
|
||||
## Updates
|
||||
|
||||
* Version 0.8 (2018-10-16), emphasized that this document is no longer
|
||||
specifying the current rules, it is for background info only.
|
||||
|
||||
* Version 0.7 (2018-06-01), marked as background material: The normative
|
||||
text on variance and on super-bounded types is now part of the language
|
||||
specification.
|
||||
|
|
|
|||
Loading…
Reference in a new issue