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.