RFC: removing let pattern matching

[Command-Master]

Proposal

Currently pattern matching with let doesn't keep the definition of the value. I believe this conflicts with the rest of the behavior of let and is confusing, especially for new users (example 1, example 2, example 3), and so should be removed or linted against, and have pattern := value will have to be used instead.

An alternative option is to change it to keep the value, e.g. let (a, b) := l will behave like let a := l.1; let b := l.2, but this will require more effort.

Community Feedback

Zulip discussion.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[nomeata]

Reasonable suggestion, although a bit counterintuitive for uses of Lean as a functional programming language.

It may make sense for mathlib to implement a linter for this, and enforce this there (first), and if that works well reconsider if this should be the general rule for lean.

[lecopivo]

I would really like to see this changed. I ran into this problem when writing simp theorems for simplifying code were I care about let bindings and let patterns on rhs of the theorem was not behaving as I expected.

I would really like if let (a, b) := l de sugars into let ab := l; let a:= ab.1; let b:= ab.2. The additional ab let is there because l can be non trivial computation.

I think that in my use case of simp theorems, an alternative solution could be to add something likezetaIota option to whnf which would reduce match statement but would introduce appropriate let bindings. For example match (x,yz) with (a,b,c) => f a b c would be reduced to let a := x; let bc:= yz; let b := bc.1; let c := bc.2; f a b c. However, I don't think this solves the original issue.

[Kiiyya]

I ran into this problem as well. It would be sweet if let (a, b) := x desugars into let a := x.1. I imagine this will be non-trivial to generalize and get the metaprogramming right for anything other than product types though, but at least having product types is neat. What about inductive T : Nat -> Type | foo : String -> T 0 | bar : Nat -> T 1, and then let (.foo s) := t given t : T 0?

Alternatively, let h@(a, b, c) := x as a shorthand for match h : x with (a, b, c) => ..., but I am not a fan of this as much as the above.

[Kha]

Result from triage team discussion: we agree that this behavior can be confusing, but the alternatives are confusing to programmers as well. It also conflicts with #3559. Thus we don't see a way to acceptance; a downstream linter like mentioned by Joachim would be a better approach.