RFC: `while let`

Stream: lean4

[Marcus Rossel]

We all know and love if let notation, right? What do people think about having analogous notation when using while? Then you can write something like:

let mut n? : Option Nat := 0
while let some n := n? do
  n? := doSomething n

This would behave the same as:

let mut n? : Option Nat := some 0
repeat
  if let some n := n? then
    n? := doSomething n
  else
    break

(Both Rust and Swift also have this feature.)

[Max Nowak 🐉]

Rust also has this feature. It would be handy I think.

[Chris Henson]

lean4#1996

[Cameron Zwarich]

My favorite substitute:

repeat
  let some n := n? | break
  ...

[Niels Voss]

I'm a bit worried about Lean adding too much syntax sugar to core, since anything added to core will likely remain in the language forever. Adding more syntax sugar in core also makes it harder to make a second implementation of Lean in the distant future. IMO we should be taking advantage of Lean's metaprogramming to implement new language features outside of core where they have a lower cost.

[Henrik Böving]

Adding more syntax sugar in core also makes it harder to make a second implementation of Lean in the distant future.

This is basically impossible with the fragility of the core algorithms of Lean combined with how much projects (knowingly or unknowingly) rely on details. There are certain files in core where basically any change will break a proof in mathlib.

[Chris Henson]

I agree with @Niels Voss. The issue I linked above has a comment showing a macro to define while let.

[Kyle Miller]

That's a valid worry, however in this case, isn't it added cognitive complexity that while doesn't accept the same condition syntax as if?

[Kyle Miller]

The unless syntax probably shouldn't have full if condition syntax though... or at least it could parse and then have an error (the body of the unless joins back into a context where there could be some extra pattern variables)

[Eric Wieser]

Perhaps unless let .some x := x? then return could emit an error saying "write let .some x := x? | return instead"?

[Eric Wieser]

Though there are a lot of cases where I've wanted

unless h : P x do
  throw "oops"
-- now have `h`

and

let .isTrue h := inferInstanceAs (Decidable (P x)) |  throw "oops"

is a bit unwieldy

[Marcus Rossel]

Kyle Miller said:

isn't it added cognitive complexity that while doesn't accept the same condition syntax as if?

That's at least how it is for me. I want to write while let and then have to think about what the best workaround is. And seeing as @Cameron Zwarich already has a favorite substitute, I'm guessing I'm not the only one :smile:

[Marcus Rossel]

But also, changes/extensions to do-notation are being postponed until the implementation of do-notation is reworked, right?

[Robin Arnez]

Well, while, repeat, etc. aren't part of do notation; they are just macros for for _ in Lean.Loop.mk do ... so I believe it's not so strict? Not entirely sure though