From cd2e7680edc454b50cac63e5f3f37a99d4181585 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Fri, 7 Dec 2018 09:25:17 +0000 Subject: [PATCH] Corrected instantiate-to-bound.md. 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 --- docs/language/dartLangSpec.tex | 15 ++- .../language/informal/instantiate-to-bound.md | 101 +++++++++++++++--- 2 files changed, 92 insertions(+), 24 deletions(-) diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex index 594801c9fd7..e98c0db83d3 100644 --- a/docs/language/dartLangSpec.tex +++ b/docs/language/dartLangSpec.tex @@ -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 diff --git a/docs/language/informal/instantiate-to-bound.md b/docs/language/informal/instantiate-to-bound.md index dfe36bc86ea..e54f47d36a5 100644 --- a/docs/language/informal/instantiate-to-bound.md +++ b/docs/language/informal/instantiate-to-bound.md @@ -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 _X1 .. Xk_ and bounds _B1 .. Bk_. We say that the formal type parameter @@ -145,17 +145,17 @@ is satisfied: 2. _Bj_ is included, but does not contain any of _X1 .. Xk_. If _Bj_ contains a type _T_ of the form `typeName` (*for instance, `C` or `p.D`*) which denotes a generic class - or parameterized type alias _G1_ (*that is, _T_ is a raw type*), + or generic type alias _G1_ (*that is, _T_ is a raw type*), every type argument of _G1_ has a simple bound. The notion of a simple bound must be interpreted inductively rather than coinductively, i.e., if a bound _Bj_ 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 _Bj_ is a simple bound, the answer is no. *For example, with `class 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 _F1 .. Fk_ be the formal type parameter declarations in the declaration of _G_, with type parameters _X1 .. Xk_ and bounds _B1 @@ -228,7 +228,8 @@ _Up,m_ (*so each type variable is related to, that is, depends on, every type variable in its bound, possibly including itself*). Let _==>m_ be the transitive closure of _-->m_. For each _m_, let _Ui,m+1_, for _i_ in _1 .. k_, be determined -by the following iterative process: +by the following iterative process, where _Vm_ denotes +_G<U1,m, Uk,m>_: 1. If there exists a _j_ in _1 .. k_ such that _Xj ==>m Xj_ @@ -246,9 +247,11 @@ by the following iterative process: _Ui,m+1 = Ui,m_. Otherwise there exists a _q_ such that _Xi_ belongs to _Mq_; _Ui,m+1_ is then obtained from _Ui,m_ - by replacing every covariant occurrence of a variable in _Mq_ by - `dynamic`, and replacing every contravariant occurence of a variable in - _Mq_ by `Null`. + by substituting `dynamic` for every occurrence of a variable + in _Mq_ that is in a covariant or invariant position + in _Vm_, and substituting `Null` for every occurrence of + a variable in _Mq_ that is in a contravariant position + in _Vm_. 2. Otherwise, (*if no dependency cycle exists*) let _j_ be the lowest number such that _Xj_ occurs in _Up,m_ for some _p_ and @@ -257,9 +260,11 @@ by the following iterative process: _Xj_ does not contain any type variables; but _Xj_ is being depended on by the bound of some other type variable*). Then, for all _i_ in _1 .. k_, _Ui,m+1_ is obtained from - _Ui,m_ by replacing every covariant occurrence of _Xj_ - by _Uj,m_, and replacing every contravariant occurrence of - _Xj_ by `Null`. + _Ui,m_ by substituting _Uj,m_ for every occurrence + of _Xj_ which occurs in a covariant or invariant position in + _Vm_, and substituting `Null` for every occurrence of + _Xj_ which occurs in a contravariant position in + _Vm_. 3. Otherwise, (*when no dependencies exist*) terminate with the result _<U1,m ..., Uk,m>_. @@ -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 Function(X); +class B> {} + +B b; // The raw `B` means `B>`. +``` + +*It is then possible to store an instance of, say, +`B` 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>`, because +`Inv` is not a subtype of `Inv`.* + +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> {} +typedef F> = 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>`, 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 Function(C)`. 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` and `F`, even when +`T1 <: T2` or vice versa. In particular there is no type `T` such that a +function of type `F` could be the value of a variable of type +`C Function(C)`. So the raw `F`, if permitted, would +not be "a supertype of `F` for all possible `T`", it would be a type +which is unrelated to `F` 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 _G1 .. Tk>_ it is applied to _T1 .. Tk_; 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.