-
Notifications
You must be signed in to change notification settings - Fork 207
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
Add declaration-site variance feature specification #1230
base: main
Are you sure you want to change the base?
Conversation
*If _X_ has the variance modifier `inout` then there are no variance | ||
related restrictions on the positions where it can occur.* | ||
|
||
*For superinterfaces we need slightly stronger rules than the ones that |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'll relax this tomorrow, such that it matches the implementation.
_contravariant_ if it has the modifier `in`; and we say that it is | ||
_invariant_ if it has the modifier `inout`. | ||
|
||
The covariant occurrences of a type (schema) `T` in another type (schema) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This definition wigs me out a bit: I know what it's saying, but if I really get pedantic it's weird. It's basically computing a set which will have cardinality zero or one. That is, the base case says that S
is a covariant occurrence of T
(that is, they are same the type variable). Presumably we're meant to interpret this as a singleton set. But the only thing ever put in such as set is... T
. So all of the unions are either of empty sets, or of the same singleton set. So all this is computing is "yes this variable occurs" or "no it doesn't". So I think it would be better to phrase these as predicates: "We say that a type (schema) T
occurs covariantly in another type (schema) S
if: ...."
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I revised the definitions to make them use the same approach as the language specification. That would eliminate the need to make the notion of "an occurrence of a type" explicit.
|
||
- if `S` and `T` are the same type, | ||
- `S` is a covariant occurrence of `T`. | ||
- if `S` is `Future<U>` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Add S is U?
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, and the case where S
is X & S
. I'll go over the list of type forms.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Did that.
- the covariant occurrences of `T` in `U` | ||
- if `S` is `FutureOr<U>` | ||
- the covariant occurrencs of `T` in `U` | ||
- if `S` is an interface type `C<T0, ..., Tk>` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this is ok, but it feels slightly off to me that we don't consider an invariant occurrence to be both a covariant occurrence and an invariant occurrence. I think it works out with the way the definitions are used here? But it's worth double checking
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I suspect we could do both. The language specification defines that a type T
occurs covariantly in a type S
if every occurrence of T
in S
is covariant, so we'd need to say that it occurs covariantly and not invariantly, etc. I'll double check.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it's working (it's the same approach as in the language specification, and I think that's in a good shape).
|
||
It is a compile-time error if a variance modifier is specified for a type | ||
parameter declared by a static extension, a generic function type, a | ||
generic function or method, or a type alias. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Presumably allowed for enums (post enhanced enums)?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Agreed, we can have types E<T1>
and E<T2>
with T1 <: T2
, and we can have enum values with such types, so there is room for subtype relationships even though the enum declaration as such cannot be a superinterface of anything.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Added commentary to that effect.
every type argument associated with an extension method invocation is | ||
statically known at the call site. Similar reasons apply for functions and | ||
function types. Finally, the variance of a type parameter declared by a | ||
type alias is determined by the usage of that type parameter in the body of |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do these meaningfully have variance?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We have specified the variance of a type alias type parameter in this way, so
typedef F<X, Y> = X Function(Y);
has a covariant type parameter followed by a contravariant type parameter. I would assume that we just keep doing that.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I made it more explicit that the notion of the variance of a type parameter of a type alias is unchanged.
of _F_ (*with no constraints on other occurrences*), or if it occurs both | ||
covariantly and contravariantly. | ||
|
||
*In particular, an unused type parameter is considered covariant.* |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What does this mean? Usually I think of variance as specifying the subtyping relation. But given typedef F<X> = int
, I expect that F<num> <: F<double>
and F<double> <: F<num>
, so in what sense is X
covariant?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thinking about this again, I noticed that we don't have any equivalence of this kind. The unused type variable is handled in the few situations where that is needed, because a rule applies to, e.g., any non-contravariant type variable, and that includes both unused, invariant, and covariant ones.
``` | ||
|
||
*In a superinterface, a type parameter without a variance modifier can be | ||
used in an actual type argument for a parameter with a variance modifier, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Worth making it explicit that this is subject to the checks above, which de facto means that the vice versa only allows the "explicitly covariant or invariant to implicitly covariant" cases? That is, class C<in X> implements List<X>
is a no-no, right?
And don't we have the "twisted super-hierarchy" problem to deal with here too, so we have to outlaw "class C implements Contra, Invariant"?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
And don't we have the "twisted super-hierarchy" problem to deal with here too, so we have to outlaw "class C implements Contra, Invariant"?
On further thought, this is I think disallowed by our existing super-interface check, but probably worth pointing that out here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I added a separate section about the dynamic checks.
|
||
If _X_ has the variance modifier `out` then it is a compile-time error for | ||
_X_ to occur in a non-covariant position in a member signature in the body | ||
of _D_, except that it is not an error if it occurs in a covariant position |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Only covariant? Or also invariant?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As soon as we have a dynamic type check on the actual argument it is of course sound with respect to the execution of the function body, so we can just allow the declared type to be anything the developer wants, no limits.
However, we have maintained a certain level of discipline so far: A covariant parameter should have a declared type in the dynamic type of the receiver which is a subtype or a supertype of the statically known declared type. With invariant positions I'd expect that we allow unrelated types.
I did think about this, but I haven't changed anything yet.
|
||
If _X_ has the variance modifier `in` then it is a compile-time error for | ||
_X_ to occur in a non-contravariant position in a member signature in the | ||
body of _D_, except that it is not an error if it occurs in a contravariant |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
or invariant?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Same as line 200.
|
||
When a legacy library _L_ imports a library _L2_ with sound variance, the | ||
declarations imported from _L2_ are _legacy erased_. This means that all | ||
variance modifiers in type parameter declarations are ignored. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does this work out? Doesn't this mean I can recreate your "twisted hierarchy" soundness bug by viewing a contravariant class from a legacy library?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I changed this to say that the legacy library simply gets the declaration-site based subtype relationships whenever it refers to types that involve declarations using declaration-site variance. Surely that's not only simpler, it is also much more useful.
I haven't written anything about the management of breakage associated with corelib changes.
9b92852
to
b944a7b
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Review response.
_contravariant_ if it has the modifier `in`; and we say that it is | ||
_invariant_ if it has the modifier `inout`. | ||
|
||
The covariant occurrences of a type (schema) `T` in another type (schema) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I revised the definitions to make them use the same approach as the language specification. That would eliminate the need to make the notion of "an occurrence of a type" explicit.
|
||
- if `S` and `T` are the same type, | ||
- `S` is a covariant occurrence of `T`. | ||
- if `S` is `Future<U>` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, and the case where S
is X & S
. I'll go over the list of type forms.
- the covariant occurrences of `T` in `U` | ||
- if `S` is `FutureOr<U>` | ||
- the covariant occurrencs of `T` in `U` | ||
- if `S` is an interface type `C<T0, ..., Tk>` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I suspect we could do both. The language specification defines that a type T
occurs covariantly in a type S
if every occurrence of T
in S
is covariant, so we'd need to say that it occurs covariantly and not invariantly, etc. I'll double check.
|
||
It is a compile-time error if a variance modifier is specified for a type | ||
parameter declared by a static extension, a generic function type, a | ||
generic function or method, or a type alias. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Agreed, we can have types E<T1>
and E<T2>
with T1 <: T2
, and we can have enum values with such types, so there is room for subtype relationships even though the enum declaration as such cannot be a superinterface of anything.
|
||
It is a compile-time error if a variance modifier is specified for a type | ||
parameter declared by a static extension, a generic function type, a | ||
generic function or method, or a type alias. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Added commentary to that effect.
of _F_ (*with no constraints on other occurrences*), or if it occurs both | ||
covariantly and contravariantly. | ||
|
||
*In particular, an unused type parameter is considered covariant.* |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thinking about this again, I noticed that we don't have any equivalence of this kind. The unused type variable is handled in the few situations where that is needed, because a rule applies to, e.g., any non-contravariant type variable, and that includes both unused, invariant, and covariant ones.
|
||
If _X_ has the variance modifier `out` then it is a compile-time error for | ||
_X_ to occur in a non-covariant position in a member signature in the body | ||
of _D_, except that it is not an error if it occurs in a covariant position |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As soon as we have a dynamic type check on the actual argument it is of course sound with respect to the execution of the function body, so we can just allow the declared type to be anything the developer wants, no limits.
However, we have maintained a certain level of discipline so far: A covariant parameter should have a declared type in the dynamic type of the receiver which is a subtype or a supertype of the statically known declared type. With invariant positions I'd expect that we allow unrelated types.
I did think about this, but I haven't changed anything yet.
|
||
If _X_ has the variance modifier `in` then it is a compile-time error for | ||
_X_ to occur in a non-contravariant position in a member signature in the | ||
body of _D_, except that it is not an error if it occurs in a contravariant |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Same as line 200.
``` | ||
|
||
*In a superinterface, a type parameter without a variance modifier can be | ||
used in an actual type argument for a parameter with a variance modifier, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I added a separate section about the dynamic checks.
|
||
When a legacy library _L_ imports a library _L2_ with sound variance, the | ||
declarations imported from _L2_ are _legacy erased_. This means that all | ||
variance modifiers in type parameter declarations are ignored. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I changed this to say that the legacy library simply gets the declaration-site based subtype relationships whenever it refers to types that involve declarations using declaration-site variance. Surely that's not only simpler, it is also much more useful.
I haven't written anything about the management of breakage associated with corelib changes.
This PR adds a feature specification for declaration-site variance, which is a sound and explicit mechanism for specifying that a type parameter of a generic class can be covariant (marked by
out
), invariant (inout
), or contravariant (in
), cf. #524.