Safe typing involving variance

[eernstg]

In Dart, a parameterized class type is covariant in every type parameter; for example, List<int> is a subtype of List<num> because int is a subtype of num (so the list type and its type argument "co-vary").

This is sound for all covariant occurrences of such type parameters in the class body (for instance, the getter first of a list has return type E, which is sound). It is also sound for contravariant occurrences when a sufficiently exact receiver type is known (e.g., for a literal like <num>[].add(4.2), or for a generative constructor SomeClass<num>.foo(4.2)).

However, in general, every member access where a covariant type parameter occurs in a contravariant position may cause a dynamic type error, because the actual type annotation at run time—say, the type of a parameter of a method—is a subtype of the one which is known at compile-time.

For example: Assume that a variable xs has declared type List<num>, and consider the invocation xs.add(4.2). This invocation will fail if the value of xs is a List<int>, but it will succeed with a List<num> and with a List<double>. Still, the static type of xs allows them all.

This issue is a request for improvements in the amount of control that developers have over this kind of dynamic checks. In particular, it should be possible to establish a guarantee at compile time that such a dynamic type error cannot occur.

[leafpetersen]

@munificent and I discussed the use site and declaration site variance ideas on the board today, I wanted to record a few thoughts.

We both had the sense that declaration site co and contra-variance are probably useful.

We discussed the question of whether or not to allow a class with invariant type parameter T to use that type parameter in an unsound covariant position. For example:

class C<invariant T> extends List<T> { ...}

I think it's reasonable to allow, but there is something distasteful about it. We both had the thought that perhaps one could require instead that the superclass be the invariant projection, to mark the fact that there is a transition from the statically safe to the statically unsafe space.

class C<invariant T> extends List< exactly T> { ...}

I don't think this actually has any practical effect on how this class is used, since List<exactly T> <: List<T>, but it does make it explicit that you are using an unsafe super class via a projection.

Where this becomes especially interesting is if you add the covariant projections as well, since you could then extend only the soundly covariance projection of an unsound type like List.

class C<invariant T> extends List<out T> { ...}

My expectation would be that in general we would have:

A<exactly T> <: A<T>
A<exactly T> <: A<out T>
A<T> <: A<out T>

So extending List<out T> here instead of just List<T> actually provides something useful: it restricts you to the soundly covariant subset of the methods of List. If the projection is reified as part of the super-interfaces, then this becomes even runtime sound, since C<int>() as List<int> would be a failed cast.

Does this make any sense? Something worth exploring?

[He-Pin]

I more like the Scala one. with List<+T> and Actoref<-T>

[mateusfccp]

I know the current focus of the team is null-safety, but was there any progress on this?

[eernstg]

It would not be unlikely that we will add sound declaration site variance; much of it is implemented. But no firm dates yet, and not even a firm promise that we will do it.

[mateusfccp]

Thanks for your answer. I am actually trying to implement a reader monad, but can't do something like:

class Functor<A> {}

class Reader<A, B> implements Functor<B Function(A)> {}

This is the error I'm getting:

'A' can't be used contravariantly or invariantly in 'Functor<B Function(A)>'.
Try not using class type parameters in types of formal parameters of function types, nor in explicitly contravariant or invariant superinterfaces.

I think this issue would solve my problem, so I would really appreciate if you consider implementing this.

Also, AFAIK, there's no workaround for what I am trying to do...

[eernstg]

If you're aiming at something similar to this Functor in Scala then you'd need higher-order type parameters. Dart doesn't have that, and is not likely to get it. But you can certainly make the Functor and Reader you mention type correct, for instance:

class Functor<out A> {}
class Reader<in A, out B> implements Functor<B Function(A)> {}

[mateusfccp]

I see, didn't know about these in and out keywords. Thanks for your help, @eernstg.

[eernstg]

The in out and inout keywords are not available in Dart today, they are part of the declaration-site variance feature, and that feature hasn't been released yet.