Definition of "exhaustive" for switch statements?

The section about control flow of the language guide says:

Every switch statement must be exhaustive. That is, every possible value of the type being considered must be matched by one of the switch cases.

That sounds a bit magical to me, how can the compiler determine if the cases cover the range of any type?

For example, I tested if the compiler complained with

let flag = [true, false].randomElement()!

switch flag {
case true:
    print("pos")
case false:
    print("neg")
}

and it correctly concludes there are no more options and runs.

However, this is also the case here:

let n = [-1, 1].randomElement()!

switch n {
case Int.min..<0:
    print("negative")
case 0...Int.max:
    print("non-negative")
}

but it does not compile.

Is there a precise meaning of "being exhaustive"? Like, you have to enumerate all the values of a type individually explicitly?

The compiler knows that a Bool has only 2 possible values, and that they are true and false. The compiler does not know that the ranges in your second switch cover all the possible values of Int. It has no special knowledge of the semantic meaning of Int.min and Int.max. They are just bit patterns, so far as the compiler is concerned.

Yes, yes, I understand that.

But what about the question I asked?

For any type for which the compiler is aware of every possible value, an exhaustive switch either lists every value in the list of cases, or it contains a default case.

For all other types, a default case must be included.

Is there a list of the types the compiler is aware of?

This is just formal interest, in practice of course I can provide a default if needed. I am studying the language.

1 Like

I believe that only (frozen) enums and Bool fit the criteria.

1 Like

File lib/Sema/TypeCheckSwitchStmt.cpp implements exhaustiveness checking. A comment in the file says

  /// The SpaceEngine encapsulates
  ///
  /// 1. An algorithm for computing the exhaustiveness of a switch statement
  ///    using an algebra of spaces based on Fengyun Liu's
  ///    "A Generic Algorithm for Checking Exhaustivity of Pattern Matching".
  /// 2. An algorithm for computing warnings for pattern matching based on
  ///    Luc Maranget's "Warnings for pattern matching".
  ///
  /// The main algorithm centers around the computation of the difference and
  /// the containment of the "Spaces" given in each case, which reduces the
  /// definition of exhaustiveness to checking if the difference of the space
  /// 'S' of the user's written patterns and the space 'T' of the pattern
  /// condition is empty.
6 Likes

Super interesting! So it seems to be a little more sophisticated.

To play around, I tested this edge-case:

let n = [-1, 1].randomElement()!

switch n {
case is Int:
    print("integer")
}

and it is able to determine that is exhaustive (it warns, but it compiles).

1 Like

Another case that does not need a default:

let yetAnotherPoint = (1, -1)
switch yetAnotherPoint {
case let (x, y) where x == y:
    print("(\(x), \(y)) is on the line x == y")
case let (x, y) where x == -y:
    print("(\(x), \(y)) is on the line x == -y")
case let (x, y):
    print("(\(x), \(y)) is just some arbitrary point")
}

This one appears in the language guide.

The only difference between that last case and default is that the last case provides bindings for the matched pattern. Remember that default is equivalent to case _:. It's rather trivial for the compiler to prove exhaustivity when you give it a case that unconditionally matches all patterns.

2 Likes

That's pretty clever. I wonder if this is smart enough to lazy evaluate those where predicates, or if it behaves more like a static rewrite into matching over multiple bools, like:

let yetAnotherPoint = (1, -1)

let (x, y) = yetAnotherPoint
switch (yetAnotherPoint, x == y, x == -y) {
case let ((x, y), true, _):
	print("(\(x), \(y)) is on the line x == y")
case let ((x, y), _, true):
	print("(\(x), \(y)) is on the line x == -y")
case let ((x, y), _, _):
	print("(\(x), \(y)) is just some arbitrary point")
}

But that is an observation a posteriori. I do not know if the compiler is smart enough or not to understand that my partition of Int above covers all the domain. In that case, it does not. The only way for me to check if an arbitrary total coverage is understood or not is to try if the program compiles.

The point of the thread is to define what does exhaustive mean. I am providing counterexamples to some early replies in which you do not need default, but there are no frozen enums or booleans. Also playing with examples to see what works and what not.

In the end, the answer is in the implementation linked by @mayoff, but I would need to translate that code into Swift as used by a programmer.

It's required to be lazy by the language: if the where conditions have side effects, they must not be evaluated if the pattern doesn't match. It's also relevant if the condition depends on variables being matched, which wouldn't make sense for, say, an enum that isn't in the particular case right now.

1 Like

(sorry for the self-servable questions, but I really don't understand enough about the compiler to be able to understand this in the source myself, yet)

Oh yeah, I've noticed the top-to-bottom ordering of calls in where clauses before, I was just curious of the language has special behaviour around side effect free predicates like ==, and if it can get smart about assembling together the checks to get away with only doing a single jump.

Idk if this would be worthwhile or not, but I imagined that the machine code for this could calculate the equality in each of those cases, represent those results as bits fields in a single value, multiply that value field by some constant factor, and jump that far ahead (to where the cases would be implemented). Basically, a fancy jump table that works over multiple values being matched in a tuple

1 Like

I have opened an issue, let's see what they think.

Ah, yeah, if there are no side effects the compiler is certainly allowed to do so if it thinks that'll be more efficient!

Isn't it similar to this post (below), that the actual evaluation order is undefined? Or are they different things?

Yeah, pretty much. I didn't get that @AlexanderM was talking about optimization at first, rather than what the programmer should expect.

One thing that I learnt in a youtube video that in case of Enums you don't need the default case.

Terms of Service

Privacy Policy

Cookie Policy