Speed up exhaustiveness checker

[brianhempel]

Results in 5x faster builds on our app.

Successive patterns on data constructors like tuples can cause the list
of unhandled patterns to grow exponentially.

This commit de-duplicates entries in the unhandled patterns list. This
tames the exponential growth considerably.

The proper solution is to create a real union type for nitpicking
patterns. There’s still quite a bit of speed improvement available.

Build times (app: Sketch-n-Sketch):

Elm 0.16:                                  2:32.4
Elm 0.16 with this commit:                 0:27.8
Elm 0.16 with no exhaustiveness checking:  0:11.3

This PR should solve #1267, but closer to the source.
This may or may not affect #1362.

cc @ravichugh

[process-bot]

Thanks for the pull request! Make sure it satisfies this checklist. My human colleagues will appreciate it!

Here is what to expect next, and if anyone wants to comment, keep these things in mind.

[evancz]

Awesome, love this approach! Thanks for the PR!

[evancz]

Alright, I was overeager on this. This seems to take about twice as long for a "typical" build of an Elm project as I am measuring it over here. In other words, it seems like this optimizes the corner case at the expense of 95% of users.

@justinmanley has done some cool work with benchmarking that'd let us assess this more accurately. It seems like you have some very particular pattern matches that are problem cases. I think it'd be good to get those into http://sscce.org so we can speed them up in the context of everything else.

[brianhempel]

Pattern matches on tuples of strings are an easy worst case. The following takes 25 seconds to compile:

module Scratch where

slowExhaustivenessCheck string1 string2 =
  case (string1, string2) of
    ("a", "b")   -> True
    ("c", "d")   -> True
    ("e", "f")   -> True
    ("g", "h")   -> True
    ("i", "j")   -> True
    ("k", "l")   -> True
    ("m", "n")   -> True
    ("o", "p")   -> True
    ("q", "r")   -> True
    ("s", "t")   -> True
    ("u", "v")   -> True
    ("w", "x")   -> True
    ("y", "z")   -> True
    ("aa", "ab") -> True
    ("ac", "ad") -> True
    ("ae", "af") -> True
    ("ag", "ah") -> True
    ("ai", "aj") -> True
    ("ak", "al") -> True
    ("am", "an") -> True
    ("ao", "ap") -> True
    ("aq", "ar") -> True
    ("as", "at") -> True
    ("au", "av") -> True
    ("aw", "ax") -> True
    ("ay", "az") -> True
    _            -> False

As noted, the correct solution is a proper union representation for nitpick patterns. I began some work on it and may revisit it at some point.

[evancz]

I wonder if converting to Text has any benefit for that case. Maybe it'd be quick to look into a fix like that?

[brianhempel]

Nothing to do with string representation. This example takes 23 seconds to fail the exhaustiveness check. (If you make the cases exhaustive by adding a catchall as the last pattern then the successful build takes a full 2.5mins, presumably because of #1362):

module Scratch where

type Letters = A | B | C | D | E | F

slowExhaustivenessCheck letter1 letter2 =
  case (letter1, letter2) of
    (A, B) -> True
    (A, C) -> True
    (A, D) -> True
    (A, E) -> True
    (A, F) -> True
    (B, A) -> True
    (B, C) -> True
    (B, D) -> True
    (B, E) -> True
    (B, F) -> True
    (C, A) -> True
    (C, B) -> True
    (C, D) -> True
    (C, E) -> True
    (C, F) -> True
    (D, A) -> True
    (D, B) -> True
    (D, C) -> True
    (D, E) -> True
    (D, F) -> True
    (E, A) -> True
    (E, B) -> True
    (E, C) -> True
    (E, D) -> True
    (E, F) -> True
    (F, A) -> True
    (F, B) -> True
    (F, C) -> True
    (F, D) -> True
    (F, E) -> True

The key problem is the code here. The code is logically correct. But, if a pattern's complement is represented as a list of more than one pattern then you have the possibility for exponential growth.

-- First iteration

           unhandled: _

complement of (A, B): (B, _), (C, _), (D, _), (E, _), (F, _), (_, A), (_, C), (_, D), (_, E), (_, F)

-- Second iteration

           unhandled: (B, _), (C, _), (D, _), (E, _), (F, _), (_, A), (_, C), (_, D), (_, E), (_, F)

complement of (A, C): (B, _), (C, _), (D, _), (E, _), (F, _), (_, A), (_, B), (_, D), (_, E), (_, F)

-- Third iteration

           unhandled: (B, _), (B, A), (B, B), (B, D), (B, E), (B, F), (C, _), (C, A), (C, B), (C, D), (C, E), (C, F), (D, _), (D, A), (D, B), (D, D), (D, E), (D, F), (E, _), (E, A), (E, B), (E, D), (E, E), (E, F), (F, _), (F, A), (F, B), (F, D), (F, E), (F, F), (B, A), (C, A), (D, A), (E, A), (F, A), (_, A), (B, C), (C, C), (D, C), (E, C), (F, C), (B, D), (C, D), (D, D), (E, D), (F, D), (_, D), (B, E), (C, E), (D, E), (E, E), (F, E), (_, E), (B, F), (C, F), (D, F), (E, F), (F, F), (_, F)

complement of (A, D): (B, _), (C, _), (D, _), (E, _), (F, _), (_, A), (_, B), (_, C), (_, E), (_, F)

...

Note how (B, _) and (B, A) both end up in the unhandled list, though they are redundant. What's needed is some sort of de-duping, a pattern union function that returns a representation of pattern unions.

Once you have a proper type to represent pattern unions and a union function, you might as well keep a list of handled cases rather than unhandled cases.

In the worse case, the asymptotic size of this handled data structure would be O(n) with the number of cases in the case statement--since it would have at most one new entry for each case. When handled cases could be combined into a simpler case, they would be, resulting in a union structure with fewer entries.

[evancz]

Cool, yeah, that's just like the example we have about months.

Thanks for explaining the root problem here and suggesting a better way! It is quite a clear explanation :)

If you think you can take a swing at it, great! If you think it'll be a while, would you mind writing the core idea up in a gist so we can share the project on https://github.com/elm-lang/projects and the mailing list? I can get to it eventually, but this seems like a nice opportunity for a contributor, especially because it's a pretty cool problem :)

[evancz]

The part about only keeping handled cases is confusing me. In cases like this:

zip list1 list2 =
  case (list1, list2) of
    ( [], _ ) -> list2
    ( _, [] ) -> list1

I don't quite get how the handled vs. unhandled distinction comes into play here. In any case, having a more dense representation of "not handled" makes a lot of sense to me.

[brianhempel]

Thanks for that short example. I think I was about to do it wrong.

Note that a precise "unhandled" list has the potential to be very large.

type Letter = A | B | C | D

incomplete x y =
  case (x, y) of
    (A, A) -> True

handled   = [(A, A)]
unhandled = [(A, B), (A, C), (A, D), (B, A), (B, B), (B, C), (B, D), (C, A), (C, B), (C, C), (C, D), (D, A), (D, B), (D, C), (D, D)]

You could make a more efficient representation of "unhandled" cases by creating a representation for "everything except (A, A)", but then you're just keeping track of the "handled" cases by a different name.

@kavon pointed out to me that 1985 tree pattern match compilation paper says that exhaustiveness and redundancy can be easily determined during pattern match compilation. My current plan is to take a look at that to see if some of the decision tree code can be reused here or if checking could be done during the tree compilation.

[evancz]

I think "can be easily determined during pattern match compilation" is probably a pretty big overstatement ;)

The pattern match compiler is based on When Do Match-Compilation Heuristics Matter? which came 15 years later and summarized all the work that happened in those years. A decent amount!

So maybe these can be brought together, but I think this is a riskier route. I think the denser representation can get us a big improvement without a reimplementation of all this stuff. And that can help us learn more in preparation for something more intense.

[brianhempel]

Could you check for redundancy by verifying that all given cases appear as leaves in the compiled decision tree? Missing cases are redundant.

And could exhaustiveness be verified by internally adding a wildcard as the last case before compilation and then verifying that this last cases does not appear in the compiled decision tree?

[evancz]

I'd have to revisit the code to comment with any certainty.

The exhaustiveness checker also finds redundant patterns. Overall, I would recommend against trying to unify these two things. I don't know of any other compiler that does that, and if we are going to be the first, I think we should do the easier changes first. By having them separate, we also make it possible to skip running the optimizer when we have an -O flag.

[brianhempel]

F# checks for both redundancy and exhaustiveness during pattern compilation.

[brianhempel]

On inspection, it appears that SML/NJ's FLINT compiler and the pattern match compiler in the MLRISC library also both check for redundancy and exhaustiveness during pattern compilation.

[brianhempel]

MLton, as well, appears to use information gathered during match compilation (specifically, the number of uses of each pattern) to check redundancy and exhaustiveness.

[evancz]

Okay, maybe this is the way to go, but it is definitely the harder way. If you and can show this approach is faster and won't architect us into a corner, that's awesome! I'd say, just keep folks on elm-dev in the loop.

[brianhempel]

If this issue is still outstanding in 2.5 months (Nov. 16, to be exact) I will whip up a PR.

[evancz]

Haha, sounds good! :)

[evancz]

I did some work on this last night and I've sped things up very significantly based on Warnings for Pattern Matching by Luc Maranget.

As far as I can tell, OCaml and SML do exhaustiveness checks and pattern match compilation in separate phases. With the new changes, both of these parts of the compilation pipeline are a very tiny fraction of the overall cost, so I'm not sure there's a ton to be gained with further optimizations.