languages/dart-sdk
languages/dart-sdk
1
0
Fork 0
mirror of https://github.com/dart-lang/sdk synced 2024-09-05 16:41:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

Corrected instantiate-to-bound.md.

Browse source 
Corrected instantiate-to-bound.md to (1) take the variance of the top level
type into account for each step of the algorithm, and (2) explicitly require
that the type yielded by the algorithm must be checked for well-boundedness;
finally (3) an example showing that we can indeed get a result which is not
well-bounded was added.

Also adjusted the terminology to be consistent with dartLangSpec.tex
(where we say 'generic type alias' rather than 'parameterized type
alias').

Change-Id: I4b4e4ee7988439e39b05514f172d69233b1695d7
Reviewed-on: https://dart-review.googlesource.com/c/80140
Reviewed-by: Leaf Petersen <leafp@google.com>
This commit is contained in:
Erik Ernst 2018-12-07 09:25:17 +00:00
parent 09f2736d9a
commit cd2e7680ed
2 changed files with 92 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
docs/language/dartLangSpec.tex
View file

@ -87,6 +87,8 @@
% adding the parts that are not captured by a function type subtype check.
% - Introduced the notion of member signatures, specified that they are the
% kind of entity that a class interface contains.
% - Corrected super-boundedness check to take variance into account at the
% top level.
%
% 2.0
% - Don't allow functions as assert test values.
@ -4826,14 +4828,11 @@ $T$ is \Index{super-bounded} if{}f the following conditions are both true:
\item
$T$ is not regular-bounded.
\item
For each $j \in 1 .. n$, let $S'_j$ be the result of replacing
every occurrence of a top type
in a covariant position in $S_j$ by \code{Null},
and every occurrence of \code{Null}
in a contravariant position in $S_j$ by \code{Object}.
It is then required that
\code{$G$<$S'_1, \ldots,\ S'_n$>}
is regular-bounded.
Let $T'$ be the result of replacing every occurrence in $T$
of a top type in a covariant position by \code{Null},
and every occurrence in $T$
of \code{Null} in a contravariant position by \code{Object}.
It is then required that $T'$ 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

101
docs/language/informal/instantiate-to-bound.md
View file

@ -2,7 +2,7 @@
**Author**: eernst@
**Version**: 0.8 (2018-09-26)
**Version**: 0.10 (2018-10-31)
**Status**: Implemented.
@ -133,7 +133,7 @@ bound _B_ contains a type variable `X` from the enclosing class, it is
never because `X` is contained in the body of a type alias, it will always
be as a syntactic subterm of _B_.*
Let _G_ be a generic class or parameterized type alias with _k_ formal type
Let _G_ be a generic class or generic type alias with _k_ formal type
parameter declarations containing formal type parameters
_X<sub>1</sub> .. X<sub>k</sub>_ and bounds
_B<sub>1</sub> .. B<sub>k</sub>_. We say that the formal type parameter
@ -145,17 +145,17 @@ is satisfied:
2. _B<sub>j</sub>_ is included, but does not contain any of _X<sub>1</sub>
.. X<sub>k</sub>_. If _B<sub>j</sub>_ contains a type _T_ of the form
`typeName` (*for instance, `C` or `p.D`*) which denotes a generic class
or parameterized type alias _G<sub>1</sub>_ (*that is, _T_ is a raw type*),
or generic type alias _G<sub>1</sub>_ (*that is, _T_ is a raw type*),
every type argument of _G<sub>1</sub>_ has a simple bound.
The notion of a simple bound must be interpreted inductively rather than
coinductively, i.e., if a bound _B<sub>j</sub>_ of a generic class or
parameterized type alias _G_ is reached during an investigation of whether
generic type alias _G_ is reached during an investigation of whether
_B<sub>j</sub>_ is a simple bound, the answer is no.
*For example, with `class C<X extends C> {}` the type parameter `X` does
not have a simple bound: A raw `C` is used as a bound for `X`, so `C`
must have simple bounds, but one of the bounds of `C` is the bound of `X`,
not have a simple bound: A raw `C` is used as a bound for `X`, so `C`
must have simple bounds, but one of the bounds of `C` is the bound of `X`,
and that bound is `C`, so `C` must have simple bounds: Cycle, hence error!*
*We can now specify in which sense instantiate to bound requires the
@ -174,7 +174,7 @@ parameter `X` that corresponds to the omitted type argument does not have a
simple bound.*
When a type annotation _T_ on the form `typeName` denotes a generic class
or parameterized type alias (*so _T_ is raw*), instantiate to bound is used
or generic type alias (*so _T_ is raw*), instantiate to bound is used
to provide the missing type argument list. It is a compile-time error if
the instantiate to bound process fails.
@ -200,7 +200,7 @@ applies to a type argument list which is omitted, such that a value for all
the actual type arguments must be computed.*
Let _T_ be a `typeName` term which denotes a generic class or
parameterized type alias _G_ (*so _T_ is a raw type*), let
generic type alias _G_ (*so _T_ is a raw type*), let
_F<sub>1</sub> .. F<sub>k</sub>_ be the formal type
parameter declarations in the declaration of _G_, with type parameters
_X<sub>1</sub> .. X<sub>k</sub>_ and bounds _B<sub>1</sub>
@ -228,7 +228,8 @@ _U<sub>p,m</sub>_ (*so each type variable is related to, that is, depends
on, every type variable in its bound, possibly including itself*).
Let _==><sub>m</sub>_ be the transitive closure of _--><sub>m</sub>_.
For each _m_, let _U<sub>i,m+1</sub>_, for _i_ in _1 .. k_, be determined
by the following iterative process:
by the following iterative process, where _V<sub>m</sub>_ denotes
_G&lt;U<sub>1,m</sub>, U<sub>k,m</sub>&gt;_:
1. If there exists a _j_ in _1 .. k_ such that
_X<sub>j</sub> ==><sub>m</sub> X<sub>j</sub>_
@ -246,9 +247,11 @@ by the following iterative process:
_U<sub>i,m+1</sub> = U<sub>i,m</sub>_.
Otherwise there exists a _q_ such that _X<sub>i</sub>_ belongs to
_M<sub>q</sub>_; _U<sub>i,m+1</sub>_ is then obtained from _U<sub>i,m</sub>_
by replacing every covariant occurrence of a variable in _M<sub>q</sub>_ by
`dynamic`, and replacing every contravariant occurence of a variable in
_M<sub>q</sub>_ by `Null`.
by substituting `dynamic` for every occurrence of a variable
in _M<sub>q</sub>_ that is in a covariant or invariant position
in _V<sub>m</sub>_, and substituting `Null` for every occurrence of
a variable in _M<sub>q</sub>_ that is in a contravariant position
in _V<sub>m</sub>_.
2. Otherwise, (*if no dependency cycle exists*) let _j_ be the lowest number
such that _X<sub>j</sub>_ occurs in _U<sub>p,m</sub>_ for some _p_ and
@ -257,9 +260,11 @@ by the following iterative process:
_X<sub>j</sub>_ does not contain any type variables; but _X<sub>j</sub>_ is
being depended on by the bound of some other type variable*).
Then, for all _i_ in _1 .. k_, _U<sub>i,m+1</sub>_ is obtained from
_U<sub>i,m</sub>_ by replacing every covariant occurrence of _X<sub>j</sub>_
by _U<sub>j,m</sub>_, and replacing every contravariant occurrence of
_X<sub>j</sub>_ by `Null`.
_U<sub>i,m</sub>_ by substituting _U<sub>j,m</sub>_ for every occurrence
of _X<sub>j</sub>_ which occurs in a covariant or invariant position in
_V<sub>m</sub>_, and substituting `Null` for every occurrence of
_X<sub>j</sub>_ which occurs in a contravariant position in
_V<sub>m</sub>_.
3. Otherwise, (*when no dependencies exist*) terminate with the result
_&lt;U<sub>1,m</sub> ..., U<sub>k,m</sub>&gt;_.
@ -272,6 +277,57 @@ when that number reaches zero.*
*Note that this process may produce a
[super-bounded type](https://github.com/dart-lang/sdk/blob/master/docs/language/informal/super-bounded-types.md).*
*It may seem somewhat arbitrary to treat unused and invariant parameters
the same as covariant parameters. In particular, we could easily have made
every attempt to use instantiate to bound an error, when applied to a type
where invariance occurs anywhere during the run of the algorithm. However,
there are a number of cases where this choice produces a usable type, and
we decided that it is not helpful to outlaw such cases:*
```dart
typedef Inv<X> = X Function(X);
class B<Y extends num, Z extends Inv<Y>> {}
B b; // The raw `B` means `B<num, Inv<num>>`.
```
*It is then possible to store an instance of, say,
`B<int, int Function(num)>` in `b`. It should be noted, however, that
any occurrence of invariance during instantiate to bound is likely to
cause the resulting type to not be a common supertype of all the types
that may be expressed by passing explicit type arguments. This means that
a raw type involving invariance cannot be considered to denote the type
"that allows all values for the actual type arguments". For instance,
`b` above cannot refer to an instance of `B<int, Inv<int>>`, because
`Inv<int>` is not a subtype of `Inv<num>`.*
It is a compile-time error if the above algorithm yields a type which is
not well-bounded.
*This kind of error can occur, as demonstrated by the following example:*
```dart
class C<X extends C<X>> {}
typedef F<X extends C<X>> = X Function(X);
F f; // Compile-time error.
```
*With these declarations, the raw `F` used as a type annotation is a
compile-time error: The algorithm yields `F<C<dynamic>>`, and that is
neither a regular-bounded nor a super-bounded type. It is conceptually
meaningful to make this an error, even though the resulting type can be
specified explicitly as `C<dynamic> Function(C<dynamic>)`. So that type
exists, we just cannot obtain it by passing a type argument to `F`.
The reason why it still makes sense to make the raw `F` an error is that
there is no subtype relationship between `F<T1>` and `F<T2>`, even when
`T1 <: T2` or vice versa. In particular there is no type `T` such that a
function of type `F<T>` could be the value of a variable of type
`C<dynamic> Function(C<dynamic>)`. So the raw `F`, if permitted, would
not be "a supertype of `F<T>` for all possible `T`", it would be a type
which is unrelated to `F<T>` for every single `T` that satisfies the
bound of `F`. In that sense, it is just an extreme example of that kind
of lack of usefulness that was mentioned for the raw `B` above.*
When instantiate to bound is applied to a type it proceeds recursively: For
a generic instantiation _G<T<sub>1</sub> .. T<sub>k</sub>>_ it is applied
to _T<sub>1</sub> .. T<sub>k</sub>_; for a function type
@ -297,9 +353,22 @@ applicable.
## Updates
* Oct 31st 2018, version 0.10: When computing the variance of an
occurrence of a type variable in the instantiate-to-bound algorithm,
it was left implicit with respect to which type the variance was
computed. This update makes it explicit.
* Oct 16th 2018, version 0.9: Corrected initial value of type argument
to take variance into account. Corrected the value chosen at each step
such that the invariant case is also handled. Added requirement that
the parameterized type obtained from the algorithm must be checked for
well-boundedness. Corrected the terminology to use 'generic type alias'
rather than 'parameterized type alias', following the terminology used
in the language specification.
* Sep 26th 2018, version 0.8: Fixed unintended omission: the same rules
that we specified for a generic class are now also specified to hold
for parameterized type aliases.
for generic type aliases.
* Feb 26th 2018, version 0.7: Revised cycle breaking algorithm for
F-bounded type variables to avoid specifying orderings that do not matter.