match_expr functionality?

Stream: lean4

[Thomas Murrills]

I was curious if there are any plans to extend the functionality of match_expr, or if its intended scope is specifically simple .app and .const matches.

I tried replacing Qq matches in Mathlib with match_expr, and found that almost none of them could be replaced. Some necessary features simply weren't available, whereas some matches couldn't be replaced without making the code verbose and difficult to read. (Readability and brevity is especially important for maintainability here, of course, since the regions of code that require matching against expressions are often already verbose and relatively esoteric.)

I'm not insisting that the scope be expanded if this is the intended scope, necessarily—I'm just curious as to what its intended role is and where it's going. :)

If it's of interest, here are the issues I encountered.

• Inability to match against or bind universes
• Inability to match against nested .apps, leading to less-readable nested match_exprs with duplicated _ => branches
• Inability to match against multiple Exprs simultaneously (e.g. match_expr a, b with | foo e, bar f => ...), unlike match, leading to nested match_exprs and duplicated branches
• distinction from match means that you can't simultaneously match against some other non-Expr value (e.g. a Level, or a structure which contains an Expr) at the same time, leading to nested/interleaved match/match_exprs, often with duplicated _ => branches
• Matching only against the head means that we can't match on arguments—e.g. we'd like write something kind of like match_expr e with | Eq Nat a b => ... which only matched Nat equalities, but Nat is necessarily a variable name here (contrast with match). This likewise contributes to nested match_exprs or more verbose checks.
• Inability to use notation, meaning that matching against things like + (or worse) quickly becomes verbose and difficult to read (and would be even more difficult if nested matches were allowed)
• incompatibility with Qq while matching: one can't add Qq type annotations to the matched-against identifiers in the match itself, meaning that you need a string of let a : Q(X) := a's in the body of each alt to use Qq, rendering it frequently impractical. (Qq is often necessary to legibly construct expressions, so abandoning it becomes impractical.)

(Interestingly, inability to match against anything but constants and applications didn't actually come up.)

[Eric Wieser]

I think there's a more crucial gap there, which is "no defeq matching", which is crucial for matching against a + b

[Eric Wieser]

My main wish for match_expr would be for it to be generalized to extensible match handlers; match_expr could then be match e with ~e(Nat.add $x $y) =>, and Qq could hook into the same machinery. A wide class of bugs in Qq (return, continue, let mut not working with it) are due to it being a second-class citizen that is not permitted to take part in the do control-flow rewriting

[Eric Wieser]

(Of course, match_expr is still great, and the choice to make it different syntax to match meant that it landed much more quickly than designing such an extension mechanism, leaving plenty of time to unify things the "right" way later)

[Henrik Böving]

Eric Wieser said:

I think there's a more crucial gap there, which is "no defeq matching", which is crucial for matching against a + b

I'm not 100% certain on this but as I understand match_expr is supposed to be a light weight tooling that does not call into potentially expensive things like isDefEq.

Maybe @Leonardo de Moura can explain his vision for match_expr?

[Eric Wieser]

To be clear, my point there was to say why match_expr is not a substitute for Qq; it certainly has a niche

[Eric Wieser]

And I think that niche is well-aligned with not supporting nested expressions or typeclass-based notation, as those are both places where using whnfR before matching isn't enough

[Thomas Murrills]

Eric Wieser said:

I think there's a more crucial gap there, which is "no defeq matching", which is crucial for matching against a + b

True! It would be great to have a way to support defeq matching somehow, as it is not infrequently crucial, but I will note that many Qq matches in Mathlib did not seem to need defeq matching, and were blocked only by the other issues.

[Eric Wieser]

Mathlib used to be full of defeq-matching mistakes, but it was hard to tell as an end-user; I fixed many of these in !3#18129

[Thomas Murrills]

Yeah, it is also possible that the defeq matching is actually crucial in most ~q matches despite how it seemed on first glance...