Owner: eernst@
Status: This document is now background material. For normative text, please consult the language specification.
Version: 0.6 (2018-06-01)
This document is an informal specification which specifies how to determine the reified type of a tear-off where one or more parameters has a type annotation in which a formal type parameter of the enclosing class occurs in a covariant position. This feature has no effect in Dart 1, it is only concerned with Dart 2.
The main topic here is variance, so we will briefly introduce that concept.
Consider the situation where a type is specified as an expression that contains another type as a subexpression. For instance, List<int> contains int as a subexpression. We may then consider List<...> as a function, and int as an argument which is passed to that function. With that, covariance is the property that this function is increasing, and contravariance is the property that it is decreasing, using the subtype relation for comparisons.
Generic classes in Dart are covariant in all their arguments. For example List<E> is covariant in E. This then means that List<...> is an increasing function, i.e., whenever S is a subtype of T, List<S> is a subtype of List<T>.
The subtype rule for function types in Dart 1 is different from the one in strong mode and in the upcoming Dart 2. This difference is the main fact that motivates the feature described in this document.
Concretely, the subtype rule for function types allows for covariant return types in all cases. For instance, assuming that two functions f and g have identical parameter types, the type of f will always be a subtype of the type of g if f returns int and g returns num.
This is not true for parameter types. In Dart 1, the function type subtype rule allows for covariant parameter types as well as contravariant ones, but strong mode and the upcoming Dart 2 require contravariance for parameter types. For instance, we have the following cases (using void for the return type, because the return type is uninteresting, it should just be the same everywhere):
typedef void F(num n); void f1(Object o) {} void f2(num n) {} void f3(int i) {} main() { F myF; myF = f1; // Contravariance: Succeeds in Dart 1, and in strong mode. myF = f2; // Same type: Always succeeds. myF = f3; // Covariance: Succeeds in Dart 1, but fails in strong mode. }
In all cases, the variance is concerned with the relationship between the type of the parameter for myF and the type of the parameter for the function which is assigned to myF. Since Dart 1 subtyping makes both f1 and f3 subtypes of the type of myF, all assignments succeed at run time (and static analysis proceeds without warnings). In strong mode and Dart 2, f3 does not have a subtype of the type of myF, so this is considered as a downcast at compile time, and it fails at runtime.
Contravariance is the sound rule that most languages use, so this means that function calls in strong mode and in Dart 2 are subject to more tight type checking, and some run-time errors cannot occur.
However, covariant parameter types can be quite natural and convenient, they just impose an obligation on developers to use ad-hoc reasoning in order to avoid the potential type errors at run time. The covariant overrides feature was added exactly for this purpose: When developers want to use unsound covariance, they can get it by requesting it explicitly. In the (vast majority of) cases where the sound and more strict contravariant rule fits the intended design, there will be no such request, and parameter type covariance (which would then presumably only arise by mistake) will be flagged as a type error.
In order to preserve a fundamental soundness property of Dart, the reified type of tear-offs of methods has parameter type Object for every parameter whose type is covariant. The desired property is that every expression with static type T must evaluate to a value whose dynamic type S which is a subtype of T. Here is an example why it would not work to reify the declared parameter type directly:
// Going by the OLD RULES, showing why we need to introduce new ones. typedef void F(num n); class A { // The reified parameter type is `num`, directly as declared. void f(covariant num n) {} } class B extends A { // The reified parameter type is `int`, directly as declared. void f(int i) {} } main() { A a = new B(); F myF = a.f; // Statically safe, yet fails at run time! }
The problem is that a.f has static type void Function(num), and if the reified type at run time is void Function(int) then a.f is an expression whose value at run time does not conform to the statically known type.
Even worse, there is no statically known type annotation that we can use in the declaration of myF which will make it safe—the value of a could be an instance of some other class C where the parameter type is double, and in general we cannot statically specify a function type where the parameter type is a subtype of the actual parameter type at runtime (as required for the initialization to succeed).
We could use the bottom type as the argument type, void Function(Null), but that makes all invocations unsafe (except myF(null)). We believe that it is more useful to preserve the information that “it must be some kind of number”, even though not all kinds of numbers will work. With Null, we just communicate that all invocations are unsafe, with no hints at all about which ones would be less unsafe than others.
We do not want any such expressions where the value is not a subtype of the statically known type, and hence the reified type of a.f is void Function(Object). In general, the type of each covariant parameter is reified as Object. In the example, this is how it works:
typedef void F(num n); class A { // The reified parameter type is `Object` because `n` is covariant. void f(covariant num n) {} } class B extends A { // The reified parameter type is `Object` because `i` is covariant. void f(int i) {} } main() { A a = new B(); F myF = a.f; // Statically safe, and succeeds at runtime. }
Note that an invocation of myF can be statically safe and yet fail at runtime, e.g., myF(3.1), but this is exactly the same situation as with the torn-off method: a.f(3.1) is also considered statically safe, and yet it will fail at runtime.
The purpose of this document is to cover one extra type of situation where the same typing situation arises.
Parameters can have a covariant type because they are or contain a formal type parameter of an enclosing generic class. Here is an example using the core class List (which underscores that it is a common phenomenon, but any generic class would do). It illustrates why we need to change the reified type of tear-offs also with parameters that are covariant due to class covariance:
// Going by the OLD RULES, showing why we need to introduce new ones. // Here is the small part of the core List class that we need here. abstract class List<E> ... { // The reified type is `void Function(E)` in all modes, as declared. void add(E value); // The reified type is `void Function(Iterable<E>)` in all modes, as declared. void addAll(Iterable<E> iterable); ... } typedef void F(num n); typedef void G(Iterable<num> n); main() { List<num> xs = <int>[1, 2]; F myF = xs.add; // Statically safe, yet fails at run time // in strong mode and Dart 2. G myG = xs.addAll; // Same situation as with myF. }
The example illustrates that the exact same typing situation arises in the following two cases:
int i in B.f).E value and Iterable<E> iterable in List.add resp. List.addAll).This document specifies how to preserve the above mentioned expression soundness property of Dart, based on a modified rule for how to reify parameter types of tear-offs. Here is how it works with the new rules specified in this document:
abstract class List<E> ... { // The reified type is `void Function(Object)` in all modes. void add(E value); // The reified type is `void Function(Object)` in all modes. void addAll(Iterable<E> iterable); ... } typedef void F(num n); typedef void G(Iterable<num> n); main() { List<num> xs = <int>[1, 2]; F myF = xs.add; // Statically safe, and succeeds at run time. G myG = xs.addAll; // Same situation as with myF. }
The grammar remains unchanged.
The static type of a property extraction remains unchanged.
The static type of a torn-off method is taken directly from the statically known declaration of that method, substituting actual type arguments for formal type parameters as usual. For instance, the static type of xs.addAll is void Function (Iterable<num>) when the static type of xs is List<num>. Note that this is significant because the reified types of some torn-off methods will indeed change with the introduction of this feature.
When we say that a parameter is covariant by modifier, we are referring to the definition of being a covariant parameter which is given in covariant overrides.
When a parameter p is covariant by modifier, there will necessarily be a declaration of a formal parameter p1 (which may be the same as p, or it may be different) which contains the built-in identifier covariant.
We need to introduce a new kind of covariant parameters, in addition to the ones that are covariant by modifier. To do that, we also need to refer to the variance of each occurrence of a type variable in a type, which is specified in the language specification.
Consider a class T which is generic or has a generic supertype (directly or indirectly). Let S be said generic class. Assume that there is a declaration of a method, setter, or operator m in S, that X is a formal type parameter declared by S, and that said declaration of m has a formal parameter x wherein X occurs covariantly or invariantly. In this situation we say that the parameter x is covariant by class covariance.
This means that the type annotation of the given parameter may actually be covariant in the relevant type parameter, or it may vary among types that have no subtype relationship to each other. The parameter will be called ‘covariant’ in both cases, because the situation where it is actually covariant is expected to be much more common than the situation where it varies among unrelated types.
When checking whether a given instance method declaration D1 is a correct override of another instance method declaration D2, it is ignored whether or not a formal parameter in D1 or D2 is covariant by class covariance.
This differs from the treatment of parameters which are covariant by modifier, where an overriding parameter type must be a subtype or a supertype of each overridden parameter type. In practice this means a parameter which is covariant by modifier may be specialized covariantly without limit, but a parameter which is covariant by class covariance must be overridden by a parameter with the same type or a supertype thereof, and it is only that type itself which “is covariant” (in the sense that clients know an upper bound T statically, and for the actual type S at run time it is only known that S <: T). Here is an example:
abstract class C<X> { void f1(X x); void f2(X x); void f3(covariant num x); void f4(X x); void f5(covariant X x); } abstract class D extends C<num> { void f1(num n); // OK void f2(int i); // Error: `num <: int` required, but not true. void f3(int i); // OK: covariant by modifier (only). void f4(covariant int i); // OK: covariant by modifier (and class). void f5(int i); // OK: covariant by modifier (and class). }
In the following, the phrase covariant parameter denotes either a parameter which is covariant by modifier, or a parameter which is covariant by class covariance.
We could have used ‘covariant by class covariance’ throughout, but for overall simplicity we make it explicit that the treatment of both kinds of covariant parameters is identical in the dynamic semantics.
The reified type for a function f obtained by a closurizing property extraction on an instance method, setter, or operator is determined as follows:
Let m be the name of the method, operator, or setter which is being closurized, let T be the dynamic type of the receiver, and let D be the declaration of m in T or inherited by T which is being extracted.
The reified return type of f the is the static return type of D. For each parameter p declared in D which is not covariant, the part in the dynamic type of f which corresponds to p is the static type of p in D. For each covariant parameter q, the part in the dynamic type of f which corresponds to q is Object.
The occurrences of type parameters in the types of non-covariant parameters (note that those occurrences must be in a non-covariant position in the parameter type) are used as-is. For instance, <String>[].asMap() will have the reified type Map<int, String> Function().
The dynamic checks associated with invocation of such a function are still needed, and they are unchanged.
That is, a dynamic error occurs if a method with a covariant parameter p is invoked, and the actual argument value bound to p has a run-time type which is not a subtype of the type declared for p.
The “erasure” of the reified parameter type for each covariant parameter to Object may seem aggressive.
In particular, it ignores upper bounds on the formal type parameter which gives rise to the covariance by class covariance, and it ignores the structure of the type where that formal type parameter is used. Here are two examples:
class C<X extends num> { void foo(X x) {} void bar(List<X> xs) {} }
With this declaration, the reified type of new C<int>().foo will be void Function(Object), even though it would have been possible to use the type void Function(num) based on the upper bound of X, and still preserve the earlier mentioned expression soundness. This is because all supertypes of the dynamic type of the receiver that declare foo have an argument type for it which is a subtype of num.
Similarly, the reified type of new C<int>().bar will be void Function(Object), even though it would have been possible to use the type void Function(List<num>).
Note that the reified type is independent of the static type of the receiver, so it does not matter that we consider new C<int>() directly, rather than using an intermediate variable whose type annotation is some supertype, e.g., C<num>.
In the first example, foo, there is a loss of information because we are (dynamically) allowed to assign the function to a variable of type void Function(Object). Even worse, we may assign it to a variable of type void Function(String), because void Function(Object) (that is, the actual type that the function reports to have) is a subtype of void Function(String). In that situation, every statically safe invocation will fail, because there are no values of type String which will satisfy the dynamic check in the function itself, which requires an argument of type int (except null, of course, but this is rarely sufficient to make the function useful).
In the second example, bar, the same phenomenon is extended a little, because we may assign the given torn-off function to a variable of type void Function(String), in addition to more reasonable ones like void Function(Object) , void Function(Iterable<Object>), and void Function(Iterable<int>).
It is certainly possible to specify a more “tight” reified type like the ones mentioned above. In order to do this, we would need the least upper bound of all the statically known types in all supertypes of the dynamic type of the receiver. This would involve a least upper bound operation on a set of types, and it would involve an instantiate-to-bounds operation on the type parameters.
The main problem with this approach is that some declarations do not allow for computation of a finite type which is the least upper bound of all possible instantiations, so we cannot instantiate-to-bound:
// There is no finite type `T` such that all possible values for `X` // and no other types are subtypes of `T`. class D<X extends D<X>> {}
Similarly, some finite sets of types do not have a denotable least upper bound:
class I {} class J {} class A implements I, J {} class B implements I, J {}
In this case both of A and B have the two immediate superinterfaces I and J, and there is no single type (that we can express in Dart) which is the least of all the supertypes of A and B.
So in some cases we will have to error out when we compute the reified type of a tear-off of a given method, unless we introduce intersection types and infinite types, or unless we find some other way around this difficulty.
On the other hand, it should be noted that the common usage of these torn-off functions would be guided by the statically known types, which do have the potential to keep them “within a safe domain”.
Here is an example:
main() { List<int> xs = <int>[]; void Function(int) f1 = xs.add; // Same type statically, OK at runtime. void Function(num) f2 = xs.add; // Statically a downcast, can warn, OK at runtime. void Function(Object) f3 = xs.add; // A downcast, can warn, OK at runtime. void Function(String) f4 = xs.add; // An unrelated type, error in strong mode. List<num> ys = xs; // "Forget part of the type". void Function(int) f5 = ys.add; // Statically an upcast, OK at runtime. void Function(num) f6 = ys.add; // Statically same type, OK at runtime. void Function(Object) f7 = ys.add; // Statically a downcast, OK at runtime. void Function(String) f8 = ys.add; // An unrelated type, error in strong mode. List<Object> zs = ys; void Function(int) f9 = zs.add; // Statically an upcast, OK at runtime. void Function(num) fa = zs.add; // Statically an upcast, OK at runtime. void Function(Object) fb = zs.add; // Statically same type, OK at runtime. void Function(String) fc = zs.add; // Finally we can go wrong silently! }
In other words, the static typing helps programmers to maintain the same level of knowledge (say, “this is a list of num”) consistently, even though it is consistently incomplete (“it's actually a list of int”), and this helps a lot in avoiding those crazy assignments (to List<String>) where almost all method invocations will go wrong.
Jun 1st 2018, version 0.6: Removed specification of variance, for which the normative text is now part of the language specification. Adjusted the wording to fit the slightly different definitions of variance given there. The meaning of this feature specification has not changed.
Feb 1st 2018, version 0.5: Added specification of override checks for parameters which are covariant from class.
Nov 24th 2017, version 0.4: Modified the definition of what it takes to be a covariant parameter: Some cases were previously incorrectly omitted.
Nov 11th 2017, no version number specified: Clarified examples.
Apr 21st 2017, no version number specified: Some typos corrected.
Feb 16th 2017, no version number specified: Initial version.