Static Exhaustiveness Checks
Pattern Matching is not just convenient syntax sugar. By using a match
statement instead of an if-else chain,
Claro is able to statically validate that every possible case is exhaustively handled by some case
.
For example, the following match
over a value of type oneof<Red, Yellow, Green>
is missing a case
to handle the
Green
atom and Claro rejects the match
at compile-time:
Fig 1:
atom Red
atom Yellow
atom Green
var lightColor: oneof<Red, Yellow, Green> = Green;
var lightColorStr: string;
match (lightColor) {
case _:Red -> lightColorStr = "red";
case _:Yellow -> lightColorStr = "yellow";
}
print(lightColorStr);
Compilation Errors:
exhaustiveness_checks_EX1_example.claro:8: Non-exhaustive Match: The given cases do not match every possible value of the matched type `oneof<Red, Yellow, Green>`.
For example the following case is unhandled:
case _:Green -> ...;
You can also ensure that all possible cases are being handled by adding a final fallback case as below:
case _ -> ...;
match (lightColor) {
^^^^^^^^^^
1 Error
By following the suggestion in the error message above, we can fix the program:
Fig 2:
atom Red
atom Yellow
atom Green
var lightColor: oneof<Red, Yellow, Green> = Green;
var lightColorStr: string;
match (lightColor) {
case _:Red -> lightColorStr = "red";
case _:Yellow -> lightColorStr = "yellow";
case _:Green -> lightColorStr = "green";
}
print(lightColorStr);
Output:
green
Non-Trivial Exhaustiveness Checks Example
The above example is fairly trivial, just validating that all oneof
type variants are handled. However, Claro's
exhaustiveness checks are fairly sophisticated, and should be able to catch mistakes in much more complicated scenarios:
Fig 3:
newtype Foo<T> : T
var myStruct2 = {a = {x = 1, y = "ninety-nine"}, z = Foo(true)};
match (Foo(myStruct2)) {
case Foo({a = {x = 1, y = "two"}, z = Foo(false)}) -> print("Foo(\{a = \{x = 1, y = \"two\"}, z = Foo(false)})");
case Foo({a = {x = 3, y = "zero"}, z = Foo(false)}) -> print("Foo(\{a = \{x = 3, y = \"zero\"}, z = Foo(false)})");
case Foo({a = {x = 1, y = _}, z = Foo(false)}) -> print("Foo(\{a = \{x = 1, y = _}, z = Foo(false)})");
case Foo({a = {x = _, y = "two"}, z = Foo(false)}) -> print("Foo(\{a = \{x = _, y = \"two\"}, z = Foo(false)})");
case Foo({a = A, z = Foo(true)}) -> print("Foo(\{a = A, z = Foo(true)}) where A = {A}");
case Foo({a = {x = 3, y = "six"}, z = Foo(false)}) -> print("Foo(\{a = \{x = 3, y = \"six\"}, z = Foo(false)})");
}
Compilation Errors:
exhaustiveness_checks_EX3_example.claro:4: Non-exhaustive Match: The given cases do not match every possible value of the matched type `Foo<struct{a: struct{x: int, y: string}, z: Foo<boolean>}>`.
For example the following case is unhandled:
case Foo({a = {x = _, y = _}, z = Foo(false)}) -> ...;
You can also ensure that all possible cases are being handled by adding a final fallback case as below:
case _ -> ...;
match (Foo(myStruct2)) {
^^^^^^^^^^^^^^
1 Error
Again, following the suggestion from the error message, we can fix the program:
Fig 4:
newtype Foo<T> : T
var myStruct2 = {a = {x = 1, y = "ninety-nine"}, z = Foo(true)};
match (Foo(myStruct2)) {
case Foo({a = {x = 1, y = "two"}, z = Foo(false)}) -> print("Foo(\{a = \{x = 1, y = \"two\"}, z = Foo(false)})");
case Foo({a = {x = 3, y = "zero"}, z = Foo(false)}) -> print("Foo(\{a = \{x = 3, y = \"zero\"}, z = Foo(false)})");
case Foo({a = {x = 1, y = _}, z = Foo(false)}) -> print("Foo(\{a = \{x = 1, y = _}, z = Foo(false)})");
case Foo({a = {x = _, y = "two"}, z = Foo(false)}) -> print("Foo(\{a = \{x = _, y = \"two\"}, z = Foo(false)})");
case Foo({a = A, z = Foo(true)}) -> print("Foo(\{a = A, z = Foo(true)}) where A = {A}");
case Foo({a = {x = 3, y = "six"}, z = Foo(false)}) -> print("Foo(\{a = \{x = 3, y = \"six\"}, z = Foo(false)})");
# Adding the case suggested by the prior error message.
case Foo({a = {x = _, y = _}, z = Foo(false)}) -> print("Foo(\{a = \{x = _, y = _}, z = Foo(false)})");
}
Output:
Foo({a = A, z = Foo(true)}) where A = {x = 1, y = ninety-nine}
Note: Claro's suggestions for resolving non-exhaustiveness match
statements are intelligent and reliable, but Claro
will only warn about a single missing case example at a time (even if there are multiple unhandled cases). You may have
to apply multiple suggestions in succession, but simply following the suggestions will definitely (eventually) lead to a
fully exhaustive match statement.