Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Compute a sound type for "contravariant members" #297

Open
eernstg opened this issue Apr 3, 2019 · 0 comments
Open

Compute a sound type for "contravariant members" #297

eernstg opened this issue Apr 3, 2019 · 0 comments
Labels
feature Proposed language feature that solves one or more problems

Comments

@eernstg
Copy link
Member

eernstg commented Apr 3, 2019

In response to #296, this issue is a proposal for how to compute a sound type for devariant members of a class type.

For the motivation and some examples, please consult #296.

This proposal simply specifies how to compute a sound type for a class member of the kind that we have called a "contravariant member" in earlier discussions about this topic. At the same time, this proposal introduces the new name devariant member for such members, in order to emphasize that contravariance as well as invariance requires a novel approach when it comes to covariant type parameters, and in case we add support for contravariant type parameters we will need to use a similar approach for covariant and invariant occurrences. In this proposal, it is assumed that a type parameter can be contravariant, because that's a tiny generalization and it might be useful enough to happen.

Note that this proposal specifies how to compute the type of a member as a whole, e.g., both the return type and the type of each formal parameter for a method, but it may be relevant to use just part of such a type. For instance, we may choose to use just the return type of a method obtained as specified here, and then use parameter types obtained differently.

We focus on the approach where the complete signature of each member is specified, and it is then a trivial matter to extract parts of the type as needed, or to compute just the parts which are needed.

For reasons why we might want to do this, please check the discussion at the end.

Proposal

Let C be a generic class, let X be a type parameter of C which is not declared invariant (cf. #214), and let m be a member of the interface of C. Let F be the function type of m if m is not a getter, and let F be the return type of m if m is a getter.

This covers instance variables as well, because an instance variable T x implicitly induces a getter and, if not final, a setter. Note that nothing is said about constructors, because they are not subject to variance; and nothing is said about static members, because they cannot have type parameters of their enclosing class in their signature.

We say that m is a devariant member of C with respect to X if and only if

  • X is covariant, and X occurs in F in a contravariant position and/or in an invariant position, or
  • X is contravariant, and X occurs in F in a covariant position and/or in an invariant position.

Let m be a member of a class C. We say that m is a devariant member of C if there exists a type parameter X declared by C, such that m is devariant with respect to X.

Let C be a generic class and m a member of the interface of C. Let T of the form C<T1 .. Ts> be a parameterized type with no compile-time errors. (In particular, C has s type parameters and the actual type arguments do not violate the declared bounds.) Assume that the type variables declared by C are X1 .. Xs.

The notation [T1/X1 .. Ts/Xs]F denotes a non-capturing substitution operation whereby all occurrences of Xj in F are replaced by Tj, for all j in 1 .. s. We introduce a new substitution operator here, in order to handle devariant members.

We define the variance aware substitution operator [T1,S1/X1 .. Ts,Ss/Xs]var as follows: It is non-capturing, just like the regular substitution operator, and it replaces each covariant occurrence of Xj by Tj and each contravariant occurrence of Xj by Sj.

If there exists a type parameter Xj which occurs invariantly in F, then replace F by the least upper bound of [Never/Xj]F and [Bj/Xj]F, where Bj is the declared bound of Xj. (This is a type which is a supertype of all types obtained by choosing a value for Xj, and it does not contain Xj itself.) Repeat this step until no type parameter occurs invariantly in F.

For j in 1 .. s, if Xj is covariant then let Uj be Tj and let Vj be Null; if Xj is contravariant then let Uj be Object and let Vj be Tj; and if Xj is neither covariant nor contravariant (in particular, if Xj is declared invariant) then let both Uj and Vj be Tj. Then:

  • if m is a non-getter member of C then the function type of m for a receiver of type T is [U1,V1/X1 .. Us,Vs/Xs]var F, where F is the function type of m.

  • if m is a getter which is a member of C with return type F, then the return type of m for a receiver of type T is [U1,V1/X1 .. Us,Vs/Xs]var F.

In the case where T is of the form C<invariant? T1 .. invariant? Ts> where one or more of the actual type arguments have been marked as invariant (cf. #229), the corresponding member types are computed in the same manner, except that each type parameter which corresponds to an actual type argument marked invariant is considered to have no variance (that is, it is not covariant and it is not contravariant).

Discussion

It is easy to verify that this produces the same type for any non-devariant member as the existing approach (which is directly substituting the actual type arguments for the formal type parameters), that the resulting typing for a devariant member is a supertype of the type which is achieved with the current approach, and also that this is a sound approximation.

The chosen approach for type parameters that occur in an invariant position in the member signature makes the choice to weaken the type to a supertype that does not depend on the type variable. It would also be possible to weaken all function types to Function and all non-function type to Object, which might be preferable if we consider the least upper bound operation to be a little bit too confusing. This would immediately address the concern that the elimination of type parameters that occur invariantly may not be confluent (so different orderings could produce different results).

We will need to introduce some exceptions, because we are already dealing with the devariance problem in other ways:

For methods that have parameters which are covariant-by-class (e.g., List.add), we will probably still check actual arguments according to the type obtained by simple substitution, and rely on a dynamic check of the type of the actual argument in the body of the method. Similarly, we will probably continue to give the tear-off of such a method the same type as today (by simple substitution), and let the thus obtained function object have a reified type which is Object for the parameters which are covariant-by-class.

The point is that general function type subtyping and method overriding are different: With a first class function of type S Function(T) it is probably common to use a "dummy" function of type S Function(dynamic), or at least a function of type S Function(T1) where T1 is some supertype of T, because such a function is already available, and its body "does not need to know everything" about its argument. In contrast, it is probably quite rarely the case that a method accepting an argument of type T is overridden by a method accepting an argument of type dynamic, or even any supertype T1 of T, because it is not so common to have an overriding method that does not need to know as much about its arguments as the overridden methods did. This means that the statically known argument type for a method is relevant to the call site, even though it is statically known that it is not sound, and even though it is technically possible that the type which is actually required by the callee is some supertype-of-a-subtype (that is, it could be anything whatsoever).

However, the situation where we invoke an instance method that has one or more parameters which are covariant-by-class may be less common in the future, because we would be able to use invariant modifiers on type parameter declarations and/or type arguments (#214, #229), and thus eliminate the variance on many more type arguments than what's currently possible. A tear-off of such a receiver would then not have to erase any parameter types to Object, because the precise type can be expressed locally and usages can be type checked statically. This would be particularly helpful for method signatures involving invariant occurrences of type variables.

However, for such tear-offs it should be noted that it would be more consistent and it would be sound (that is, there would not be a need for dynamic checks on parameters that are covariant by class in the body of a tear-off) if we used the proposal in this issue to compute the static type of such a tear-off, and we use the actual value of the given type variables to compute the reified type of the function object, and then we use static typing plus an additional entry point ("callAndCheckParameters") of the function object for every invocation which is not statically safe. So it would be nice, if we can tolerate the breakage.

It should also be noted that there is a usability issue connected with these two approaches to typing: Consider the following situation:

main() {
  List<num> xs;
  ...
  xs.add(e); // Static type of `e` is `T`.
}

With the current typing, it is a compile-time error if T is not assignable to num, which means that downcasts to num are accepted silently, and so are "upcasts to num". The latter is misleading, of course, because the actual dynamic check will be that e is S where S is some subtype of num, so there is no reason to expect this to be a downcast, it's just a cast (for instance, if S is int and the value of e has type double then the cast will fail, and it's not a downcast). With --no-implicit-casts we will accept arguments whose static type is a subtype of num and reject supertypes.

Nevertheless, rejecting e with a static type which is unrelated to num is more informative than just noting that the statically safe approximation to the actual argument type is Null, and anything else than that needs a dynamic check.

This is because we know that the actual type argument S for xs (which is also the argument type for add) is a subtype of num, which means that it is known that an argument of type String cannot possibly succeed (unless the value is null), and for other types it is arguably less likely that a cast from an arbitrary type to another arbitrary type will succeed than it is that a cast between two subtypes of the statically known upper bound of S will succeed.

Should we then, somehow, include the type obtained by simple substitution in the static analysis of devariant members? If we consider a receiver c with static type C<T> then the value returned by its f getter will be a function of type void Function(T1) for some type T1 which is a supertype of some type T2 which is the actual type argument at C of the dynamic type of c. This is already flexible enough to make it difficult to justify any other typing than one that says "T1 is a supertype of Null". So when it comes to returned results (from getters and methods) it is not likely to be useful to try to use the results from direct substitution (that is, today's typing). It is only the treatment of parameters of instance members which is likely to be more useful when we preserve the results from direct substitution.

This seems to indicate that we could use the types computed as specified here for return types (of getters and methods), and we could consider allowing them to be used for tear-offs of devariant members. (Say, we could allow the tear-off to produce a function object that admits static typing: With no dynamic type checks in the body of the main entry point, and with a reified type which is precisely as declared).

We may then be able to rely on invariant modifiers on types to reduce the number of occurrences of devariant method invocations, such that the non-homogeneous treatment of parameters that are covariant-by-class will only play a small role.

@eernstg eernstg added the feature Proposed language feature that solves one or more problems label Apr 3, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature Proposed language feature that solves one or more problems
Projects
None yet
Development

No branches or pull requests

1 participant