[Exhaustiveness Checking] Different behavior between statements and expressions about sdk

[lrhn]

I can explain that. The type num is a sealed class, which the switch statement takes as a hint that the switch must be exhaustive.
That's based on the static type of the switch value expression.

When you cast the num to Object, and switch on that, that switch does not have to be exhaustive.

Neither switch is exhaustive, cases with a when clause never exhaust anything.

A switch on num, or another sealed type, must be exhaustive.

[lrhn]

That's expected behavior.

Switch statements are not assumed to be exhaustive unless they are on a sealed type or enum. Type inference proceeds under the assumption that it's not exhaustive (possibly except for some very trivial cases that the type inference can see, like having a default case, or another match-all case).

Then, if the switch wasn't assumed to be exhaustive, it's not checked whether it is actually exhaustive using the algorithm which can decide that, but which needs to run after type inference is done.

Switch expressions, on the other hand, must be exhaustive, so they're assumed to be so, and then it's always checked afterwards to be sure.

[mattrberry]

Thanks for the quick response!

Why is this the case? Why not run the exhaustiveness algorithm on switch statements as well?

I'd argue this is not the expected behavior for the end user, even if it matches the spec. The docs don't seem to indicate a difference in exhaustiveness checking between expressions and statements https://dart.dev/language/branches#exhaustiveness-checking. In fact, the docs demonstrate an exhaustiveness check performed over bool? in a switch statement, which seems to blur the lines for when exhaustiveness checking is performed

[lrhn]

The issue is that type inference is affected by exhaustiveness, but exhaustiveness computation depends on the result of type inference.

If we could somehow integrate exhaustiveness computation into the type inference phase, it might be possible to know precisely whether a switch is exhaustive or not right when type inference needs that information, but so far that has not been done.
(I personally don't know why, I haven't written either algorithm, I'll just take the words of those who have that it's not trivial, and not even obviously possible.)

[skylon07]

My two cents: I'd argue switch statements not being exhaustive is what the user should expect. In my mind, they are logically similar to chaining if-else blocks, so suggesting switch statements should be exhaustive is like suggesting those if { ... }s should always be followed by else { ... }s... which seems weird to me.

The question is if something like this is something we want:

var myList = [1, "2", 3, 4, "five"];
for (var item in myList) {
  switch (item) {
    case int(): {
      // do something special to numbers only
    }
    // should I *have* to add `case: String` or `default` here?
  }
}

I'd argue it is since otherwise it would become very burdensome to write "exhaustive but most cases ignored" switch statements.

I'd imagine in most cases where you would want/need the guarantee of an exhaustive switch statement, you could just use a switch expression instead. In those cases I usually just find myself assigning the switch to a variable then using that as a bundled polymorphic thing. It helps prevent code duplication and separates the logic for me.

Curious what your thoughts are on this @mattrberry. All of this is really just a blurb on how I program in my own opinionated way.

[mattrberry]

@skylon07 I'm not suggesting that switch statements must be exhaustive; I don't think you should always need a default case. Rather, I'm suggesting that when they are exhaustive, it'd be nice for the compiler to recognize it.

In my example above, both the statement and the expression exhaustively cover all possible cases, yet the compiler doesn't see that for the statement. What's particularly weird is when the compiler does recognize exhaustiveness in statements. For example, it can determine that switch ([]) { case [...]: return; } is exhaustive.

I'd imagine in most cases where you would want/need the guarantee of an exhaustive switch statement, you could just use a switch expression instead.

There are cases in which I think a statement results in clearer code, since the cases can't be expressed as blocks. There are workarounds, but IMO they're suboptimal

[lrhn]

The inference phase recognizes that [....] is a single pattern which covers the entire type of the switch value, equivalent to a pattern like List _.

That's the kind of "catch-all" patterns that the inference algorithm is capable of recognizing, but it's harder for it to recognize that more than one pattern together exhaust the input, even if neither does by itself.

That's what requires the more complicated algorithm, which also requires type inference to have run first.

[skylon07]

@mattrberry Ah, I see what you're saying -- I misunderstood your original point.

Also, messing around with this more, I actually came up with an example that was confusing to me...

void main() {
  num myNum = 5.5;
  // this switch errors
  switch (myNum) {
    case _ when myNum is int: // case int() but more complicated
      print("is int");
    case _ when myNum is double: // case double() but more complicated
      print("is double");
  }
  
  Object myObject = 5.5;
  // this switch does not error
  switch (myObject) {
    case _ when myObject is int: // case int() but more complicated
      print("is int");
    case _ when myObject is double: // case double() but more complicated
      print("is double");
  }
}

The top switch throws compiler errors, but the bottom one does not. It seems switch (myNum) is required to be exhaustive, but switch (myObject) is not. I would have thought both of them wouldn't need to be exhaustive, since they're both switch statements. Do either of you have an explanation for this?

[skylon07]

Weird... I guess I just haven't used switch statements enough, but that totally makes sense. Didn't realize num was actually defined as a sealed class either, which also makes sense.

Thanks @lrhn for explaining that!

[mattrberry]

I personally don't know why, I haven't written either algorithm, I'll just take the words of those who have that it's not trivial, and not even obviously possible.

@lrhn Possible to check with those who implemented it or get some comment here before closing? I feel like my question was not actually answered here.

[lrhn]

That would be a language question then, because the current behavior is matching the specification.
If we dare change the specification, that's a language change.
(Maybe we have an open issue for it already in the language tracker, but searching GitHub isn't awesome, and even less so on mobile.)

[mattrberry]

I'll open this in the language repo then, thanks