Exponential compile time with respect to constructors nesting level

Ecosystem
,
1

I have narrowed down a minimal reproduction to the following code:

type 'a elt =
  | A : unit elt
  | B : unit elt
  | C : unit elt
  | D : unit elt
  | E : unit elt
  | F : unit elt
  | G : unit elt
  | H : unit elt

module List = struct
  type 't t =
    | ( :: ) : 'hd elt * 'tl t -> ('hd * 'tl) t
    | [] : unit t
end

let f List.[ _; _; _; _; _; _; _ ] = Printf.printf "woops"

The compile time of this unit is exponential (or something akin) over the size of the final pattern matching. Run time of ocamlc test.ml version 4.12.1 depending on the nesting level of the final pattern matching (ie. 0 is List.[], 1 is List.[ _ ], etc):

0: time: 0.113 real
1: time: 0.115 real
2: time: 0.116 real
3: time: 0.129 real
4: time: 0.226 real
5: time: 0.954 real
6: time: 6.737 real
7: time: 54.016 real

I tested with 4.13.1 and the problem persists. The size of the 'a elt variant seems to also have an exponential effect of compile time. Overall it roughly looks like we’re exponential over variant size * pattern nesting level.

Interestingly, this can be worked around by splitting the pattern matching in multiple steps:

(* This takes 25 seconds to compile *)
let f list =
  let List.[ _a; _b; _c; _d; _e; _f; _g ] = list in
  Printf.printf "woops"

(* This is equivalent and takes 22ms to compile *)
let f list =
  let List.(_a :: _b :: _c :: _d :: list) = list in
  let List.[ _e; _f; _g ] = list in
  Printf.printf "woops"

I’m wondering if we’re hitting some actual exponential complexity in the typing algorithm, although the second version being equivalent and instantaneous sort of hints the typer could type it efficiently – but I might be wrong there.

3 Likes
2

This is partially the expected behavior of the exhaustiveness check for pattern matching in presence of GADTs: checking that the pattern [ _; _; ... ] with n-nested _ is exhaustive requires to check that there is no value of shape _ :: _ :: _ :: ... :: _ with n+1 _ for the inferred type . In other words, your code is equivalent to:

let f x = match x with
| [ _; _ ;_ ] -> Printf.printf "woops"
| [] -> .
| [ _ ] -> .
| [ _ ; _ ] -> .
| _ :: _ :: _ :: _  -> .

and the compiler has to check that the refutable patterns ([], [], [; ]and :: _ :: _ :: _`) are really not possible. And this check is fundamentally undecidable for arbitrary patterns (see https://www.math.nagoya-u.ac.jp/~garrigue/papers/gadtspm.pdf).

Since the test is undecidable, OCaml uses the number of _ in patterns as an indication of how much effort it should spend trying to prove that there is no counter-example. More precisely, it explodes every _ once for sum types with more than one constructor. Types with morally one constructor are expanded at most 5 time however (and strangely that matters here) . Thus, the time spent checking exhaustiveness might grow exponentially with the number of _. However, knowing this behavior, you can design the types to guide the exhaustiveness checker to avoid doing the expansion at the wrong place:

type 'a hidden = Hide of 'a [@@unboxed]
type 'a h2 = 'a hidden hidden
type 'a h4 = 'a h2 h2
type 'a h5 = 'a h4 hidden

module List = struct
  type 't t =
    | ( :: ) : 'hd elt h5 * 'tl t -> ('hd * 'tl) t
    | [] : unit t
end
let f List.[ _; _; _; _; _; _; _ ] = Printf.printf "woops"

Here, by hiding the elt type beyond 5 layer of expansion of the 'a hidden type, we ensure that the exhaustiveness check never explodes the elt type and we recover a linear behavior in the number of _.

This example suggests that the exhaustiveness checker might be missing an optimisation for those cases where exploding no _ is enough.

1 Like
3

Makes sense, the behavior is justified although it looks like this specific use case could be optimized.

Regarding the 5 levels of nesting, is that a simple heuristic or is there an actual proof that a value with the correct shape cannot occur past that limit? In the one hand I don’t suppose the typer would let a non-exhaustive pattern through, but the limit seems sort of arbitrary from an external point of view.

In any case, the “splitting the pattern in multiple steps” definitely seems more friendly than nesting the GADT 5 levels deep. Now that I have a better understanding of the reason why, I’ll update with any better solution if I work on out in the future.

Thanks !

4

The 5 level of nesting is a consequence of the way the refutation clause checker spend fuel while trying to check that there is no counter-examples: it spends 0.2 units of fuel when exploding one _ wildcard into exactly one constructor, and 1. unit when exploding a wildcard in more than one constructor. Once the fuel is spent, no more wildcard is exploded.

The limit is arbitrary, but this just means that the typechecker will reject valid refutation clause by lack of fuel (thus rejecting a potentially valid program). This is the safe option, and it is possible to be more explicit in the patterns (aka add more wildcards) to convince the typechecker to try harder. (As an extreme example, this strange pattern matching in this file typed-musings/tour.ml at master · Octachron/typed-musings · GitHub is here to give enough fuel to the refutation clause checker to check that there is no knight’s tour on a 3-by-3 chessboard.)

A possible solution that might work would be a way to fine tune the fuel used for refutation clause: in your example, refuting the missing pattern cases is simpler if the refutation checker is not given any fuel and thus do not try to explode any wildcards.

1 Like