Why even try the semantic constraints, if expression can't match the pattern structure?

Question

This result is unexpected:

Trace[MatchQ[{7}, {_?NumberQ, __}], NumberQ] (* ->  {{NumberQ[7], True}} *)

Why evaluate NumberQ if the pattern can't conceivably match? What kind of side-effect might change the expression arity during pattern-matching?

Precisely, due to the unbound side-effects and for performance reasons, I would have thought that the matcher would labor very hard to avoid invoking the evaluator.

Note that other cases are not surprising:

Trace[MatchQ[{7}, {_?NumberQ, _}], NumberQ] (* -> {} *)

Trace[MatchQ[{7}, {_?NumberQ, ___}], NumberQ] (* ->  {{NumberQ[7], True}} *)

The combination of a constraint and BlankSequence seems to make the pattern-matcher overly suspicious. So, "a list of two expressions, first one a number" bypasses the evaluator; "a list of two or more expressions, first one a number" triggers the evaluation of the restriction.

Optimization of pattern-matching is unresolved in general. In the context of expressions in the form head + n parts, however, trying to calculate the lower bound of n for the class of expressions represented by a pattern strikes me as one of the obvious problems to focus on.

Given the experience of these last weeks, though, the struggle between my intuition and Mathematica is always won by the latter. What am I missing, then?

Update:

Mr.Wizard and Leonid Shifrin discussed a few years ago about the uneasy relation between the evaluator and the pattern-matcher.

Answer 1

This is closely related to my own questions posted a few years ago on Stack Overflow:

• PatternTest not optimized?
• Mathematica's pattern matching poorly optimized?

I still am not convinced that some of these patterns could not be better handled but I have come to accept that such things are not likely to change. Although it can be argued that such methods are "perverse" it can fairly easily be demonstrated that such side-effects can be used. Consider:

i = 0;

count[x_] := (If[x > 0, i++]; True)

Cases[{{1}, {-3}, {2}, {0, 4}}, {_?count, __}, ∞]

i

{{0, 4}}

2

This counts the number of (sub)lists that start with a positive number at the same time as a different match is returned by Cases. Again, I would try to avoid such methods myself, but since these methods have been possible changing the language now could have unintended consequences. At first it might seem that NumberQ is safe from such side-effects, but the language allows its redefinition with e.g. Block so all bets are off.

I'm afraid such changes might only appear, if ever, in a "reboot" of the language; a kind of "Wolfram Language 2.0" I suppose. Sadly I think such things are not a priority to the developers, but I do hope to some day see a smaller, cleaner, and faster core language implemented, with a highly optimized pattern matcher, JIT compilation etc.

As a more realistic alternative perhaps it would be possible to introduce a new Head that affects pattern matching (much as HoldPattern or Verbatim do now) that would declare a pattern to be "pure" and without side-effects, which would trigger additional optimizations. Nevertheless having to use this Head every time you wanted optimal behavior for patterns that do not involve side effects would seem very clumsy.