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.
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.
/// 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.
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")
}
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.
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.
(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