[Patterns] Should List and/or Map patterns be considered for exhaustiveness?

[leafpetersen]

The patterns proposal lists a small set of types which are considered for exhaustiveness:

bool
Null
A enum type
A type whose declaration is marked sealed
T? where T is exhaustive
FutureOr<T> for some type T that is exhaustive
A record type whose fields are all exhaustive types

List and Map are not included in this list, which suggests that code like the following will not be considered for exhaustiveness checking:

switch([3]) {
  [] => "Empty",
  [var x, ...] =>  "$x"
}

I believe the code above will be considered an error, since there is no default, and the type in question is not an exhaustive type.

Should we include List and Map as exhaustive types? The code above seems like really good code to allow. On the other hand, List and Map are not sealed types, so we probably (possibly?) don't want to require full exhaustiveness:

class MySpecialList() implements List<int> {...}
switch([3]) {
   case MySpecialList(): print("Special List");
}

Should we treat List (and possibly Map) as types which are exhaustive types only WRT to length? That is, we require that all lengths are covered, but not necessarily all subtypes? And if so, to what extent do we generalize this to explicit calls to the length getter, as opposed to only considering explicit patterns. Does the following get an exhaustiveness error?

switch([3]) {
  List(length: <1) => "Empty",
  [var x, ...] =>  "$x"
}

This would seem to start to require more reasoning about integers than we necessarily want to do.

Perhaps the correct way to think about this is to separate out what we can show to be exhaustive from what we require to be exhaustive? That is, we say:

• A switch statement is required to be exhaustive (and hence is only checked for exhaustiveness) only if the scrutinee has an exhaustive type as defined above.
• A switch expression is always required to be exhaustive, and is always checked for exhaustiveness
• Exhaustiveness checking may take into account more than just the set of exhaustive types, and hence there will be switch expressions which are proved exhaustive which would not be considered for exhaustiveness checking as switch statements.

For flow analysis and type inference, we have proposed that reachability for switch statement be driven entirely based on whether or not the type of the scrutinee is an exhaustive type (or if there is an explicit default). This would imply that there are switch statements which will be assumed to be non-exhaustive, but which are in fact exhaustive, and could be proven so if turned into switch statements.

Example:

class A {
  final bool value;
  A(this.value);
}
void test(A a) {
  int x;
  // A is not an exhaustive type, so this switch is assumed to be non-exhaustive
  switch(a) {
    case A(value:true): x = 0;
    case A(value:false): x = 1;
  }
  x.isEven; // Error, x is not definitely assigned
}
void test(A a) {
  int x;
  (switch(a) {
    A(value:true) => x = 0,
    A(value:false) => x = 1
  })
  x.isEven; // Ok, x is definitely assigned.
}

cc @munificent @eernstg @lrhn @kallentu @natebosch @jakemac53 @stereotype441 @johnniwinther

[munificent]

• A switch statement is required to be exhaustive (and hence is only checked for exhaustiveness) only if the scrutinee has an exhaustive type as defined above.
• A switch expression is always required to be exhaustive, and is always checked for exhaustiveness

This is actually what the proposal currently states, but it's not worded very clearly. It says:

• It is a compile-time error if the cases in a switch expression are not
  exhaustive. Since an expression must yield a value, the only other option
  is to throw an error and most Dart users prefer to catch those kinds of
  mistakes at compile time.

• It is a compile-time error if the cases in a switch statement or switch
  collection element are not exhaustive and the static type of the matched
  value is an exhaustive type.

Note that the first bullet point makes no mention of whether the matched value type is an exhaustive type or not. That means switch expressions must always be exhaustive regardless of the type you're matching on.

I'll add some clarification.

• Exhaustiveness checking may take into account more than just the set of exhaustive types, and hence there will be switch expressions which are proved exhaustive which would not be considered for exhaustiveness checking as switch statements.

Yes, we will define exhaustiveness for all types. The "exhaustive types" part of the proposal has only one purpose: if defines (by negation) the set of types you can switch on in a switch statement that don't lead to a compile time error if the switch isn't exhaustive. "Exhaustive type" is probably a confusing choice of term, but it was the first one that came to mind. I'll see if I can come up with something better. Maybe "statement-exhaustive type" or something?

[munificent]

On the other hand, List and Map are not sealed types, so we probably (possibly?) don't want to require full exhaustiveness:

class MySpecialList() implements List<int> {...}
switch([3]) {
   case MySpecialList(): print("Special List");
}

In switch expressions, we do want full exhaustiveness and this switch isn't exhaustive.

Should we treat List (and possibly Map) as types which are exhaustive types only WRT to length? That is, we require that all lengths are covered, but not necessarily all subtypes?

I think it would be good to require that all subtypes be covered too, which, if you have a list pattern or match on List (and not MySpecialList) should give you that. Unless there's something else you're thinking about that I'm missing.

This would seem to start to require more reasoning about integers than we necessarily want to do.

I would be happy to have exhaustiveness be able to reason about integer ranges and use that for length checks in list patterns too. It would be very cool if exhaustivess was smart about relational patterns on integer types. But if we can't make that work, it's not the end of the world either.

Right now, exhaustiveness is just not fleshed out at all for lists. I think there's a big TODO in the proposal for it.

[eernstg]

I think exhaustiveness for lists (and maps) would have to use an irrefutable case (default:, case _:, case var v:). For example, an instance of type List whose length is -1 would not match any list pattern (respectively map pattern).

Those lists (maps) would of course be "bad", but exhaustiveness is used in flow analysis and hence it must be sound. I'd think this means that exhaustiveness for lists and maps is trivial, but it always relies on a catch-all case.

[leafpetersen]

On the other hand, List and Map are not sealed types, so we probably (possibly?) don't want to require full exhaustiveness:

class MySpecialList() implements List<int> {...}
switch([3]) {
   case MySpecialList(): print("Special List");
}

In switch expressions, we do want full exhaustiveness and this switch isn't exhaustive.

Should we treat List (and possibly Map) as types which are exhaustive types only WRT to length? That is, we require that all lengths are covered, but not necessarily all subtypes?

I think it would be good to require that all subtypes be covered too, which, if you have a list pattern or match on List (and not MySpecialList) should give you that. Unless there's something else you're thinking about that I'm missing.

I'm not sure what you're saying here. Which of the following non-exhaustive statements do you propose should be errors/not errors?

switch([3]) {
    case MySpecialList(): print("Special List");
 }

switch(<Object>[3]) {
    case List<int>(): print("List of int");
 }

switch([3]) {
    case []: print("Empty");
 }

[munificent]

I think exhaustiveness for lists (and maps) would have to use an irrefutable case (default:, case _:, case var v:). For example, an instance of type List whose length is -1 would not match any list pattern (respectively map pattern).

Ah right. Paul mentioned that recently too. Filed an issue: #2701

Those lists (maps) would of course be "bad", but exhaustiveness is used in flow analysis and hence it must be sound. I'd think this means that exhaustiveness for lists and maps is trivial, but it always relies on a catch-all case.

I'd like to avoid requiring a pointless default case for lists, but I agree that whatever we do of course must be sound.

I'm not sure what you're saying here. Which of the following non-exhaustive statements do you propose should be errors/not errors?

switch([3]) {
    case MySpecialList(): print("Special List");
 }

switch(<Object>[3]) {
    case List<int>(): print("List of int");
 }

switch([3]) {
    case []: print("Empty");
 }

I think none of those should be compile-time errors because they are switch statements. If they were switch expressions, they all would be. In other words, I don't think lists should be an always-exhaustive type.

[leafpetersen]

I think none of those should be compile-time errors because they are switch statements. If they were switch expressions, they all would be. In other words, I don't think lists should be an always-exhaustive type.

This matches my understanding, but I was confused by:

I think it would be good to require that all subtypes be covered too, which, if you have a list pattern or match on List (and not MySpecialList) should give you that. Unless there's something else you're thinking about that I'm missing.

Maybe you were moving back to switch expressions here? Which again comes back to the main clarification which I take out of this issue, which is that:

• Exhaustiveness checking may take into account more than just the set of exhaustive types, and hence there will be switch expressions which are proved exhaustive which would not be considered for exhaustiveness checking as switch statements.

[munificent]

Re-opening because I missed your last example which is a really interesting one:

Example:

class A {
  final bool value;
  A(this.value);
}
void test(A a) {
  int x;
  // A is not an exhaustive type, so this switch is assumed to be non-exhaustive
  switch(a) {
    case A(value:true): x = 0;
    case A(value:false): x = 1;
  }
  x.isEven; // Error, x is not definitely assigned
}

I suspect that users will be surprised that x isn't definitely assigned here. They will see that the language does correctly calculate exhaustiveness for this set of cases. It just doesn't use that fact for type promotion.

What I really don't want is users to end up preferring to jam switch expressions into statement contexts just to get tighter exhaustiveness checking like your second example:

void test(A a) {
  int x;
  (switch(a) {
    A(value:true) => x = 0,
    A(value:false) => x = 1
  })
  x.isEven; // Ok, x is definitely assigned.
}

I don't have a good sense of:

1. How often switch statements in existing Dart code are deliberately not exhaustive (i.e. they have no default case and when run, it's expected and desired that often no case matches). Anecdotally, my impression is that a significant fraction are.

2. How often switch statements in future Dart code with pattern matching will be. It may be that idiomatic Dart style leans more heavily towards exhaustiveness once we ship patterns, even in statement-level code where it's not strictly needed.

3. How often users will switch on non-exhaustive types but where all of the fields in object patterns are exhaustive.

@pq, do you think it would be possible to get any data on #1? It requires static analysis to know what static type is being switched on and whether the cases in it are exhaustive or not.

I suspect that we can live with the current proposal but this is definitely worrisome.

[lrhn]

I'd be fine with exhausting lists if we can show that any list of the input type is definitely covered by at least one case.

I don't want list types to require exhaustiveness in a non-expression switch.

It's the same thing as the A(value:...) example. We should detect exhaustiveness even for types that don't require it.
Any type is exhausted by itself. If the input has type A, then a pattern of A x will exhaust it, just as surely as var x.

Such exhaustiveness is not fragile in the same ways as enum-values or sealed-subtypes exhaustiveness, where adding a new value or subtype will change the behavior of switches. It's not based on things external to the type, which can be changed independently, but only on the type itself. If you match the type A directly, there is no non-breaking change which can change that.

Object patterns can exhaust a type by exhausting all the properties being looked at, which is why: case A(value: true): ... case A(value: false): ... should exhaust A. Every value of A must fall into one of these buckets, because the value of A.value is a bool, which his exhausted by true and false.

I'm not worried about giving users the advantage of exhaustiveness if they actually exhaustively match A(value: bool) on an A input. It's not a fragile property subject to accidental or unintended breakage.
(Changing the A.value to bool? would break the switch, but it would break any other use of A.value too, it's not about the switch exhaustiveness, it's just plain breaking.)
My only worry is how to give good error messages for people who expected to get exhaustiveness, but missed a case.

Only enums, bool and Null are exhausted by values, all other types are exhausted by type checks on themselves, or exhaustive type checks of subtypes if sealed.

Back to lists (and with the negative-length loophole considered closed):
We "just" need to show that we cover all lengths of lists of the input type entirely, which requires at least one rest-pattern, and totally covering all indexes that are checked by refutable patterns.
I'm sure there are details to get right. It sounds daunting, but no more than other exhaustiveness things we're planning to do. E.g,:

switch (boolList) {
  [] => 0,   // length 0 totally covered
  [var b] => b ? 1 : 0,  // Length 1 totally covered
  [false, ..., false] => 0,  // Length 2+ covered for [0]==false and [len-1]==false
  [true, ...,] => 1, // Length 2+ covered for [0]==true
  [..., true] => 1 // Length 2+ covered for [len-1]==true
}

is probably exhaustive.

switch (boolList) {
  [] => ...
  [var x] => ...
  [var x, var y] => ...
  [var x, ..., true, var y] => ...
  [var x, false, ... var y] => ...
  [var x, var y, ..., var z, var w] => ...
}

gets trickier, because we need to cover length-3 lists using list[1] and list[len - 2], and recognizing they are the same for len==3.
If we can do it, it'd be good. If we have to restrict exhaustiveness-recognition to simpler patterns (like no trailing patterns after ...), it'll probably still be useful.

Maps are right out. Matching all lengths of maps is pointless because the structure of a map is not defined by its length, but by its keys. We'd have to exhaust the powerset of the key type to know we've exhausted all possible maps. Most maps being matched will be JSON, and the keyset is String, which is an infinite type.
If your switch doesn't contain the map pattern {...}, it won't be exhaustive. If it does, it will be exhaustive, because we should special-case treat {...} to act like the Map() object pattern, which exhausts its own type.

If we are considering exhaustiveness for lists when we match all lengths, then we should consider exhaustiveness for integers when we cover all ranges. Otherwise exhausting the list lengths feel a little under-defined. (How do we know we cover all integer lengths?)

We can (and probably should) special case integer values, so that

int sign(int integer) => switch (integer) {
  case < 0 => -1,
  case 0 => 0,  // or: case == 0 => 0
  case >0 => 1,
};

works.
We have the comparison patterns mainly to support integers, so we should also trust them.
(I think it should still work on the web, as long as we won't recognize >= -9223372036854775808 as trivially true. A NaN is not an integer. And that's also why we cannot do the same for doubles, unless we special case the pattern double.nan to match a nan value, instead of failing any equality check.)

[stereotype441]

What I really don't want is users to end up preferring to jam switch expressions into statement contexts just to get tighter exhaustiveness checking like your second example:

void test(A a) {
  int x;
  (switch(a) {
    A(value:true) => x = 0,
    A(value:false) => x = 1
  })
  x.isEven; // Ok, x is definitely assigned.
}

Ugh, yeah. I don't want to create any incentives to do this either.

It feels to me like the crux of the problem is that since constant evaluation happens after flow analysis, and checking for exhaustiveness errors has to happen after constant evaluation, flow analysis has to make some assumption about switch statement exhaustiveness that might be wrong. If it assumes switches on lists are exhaustive (i.e. we make lists an exhaustive type), then users who don't want an exhaustive switch statement for their list are going to have to add a default clause, and that's going to be frustrating. If it assumes switches on lists aren't exhaustive (i.e. we don't make lists an exhuastive type), then users who do want an exhaustive switch statement, and who want the flow analysis benefits that come with it, are going to be frustrated and might resort to horrible things like rewriting to a switch expression (yuck).

I wonder if we could have it both ways, though. We could:

• Keep the current definition of exhaustive type (lists are not an exhaustive type)
• During flow analysis:
  • For switch expressions, and switch statements with a scrutinee that is an exhaustive type, flow analysis always assumes the switch is exhaustive.
  • For switch statements with a scrutinee that is not an exhaustive type, flow analysis runs the exhaustiveness checking algorithm in a mode where any references to constants are skipped (this may mis-classify some switch statements as non-exhaustive but that's not a soundness violation). (Exception: direct references to enum constants are still taken into account, since we can do that without needing to wait for constant evaluation).
• After constant evaluation:
  • For switch expressions, and switch statements with a scrutinee that is an exhaustive type, the exhaustiveness checking algorithm runs in a mode where it accounts for counstant values, and produces a compile-time error if the switch statement wasn't exhaustive.
  • For switch statements with a scrutinee that is not an exhaustive type, no further exhuastiveness checking is performed.

This would mean that:

• It is a compile-time error if a switch expression is not exhuastive (as currently specified).
• It is a compile-time error if a switch statement has a scrutinee that is an exhaustive type, and it is not exhaustive (as currently specified).
• It is allowed for a switch statement to be non-exhaustive provided that its scrutinee is not an exhaustive type (as currently specified).
  • However, if such a switch statement is exhaustive anyway (and the exhaustiveness checking algorithm can tell that it's exhaustive without having to rely on constant evaluation), flow analysis gets the benefit of knowing that it's exhaustive. This means that the only time the user would have to add unnecessary default clauses to shut up compile errors is if the scrutinee type is a non-exhaustive type and constant evaluation is required to prove that the switch is exhaustive. Which is almost never going to happen in practice.

There is an implementation cost to this strategy, though, which is that the exhaustiveness checking algorithm would have to be written in such a way that it can be invoked either during flow analysis or after constant evaluation depending on the circumstance. My gut feeling is that would not be too much of a problem, but CC @johnniwinther in case he wants to weigh in.

[johnniwinther]

@stereotype441 My work so far indicates that this might be doable.

[pq]

@pq, do you think it would be possible to get any data on #1? It requires static analysis to know what static type is being switched on and whether the cases in it are exhaustive or not.

Sure. One approach would be to take exhaustive_cases which enforces exhaustiveness for "enum-like classes", and look at generalizing it to flag non-exhaustive switches over other types for the purpose of data-gathering.

[munificent]

I would love love love to see data (especially from google3) on this if you have the time to dig it up.

[srawlins]

I think this was completed.

[munificent]

The initial issue is a little vague and the subsequent discussion meanders (in part because of my mis-understanding of Leaf's issue and comments) but I believe the core issue is still open. There are two separate but confusingly similar concepts:

• Which types let us determine whether a set of patterns matching that type are exhaustive and what is the algorithm for that? This is "exhaustiveness".
• Which types, when appearing as the value type in a switch statement for the switch to be exhaustive or report a compile-time error otherwise. This is "always-exhaustive types".

The list Leaf points out in the issue is the list of always-exhaustive types, which is what I think this issue is about.

These are separate concepts because Dart has one foot on the imperative side and one foot on the functional side. That puts switch statements in a weird place. Consider:

respond(String s) {
  switch (s) {
    case 'hi': print('hello');
    case 'bye': print('later');
  }
}

There is nothing unsound about this function. If you call it with one of two expected strings, it prints another string in reply. Otherwise, it prints nothing. Is it correct that this function silently prints nothing on any other string? Is that what the author intended?

If we wanted the language to be maximally paranoid, we would require all switch statements to be exhaustive over all possible incoming values. That would mean that every switch needs to either have a set of cases that exhaustively covers all values (using the exhaustiveness checker) or must have a default case.

But, historically, Dart has never required that. It's happy to have switch statements that don't match any case (unless the type being switched on is an enum). It's a statement after all. You can have if statements with no else clause as well, which is basically the same thing.

When we added exhaustiveness checking and patterns, it felt weird to me to still allow non-exhaustive switch statements for all types. If you go out of your way to define a sealed class hierarchy, you probably do want all code working with values of that type to be exhaustive, even switch statements.

So to split the difference, I specified a list of "always-exhaustive" types. These are types where a switch statement must be exhaustive when matching on that type. (Switch expressions must always be exhaustive for all types.) That list isn't arbitrary but it's... heuristic-based. I chose a set of types where I thought user intuition would be that it should be exhaustive.

This issue is asking the question of whether a List of an always-exhaustive type or a Map of an always-exhaustive type should itself be considered an always-exhaustive type. In Dart 3.0, the answer is "no". But we could conceivably tighten this if we felt it was helpful for users.