[patterns] Exhaustiveness as a boolean simplification issue

[eernstg]

I think it could be useful to handle exhaustiveness using a different perspective than that of the current feature specification. Of course, any perspective will have a lot in common with any other perspective, so there will be many recognizable elements, but the approach that I'm proposing here remains more tightly connected to the language (and its implementation), because it relies on compile-time analysis of the value of boolean expressions. The main advantages of doing this are the following:

• I believe that it is easier to understand the semantics of matching, and to understand why we can conclude that certain switch expressions/statements have exhaustive cases, respectively that a given case is unreachable.
• With the reliance on the value of boolean expressions we can use pre-existing knowledge to handle the processing of a given expression (and we may be able to use existing code in the analyzer/linter) to perform this analysis. In particular, it is well-known that any boolean expression using && and || and ! can be rewritten to an equivalent boolean expression in conjunctive normal form, which is particularly convenient to check.

I'll use the same example as in the exhaustiveness feature specification:

enum Suit { club, diamond, heart, spade }

switch class Card {
  final Suit suit;
  Card(this.suit);
}

class Pip extends Card {
  final int pips;
  Pip(super.suit, this.pips);
}

switch class Face extends Card {
  Face(super.suit);
}

class Jack extends Face {
  final bool oneEyed;
  Jack(super.suit, this.oneEyed);
}

class Queen extends Face {
  Queen(super.suit);
}

class King extends Face {
  King(super.suit);
}

I'm using switch rather than sealed as the class modifier that enforces that the class is abstract and the set of immediate subtypes is locally known, because sealed means several different things

Pattern predicates rather than spaces

This issue exists in order to propose that we focus on pattern predicates rather than pattern spaces, and the motivation for doing this is that we avoid explicitly reasoning about sets of objects and instead work with predicates, that is, boolean expressions.

In general, for any given pattern P that we're matching a scrutinee s of static type S against, we have a predicate P(s), which is true if and only if s matches P. Here are the cases listed in the feature spec. We elide certain elements which are repeated in every item in that "P: e" means "The predicate of the pattern P is ((S s) => e)":

• A type T: s is T.
• A record pattern (n1: P1, .. nk: Pk): P1(s.n1) && .. Pk(s.nk), where Pj is the predicate for the pattern Pj, where the argument type is the static type of the nj in the given record type.
• A list pattern <T>[P0, .. Pk]: s.length == k && P0(s[0]) && .. Pk(s[k]), where Pj is the predicate for the pattern Pj, where the argument type is T (of course, I'd prefer s.length >= k, but that's a separate discussion).
• A map pattern <K, V>{v1: P1, .. vk: Pk}: P1(s[v1]) && .. Pk(s[vk]), where Pj is the predicate for the pattern Pj, where the argument type is V.
• A wildcard pattern _: true.
• A pattern for a variable v with type T: s is T.
• A literal matcher like 5: identical(s, 5).
• A pattern for a constant expression c: identical(s, c).
• A literal matcher for true or false: s respectively !s.
• A literal matcher for an enum value like Suit.heart: identical(s, Suit.heart).
• A nullable pattern P?: s is Null || P(s).
• A non-null assertion pattern P!: P(s!). The evaluation of this predicate may throw, but when it does not throw it is known that the scrutinee isn't null.
• A cast pattern P as T: P(s as T), which may also throw.

For example: The pattern Card(suit: Suit.heart) in a context where the scrutinee has type Object has the predicate ((Object o) => o is Card && identical(o.suit, Suit.heart)).

Exhaustiveness and reachability

In order to determine whether a given set of cases with patterns P1 .. Pk with a scrutinee s is exhaustive, we need to show that P1(s) || .. || Pk(s) is true (that is, always true).

The intuition is that if P1(s) || .. || Pk(s) is true (for any given s that we might encounter) then there is always at least one case that matches, because Pj(s) is true for some j. So P1 .. Pk is exhaustive.

In order to detect that a given case Pj is unreachable, we need to show that P1(s) || .. Pj-1(s) || !Pj(s) is true (again: always true).

The intuition is that, for any given s, if Pj(s) is true then !Pj(s) is false, and if the entire expression is true (for any s, including this one) then there must be an i with 1 <= i < j, such that Pi(s) is true. This means that whenever we could have used case j, we can also use some earlier case. So we'll never choose case j, and hence it is unreachable.

How do we prove that a predicate is always true?

First, for a given sequence of cases P1 .. Pk with a scrutinee s with static type S, each case Pj has a predicate of the form (S s) => Pj(s). So for exhaustiveness we must show that the predicate (S s) => P1(s) || .. Pk(s) is always true.

Next, rewrite the expression P1(s) || .. Pk(s) to conjunctive normal form, that is, a sequence of expressions of the form (e11 || .. || e1n1) && (e21 || .. || e2n2) .. && (em1 || .. || emnm) (this is always possible).

Now we need to show for each disjunction e1 || .. || en that it is always true. It is enough if we can find just one of the operands which is always true.

In particular, the type test s is S is always true, because the scrutinee s has the static type S.

If this expression does not occur then we can gather expressions of the form s is T1 .. s is Tk, such that T1 .. Tk is the exhaustive set of immediate subtypes of a given switch type T0, and replace those expressions by s is T0. This step may be taken repeatedly, in which case we may obtain s is S and conclude that the expression is always true.

Otherwise we may have expressions of the form identical(s, true) as well as identical(s, false), which yields true in the case where S is bool (because they are connected by ||), or the same plus identical(s, null) with bool?. Or we may have identical(s, E.vj) for all values v1 .. vm of a given enum type E, which is also always true, and similarly with null when S is E?.

Otherwise we may have identical(c1, c2) where c1 and c2 are constant expressions and identical(c1, c2) is a constant expression that evaluates to true.

Otherwise we may have e and !e for any expression e, which is also always true.

We may have e is T1 and e is! T2 where T2 <: T1. This is also always true (and does not require the types to be switch classes). Conversely, assume that it is false for some object o, that is, o is! T1 and o is T2: that cannot happen because o is T1 must be true when o is T2 is true and T2 <: T1.

Recursively, for each field fj of S with type Sj, the same reasoning can be used on s.fj with respect to the type Sj. This case includes all "navigation" expressions of the form s.m1.m2. ... mk, where mj is a getter name or an index, [12], or a map lookup [someConstant].

For a predicate of the form !P we need to show that P is always false.

With s is! T, we have a couple of special cases: Whenever the type of the scrutinee is not a supertype of num, int, double, or String, it is known that s is num, s is int etc. are always false. In general, s is! T is known to be true whenever the standard lower bound of S and T is Never (fx. when S is MyClass and T is a function type). We cannot conclude the same for any other pair of class types, because it is always possible to declare a class that implements both (there is an exception in the case where the two classes have incompatible member signatures, e.g., one has a getter m and the other has a method m, but we may or may not use that).

For example, consider the following switch statement:

// Suit, Card, etc. declared as before.

void f(Card c) {
  switch (c) {
    case Face(suit: Suit.heart): return;
    case Jack(oneEyed: bool, suit: Suit.heart): return;
    default: return;
  }
}

In order to show that the second case is unreachable we need to consider the following expression, shown at first and then rewritten one step for each ==:

(c is Face && identical(c.suit, Suit.heart)) || 
!(c is Jack && identical(c.suit, Suit.heart) && c.oneEyed is bool) == // Use conjunctive normal form.

(c is Face && identical(c.suit, Suit.heart)) ||
c is! Jack || !identical(c.suit, Suit.heart) || c.oneEyed is! bool == // .. and eliminate always-false term.

(c is Face || c is! Jack || !identical(c.suit, Suit.heart)) &&
(identical(c.suit, Suit.heart)) || c is! Jack || !identical(c.suit, Suit.heart)) == // We have `e` and `!e`.

(c is Face || c is! Jack || !identical(c.suit, Suit.heart)) == // We have `Jack <: Face`.

true

Semantics and side effects

Many of these expressions depend on having a particular ordering, because they use names with a promoted type, and the promotion is justified by some earlier operand (of || or &&, typically). They also invoke getters repeatedly.

The semantics of the predicate evaluation which is used to determine whether there is a match at run time will be such that no getter is invoked multiple times for the same switch statement/expression matching process. This can be achieved by declaring local variables (such that we'd read the value of late final var c_suit = c.suit; each time we need the value of c.suit rather than invoking c.suit twice). Some of these variables will be the ones that are introduced by the patterns.

This means that there is no ambiguity in the semantics of evaluation of expressions involving getter invocations, non-null assertions, etc., because they will all be executed at most once, on demand, when the corresponding expression occurs in the patterns in the source code, and the translated code actually reads a local variable.

Discussion

The main reason why I'm interested in this approach rather than an approach that is based on spaces is that this approach deals with the language semantics directly (without involving sets of objects that don't actually get computed at run time), and we already need to reason about the value of boolean expressions in the language (e.g., in order to promote based on the values of boolean variables and in order to have lints like invariant_booleans).

It should also be obvious that there is a very tight connection between the actual matching process and the compile-time reasoning about exhaustiveness and reachability, and this makes it easier to see that the conclusions are correct, and possibly easier to report error messages.

[munificent]

Ow, wow. This is fantastic.

It looks correct to me, at least as far as I can tell from an initial reading. It might be that this produces the right answer, but doesn't have the performance bounds we want.

In particular:

• Converting to CNF could potentially cause large expression blow-up.
• Searching the disjunctive operands for is expressions of all of the subtypes of a sealed type could be slow. I think I can imagine a data structure to represent the disjunction that helps here.

I really want to try a prototype implementation of this and see how it works in practice.

[lrhn]

I think it looks interesting, but can we be sure the problem is not equivalent to satisfiability and therefore NP-complete.

Asking whether a CNF predicate is always true (ᴛᴀᴜᴛᴏʟᴏɢʏ) is co-NP complete. Are there special features of this problem which allows us to be more efficient?

[eernstg]

@lrhn wrote:

I think it looks interesting, but can we be sure the problem is not equivalent to satisfiability and therefore NP-complete.

Surely it is equivalent, and that wouldn't be news. The paper A generic algorithm for checking exhaustivity of pattern matching has the following:

The general problem of pattern matching is NP-Complete [10]. Thus we expect the worst-case performance of the generic algorithm to be exponential. This is caused by the subtraction of two constructor spaces which could result in a proliferation of spaces. However, in practice the algorithm performs well without performance issues.

See the comments below about emulating 3-SAT (which is known to be NP-hard).

@munificent wrote:

Converting to CNF could potentially cause large expression blow-up.

That is definitely true. However, we do have some special properties in this case:

I mentioned that we could eliminate subterms that are known to be false (like s is! T where T is the static type of s), but it may be much more important that we can eliminate subpatterns that are irrefutable (before we even generate the predicates).

In particular, any pattern which is just exploring the structure using extractor patterns and binding new variables to objects from there can be reduced to a type pattern. For example, C(a:, b: D(e:, f:)?) is treated as the type pattern C. This means that a full extraction of the state of the scrutinee like the following would be checked for completeness by checking the disjunction c is Pip || c is Jack || c is Queen || c is King (which is already in conjunctive normal form) which is reduced to c is Pip || c is Face and then c is Card, which is true. Of course, the steps taken are the same from that point if we start off with c is Pip || c is Face, or any other intermediate form.

void f(Card c) {
  switch (c) {
    case Pip(suit:, pips:): ...
    case Jack(oneEyed:, suit:): ...
    case Queen(suit:): ...
    case King(suit:): ...
  }
}

Next, we would sort the cases before checking exhaustiveness. A type test goes first. So if we have a catch-all case then we would immediately note that it is true:

void f(Card c) {
  switch (c) {
    case ... // Anything.
    case Card(suit:): ...
  }
}

Having sorted the cases, we would work on c is Card || ... /*some other cases*/, and since c is Card is true, the disjunction is true.

Similarly for catch-all cases in known-exhaustive subtypes

void f(Card c) {
  switch (c) {
    case ... // Anything.
    case Pip(suit:, pips:): ...
    case ... // Anything.
    case Face(suit:): ...
  }
}

Here we would check c is Face || c is Pip || ... /*more stuff*/, reduce it to c is Card || ... /*more stuff*/, and conclude that it is true (without processing the 'stuff' at all).

If we're switching on the values of an enum (or any other finite set that we may specify) we will have a predicate like identical(s, v1) || identical(s, v2) || ... || identical(s, vk) which is again already in conjunctive normal form. We would need to detect that the listed values cover the entire set of values, and this would again be just as fast as any other algorithm which ends up testing the same "all values included" criterion.

The first hard case that we'd need to consider is the case where we have a conjunction in some or all cases. In particular, we could iterate over all combinations of a couple of boolean instance variables, which would involve an extractor pattern and some constant values to match against in each subpattern:

class BoolPair {
  final bool left, right;
  const BoolPair(this.left, this.right);
}

void f(BoolPair s) {
  switch (s) {
    case BoolPair(left: false, right: false): ...
    case BoolPair(left: false, right: true): ...
    case BoolPair(left: true, right: false): ...
    case BoolPair(left: true, right: true): ...
  }
}

Of course, we could declare a class with k boolean instance variables v1 .. vk for any given k, and we could then have cases corresponding to any conjunction of those variables (like Bool93Tuple(v3: true, v71: false, v72: true), modelling v3 && !v71 && v72, along with a bunch of other patterns modeling terms of the form u && v && w). Checking exhaustiveness for that switch would then be exactly equivalent to checking satisfiability of a 3-SAT problem: If the switch is exhaustive then the corresponding expression ((v3 && !v71 && v72) || ...) is true for every possible binding of the variables v1 .. vk to boolean values; this means that the negation ((!v3 || v71 || !v72) && ...) is false for every possible binding of the variables, that is, it is not satisfiable. If it is not exhaustive then there is a binding which makes the 3-SAT term true, i.e., the 3-SAT is satisfiable.

This means that if we can do this in less than exponential time worst case then we've given a counter-example to the exponential time hypothesis, which would be cool. ;-)

[munificent]

I spent a little time hacking on a prototype today. We'll definitely need to do something significantly smarter than a naïve conversion to CNF using the distributive law. Say you have this class hierarchy:

sealed class A {}
class B extends A {}
class C extends A {}
class D extends A {}

And this switch:

test({A y, A z} record) {
switch (
  case (y: B _, z: B _): ...
  case (y: B _, z: C _): ...
  case (y: B _, z: D _): ...
  case (y: C _, z: B _): ...
  case (y: C _, z: C _): ...
  case (y: C _, z: D _): ...
  case (y: D _, z: B _): ...
  case (y: D _, z: C _): ...
  case (y: D _, z: D _): ...
}

The nine cases here cover all combinations of subtypes, so this is exhaustive. A predicate that captures those cases is:

(o.y is B & o.z is B) | 
(o.y is B & o.z is C) | 
(o.y is B & o.z is D) | 
(o.y is C & o.z is B) | 
(o.y is C & o.z is C) | 
(o.y is C & o.z is D) | 
(o.y is D & o.z is B) | 
(o.y is D & o.z is C) | 
(o.y is D & o.z is D)

If we convert it to CNF form by distributing all those |, we get:

(o.y is B | o.y is B | o.y is B | o.y is C | o.y is C | o.y is C | o.y is D | o.y is D | o.y is D) & 
(o.y is B | o.y is B | o.y is B | o.y is C | o.y is C | o.y is C | o.y is D | o.y is D | o.z is D) & 
(o.y is B | o.y is B | o.y is B | o.y is C | o.y is C | o.y is C | o.y is D | o.z is C | o.y is D) & 
(o.y is B | o.y is B | o.y is B | o.y is C | o.y is C | o.y is C | o.y is D | o.z is C | o.z is D) & 
(o.y is B | o.y is B | o.y is B | o.y is C | o.y is C | o.y is C | o.z is B | o.y is D | o.y is D) & 
... 552 lines skipped ...
(o.z is B | o.z is C | o.z is D | o.z is B | o.z is C | o.z is D | o.y is D | o.z is C | o.z is D) & 
(o.z is B | o.z is C | o.z is D | o.z is B | o.z is C | o.z is D | o.z is B | o.y is D | o.y is D) & 
(o.z is B | o.z is C | o.z is D | o.z is B | o.z is C | o.z is D | o.z is B | o.y is D | o.z is D) & 
(o.z is B | o.z is C | o.z is D | o.z is B | o.z is C | o.z is D | o.z is B | o.z is C | o.y is D) & 
(o.z is B | o.z is C | o.z is D | o.z is B | o.z is C | o.z is D | o.z is B | o.z is C | o.z is D)

It's better if we prune duplicates:

(o.y is B | o.y is C | o.y is D) & 
(o.y is B | o.y is C | o.y is D | o.z is B) & 
(o.y is B | o.y is C | o.y is D | o.z is B | o.z is C) & 
(o.y is B | o.y is C | o.y is D | o.z is B | o.z is C | o.z is D) & 
(o.y is B | o.y is C | o.y is D | o.z is B | o.z is D) & 
(o.y is B | o.y is C | o.y is D | o.z is B | o.z is D | o.z is C) & 
(o.y is B | o.y is C | o.y is D | o.z is C) & 
(o.y is B | o.y is C | o.y is D | o.z is C | o.z is B) & 
(o.y is B | o.y is C | o.y is D | o.z is C | o.z is B | o.z is D) & 
(o.y is B | o.y is C | o.y is D | o.z is C | o.z is D) & 
(o.y is B | o.y is C | o.y is D | o.z is C | o.z is D | o.z is B) & 
(o.y is B | o.y is C | o.y is D | o.z is D) & 
(o.y is B | o.y is C | o.y is D | o.z is D | o.z is B) & 
(o.y is B | o.y is C | o.y is D | o.z is D | o.z is B | o.z is C) & 
(o.y is B | o.y is C | o.y is D | o.z is D | o.z is C) & 
(o.y is B | o.y is C | o.y is D | o.z is D | o.z is C | o.z is B) & 
(o.y is B | o.y is C | o.z is B | o.z is C | o.z is D) & 
(o.y is B | o.y is C | o.z is B | o.z is D | o.z is C) & 
(o.y is B | o.y is C | o.z is C | o.z is B | o.z is D) & 
(o.y is B | o.y is C | o.z is C | o.z is D | o.z is B) & 
(o.y is B | o.y is C | o.z is D | o.z is B | o.z is C) & 
(o.y is B | o.y is C | o.z is D | o.z is C | o.z is B) & 
(o.y is B | o.y is D | o.z is B | o.z is C | o.z is D) & 
(o.y is B | o.y is D | o.z is C | o.z is B | o.z is D) & 
(o.y is B | o.y is D | o.z is C | o.z is D | o.z is B) & 
(o.y is B | o.y is D | o.z is D | o.z is B | o.z is C) & 
(o.y is B | o.z is B | o.z is C | o.z is D) & 
(o.y is B | o.z is C | o.z is B | o.z is D) & 
(o.y is B | o.z is C | o.z is D | o.z is B) & 
(o.y is B | o.z is D | o.z is B | o.z is C) & 
(o.z is B | o.y is B | o.y is C | o.y is D) & 
(o.z is B | o.z is C | o.y is B | o.y is C | o.y is D) & 
(o.z is B | o.z is C | o.z is D) & 
(o.z is B | o.z is C | o.z is D | o.y is B) & 
(o.z is B | o.z is C | o.z is D | o.y is B | o.y is C) & 
(o.z is B | o.z is C | o.z is D | o.y is B | o.y is C | o.y is D) & 
(o.z is B | o.z is C | o.z is D | o.y is B | o.y is D) & 
(o.z is B | o.z is C | o.z is D | o.y is C) & 
(o.z is B | o.z is C | o.z is D | o.y is C | o.y is D) & 
(o.z is B | o.z is C | o.z is D | o.y is D) & 
(o.z is B | o.z is D | o.y is B | o.y is C | o.y is D) & 
(o.z is B | o.z is D | o.z is C | o.y is B) & 
(o.z is B | o.z is D | o.z is C | o.y is B | o.y is C) & 
(o.z is B | o.z is D | o.z is C | o.y is B | o.y is C | o.y is D) & 
(o.z is B | o.z is D | o.z is C | o.y is B | o.y is D)

But obviously we can't just prune the duplicates after the fact because generating the enormous expression is too slow in the first place. We'll need some way to convert a predicate in CNF that collapses duplicates as it goes.

[eernstg]

I spent a little time hacking on a prototype today

Great!

We'll definitely need to do something significantly smarter than a naïve conversion to CNF using the distributive law

Yes. There is a whole subcommunity of computer science where they are working on SAT solvers, so we should be able to learn all the tricks anyone can possibly come up with from existing work in that community.

For exhaustiveness, I think we will very often have an expression which is in disjunctive normal form, like (e11 && e12) || e21 || (e31 && e32 && e33) || .... In this case we have just that, with exactly two operands in each conjunction.

We can work on the disjunctive normal form without computing the conjunctive normal form, because that amounts to considering elements of the form e1_ || e2_ || e3_ || ... where the _ runs over the given elements in each conjunction. So with the example we'd have

(e11 || e21 || e31 || ...) &&
(e12 || e21 || e31 || ...) && 
(e11 || e21 || e32 || ...) &&
(e12 || e21 || e32 || ...) &&
(e11 || e21 || e33 || ...) &&
...

We would deal with each of these by having a reference into the first conjunction e11 && e12 (pointing to either e11 or e12) and a reference into the second conjunction, and so on, and then we'd obtain the next disjunction as the current element from each of the conjunctions.

The code would need to be more general, of course, but the core idea would be to handle each case by iterating over every combination, and escaping as soon as possible:

class TypeTest {
  final String path;
  final String type;
  TypeTest(this.path, this.type);

  @override
  String toString() => '($path, $type)';
}

var isTrueCount = 0;

bool isTrue(List<TypeTest> typeTests) {
  var oyTests = <String>{};
  var ozTests = <String>{};
  ++isTrueCount;
  for (var typeTest in typeTests) {
    if (typeTest.path == 'o.y') {
      oyTests.add(typeTest.type);
      if (oyTests.length == 3) return true;
    }
    if (typeTest.path == 'o.z') {
      ozTests.add(typeTest.type);
      if (ozTests.length == 3) return true;
    }
  }
  return false;
}

void main() {
  var oyB = TypeTest('o.y', 'B');
  var oyC = TypeTest('o.y', 'C');
  var oyD = TypeTest('o.y', 'D');
  var ozB = TypeTest('o.z', 'B');
  var ozC = TypeTest('o.z', 'C');
  var ozD = TypeTest('o.z', 'D');

  for (var p1 in [oyB, ozB]) {
    if (isTrue([p1])) continue;
    for (var p2 in [oyB, ozC]) {
      if (isTrue([p1, p2])) continue;
      for (var p3 in [oyB, ozD]) {
        if (isTrue([p1, p2, p3])) continue;
        for (var p4 in [oyC, ozB]) {
          if (isTrue([p1, p2, p3, p4])) continue;
          for (var p5 in [oyC, ozC]) {
            if (isTrue([p1, p2, p3, p4, p5])) continue;
            for (var p6 in [oyC, ozD]) {
              if (isTrue([p1, p2, p3, p4, p5, p6])) continue;
              for (var p7 in [oyD, ozB]) {
                if (isTrue([p1, p2, p3, p4, p5, p6, p7])) continue;
                for (var p8 in [oyD, ozC]) {
                  if (isTrue([p1, p2, p3, p4, p5, p6, p7, p8])) continue;
                  for (var p9 in [oyD, ozD]) {
                    if (isTrue([p1, p2, p3, p4, p5, p6, p7, p8, p9])) {
                      continue;
                    }
                    print('Not exhaustive!');
                    return;
                  }
                }
              }
            }
          }
        }
      }
    }
  }
  print('Exhaustive! (running isTrue $isTrueCount times)');
}

The predicate isTrue would check out the given predicates, organize them according to the given path (like o.y or o.z in the example), and return true if those tests are sufficient to conclude that the whole disjunction is true. In the code above I've done just enough to handle type tests for B, C, and D, on two paths (o.y and o.z).

The resulting code runs isTrue 262 times (worst case is 512+256+128+64+32+16+8+4+2 == 1022 times).

I think the SAT solver community has done a lot of work about the usefulness of reordering the expressions (it may be a kind of worst case that we have B, B, B, C, C, C, D, D, D on o.y, so we have to go to level 7 in order to ever get true from o.y), but it's at least less than the maximum number of invocations of isTrue.

[munificent]

Closing this. I think we have an approach for exhaustiveness now that's much better than the initial proposal and seems to be working out.