RFC: guard patterns

[omentic]

This is split out of #371.

I would like to see support for match guards: some sort of boolean clause attached to a match branch which must return true if the branch is to be taken. These guards can refer to the variables bound in the branch of the match. The syntax might look like the following:

inductive Foo where
| bar (a b c : Nat)
| baz (a : Nat)
| bazinga (b : Nat)

let foo := Foo.bar 1 2 3
match foo with
| .bar a b c if a = b * c => ...
| .bar a b c => ...
| .baz a | .bazinga a if a = a * a => ...
| _ => ...

On the analysis side, this would work by removing the guarded branches from exhaustivity checking. If a pattern has a guard, the pattern has to appear later to satisfy the exhausitivity checker. (I think it would be counterproductive to attempt to analyse the guard clauses.) In the example above, the guard on the first clause means that Lean requires a second .bar case for all the cases not covered by the guarded clause, and the guard on the third clause means there must exist later .baz and .bazinga clauses too (or a catchall).

In the case of guards on multiple patterns (| .baz a | .bazinga a), the guard is taken to apply to each pattern.

I find myself wanting this fairly often. It exists in a number of other languages: Rust, Python, etc. It's useful for separating out cases semantically when normal pattern matching doesn't cut it and is pretty readable to boot.

[nomeata]

I've wanted them myself often as well. However, match compilation is already a very complicated beast and has to worry about verification, completeness checking, equation generation with correct overlapping conditions etc. Presumably that's why we don't have them (yet).

Often a chain of if let combined with if is a close approximation, possibly with with Id.run do and return for early return, maybe that helps in your cases.

[omentic]

Yeah, it's mostly just a syntax thing. I make do with nested conditionals as-is but I find myself missing them.

[nomeata]

Do you miss them only when doing plain programming, or also when you write functions that you want to verify?

[omentic]

Only when doing plain programming. (This is what I mostly use Lean for 😁)