Rewrite the exhaustiveness specification. #2948
Conversation
This is based on Johnni's excellent implementation. I tried to follow the semantics of the implementation as closely as I could, and mostly stuck to the terminology too. The main change is that the implementation uses "type" to also sort of do some restriction stuff, and I tried to keep that separate here such that a "type" on a space always refers to a static type.
|
|
||
| 3. Otherwise, we're intersecting two object spaces. | ||
| The *overapproximation* of a type `T` is `T` with all type variables replaced | ||
| with their *defaults*: |
There was a problem hiding this comment.
I think this is slightly underdefined.
I think we only apply "overapproximation" to class, mixin and enum declarations. So say that.
(It gets weird if we try to replace type variables of a generic function type.)
We can always extend it to apply to the type of such a declaration by going from the type to the declaration.
Also, we should probably say that we apply it to the declaration, not the type.
(Types do not have type variables or bounds, their declarations - and, depending on mood, their generic classes and interfaces, which are still different from the types - do. The types have type arguments, but the variables are long gone.)
So, given a generic enum, mixin or class declaration, instantiate its type with the default types for its declaration's type parameters.
But that's basically what "instantiate to bounds" (I2B) does, giving you a valid super-bounded supertype for all valid instantiations, so maybe just use that?
(I2B also accounts for bound expressions that aren't straight-up types, up-to and including F-bounded type parameters. Can't just use a bound as a type directly.)
There was a problem hiding this comment.
I tend to think of this as "recursively instantiate to bounds" and it is slightly different that I2B. I2B works on raw types whereas the overapproximation works on instantiated types.
For instance the overapproximation of Map<K, Map<V, K Function(K)>>> in:
method<K extends num, V extends Foo<V>>(Map<K, Map<V, K Function(K)>>> map) => switch (map) { ... };
is Map<num, Map<dynamic, num Function(Never)>>>, so that each type variable occurring in the type has been replaced with the I2B default type modulo variance.
There was a problem hiding this comment.
Reworded to make it clearer that it applies to declarations.
I didn't quite follow Johnni's answer, but I trust that it makes sense and is sufficiently compelling to you, Lasse. :D
There was a problem hiding this comment.
I'm not sure I follow it either, but that could be because I don't actually understand I2B.
Or what is being attempted here.
So let me try again:
Given a static type (which may contain free type variables referencing surrounding declarations),
take each such occurrence of a free type variable in the type, and replace it with its default type which is:
- If the referenced type variable has a bound, the default is the overapproximation of that bound.
- Otherwise if the free type variable occurs covariantly, the default is
Object?. - Otherwise the default is
Never
The resulting type has no free type variables and will be a valid super-bounded type.
... But it's not valid super-bounded. If the variable has a bound with other free type variables, the first variable occurs contravariantly, we need an underapproximation to use instead.
And what if it occurs invariantly, like List<void Function<X extends T>(X)>?
I think it can make sense to talk about type variables in static types (I'm just not used to doing so), but I think here are more details to handle, if the goal is to get a valid super-bounded type as result.
|
|
||
| 2. Otherwise, go through the fields. If the intersection of any | ||
| corresponding pair of fields is empty, then `I` is empty. | ||
| 2. Otherwise, the default is the bound if there is one. |
There was a problem hiding this comment.
class C<T, S extends T, R extends List<T>> {} has bound declarations, but not bound types.
Use I2B, it's good for you.
There was a problem hiding this comment.
I don't understand the distinction you're making here, sorry. Can you explain, or did Johhni's explanation of how overapproximation differs from I2B address this?
There was a problem hiding this comment.
The result of the "default" here is a type, but it works on a type variable declaration.
The bound of a type variable is a type expression which can have free type variables, so you cannot use the bound as a type without instantiating those type variables.
For the declaration class C<T, S extends T, R extends List<T>> {},
the line above says that the default of S is T, but T is an uninstantiated type variable, which is not a type until we know what T is.
As written, taken literally, the overapproximation of C here would be C<Object?, T, List<T>>, with no clue to what T is.
Now, we could use the type found for the T parameter to instantiate the other Ts, but that requires finding the dependency ordering between type variables, instantiating the roots, the propagating that to the other ones and instantiating those in turn.
Possible, and something I think I2B already does for you.
(But I could also be completely off, check my comment in the thread where Johnni commented.)
|
I'm going to go ahead and land this but I'm happy to iterate on it more if there are other changes to make. |
| *After the first case, we know that if `a` is a `B` or `D` then we will have | ||
| thrown an exception. But if `a` is a `C`, it may not have matched if the | ||
| field isn't `0`. So the space for the first case is a union of `B|C(field: | ||
| 0)|D'.* |
| class Animal {} | ||
| class Mammal extends Animal {} | ||
| 1. For each declaration `C` in the library of `D` that has `D` in an | ||
| `implements`, `extends`, or `with` clause: |
There was a problem hiding this comment.
After thinking more I think we also do need to say something about on types.
sealed class S {}
class A extends S {}
mixin _Gotcha on S {}
class B implements _Gotcha {}Here B does not have S as direct superdeclaration, and _Gotcha is not included in
"implements, extends, or with clause:", so B is unaccounted for an:
S s = B();
int r = switch (s) {
A() => 42;
};
print(r);should cause some soundness concerns.
Now, what should we say?
- You cannot have a sealed type as
ontype? - You cannot implement a mixin which has a sealed type as
ontype? (not quite "must bebase" because it's not transitive. If you apply the mixin, implementing the interface of the mixin application class is fine.) - You can't implement mixins? (Deity yes, please!)
(The current implementation does include _Gotcha in the exhaustion-set.)
|
|
||
| 2. Otherwise, go through the fields. If the intersection of any | ||
| corresponding pair of fields is empty, then `I` is empty. | ||
| 2. Otherwise, the default is the bound if there is one. |
There was a problem hiding this comment.
The result of the "default" here is a type, but it works on a type variable declaration.
The bound of a type variable is a type expression which can have free type variables, so you cannot use the bound as a type without instantiating those type variables.
For the declaration class C<T, S extends T, R extends List<T>> {},
the line above says that the default of S is T, but T is an uninstantiated type variable, which is not a type until we know what T is.
As written, taken literally, the overapproximation of C here would be C<Object?, T, List<T>>, with no clue to what T is.
Now, we could use the type found for the T parameter to instantiate the other Ts, but that requires finding the dependency ordering between type variables, instantiating the roots, the propagating that to the other ones and instantiating those in turn.
Possible, and something I think I2B already does for you.
(But I could also be completely off, check my comment in the thread where Johnni commented.)
|
|
||
| 3. Otherwise, we're intersecting two object spaces. | ||
| The *overapproximation* of a type `T` is `T` with all type variables replaced | ||
| with their *defaults*: |
There was a problem hiding this comment.
I'm not sure I follow it either, but that could be because I don't actually understand I2B.
Or what is being attempted here.
So let me try again:
Given a static type (which may contain free type variables referencing surrounding declarations),
take each such occurrence of a free type variable in the type, and replace it with its default type which is:
- If the referenced type variable has a bound, the default is the overapproximation of that bound.
- Otherwise if the free type variable occurs covariantly, the default is
Object?. - Otherwise the default is
Never
The resulting type has no free type variables and will be a valid super-bounded type.
... But it's not valid super-bounded. If the variable has a bound with other free type variables, the first variable occurs contravariantly, we need an underapproximation to use instead.
And what if it occurs invariantly, like List<void Function<X extends T>(X)>?
I think it can make sense to talk about type variables in static types (I'm just not used to doing so), but I think here are more details to handle, if the goal is to get a valid super-bounded type as result.
This is based on Johnni's excellent implementation. I tried to follow the semantics of the implementation as closely as I could, and mostly stuck to the terminology too. The main change is that the implementation uses "type" to also sort of do some restriction stuff, and I tried to keep that separate here such that a "type" on a space always refers to a static type.
I'm sure there are some mistakes here (but I of course don't know where they are). I imagine it will take some iteration between the implementation, the spec, and the tests before they settle on some kind of fixpoint. But this should hopefully be enough to start writing some co19 tests.
cc @sgrekhov