lean4
lean4 copied to clipboard
leanprover
RFC: `if let` chains
Decrease redundancy in cases like
if let c a := x then
if q a then
y
else z
else z
...
by supporting mixed let/condition chains like
if let c a := x && q a then
y
else z
...
This is a syntactic idea I thought was too wild to even propose, until I learned that Rust will have it, so obviously it must be a good idea.
Probably even more than for Rust though, parsing this is a bit of an issue. The cleanest approach I could come up with so far is to keep basic if syntax intact and introduce new chain syntax for subterms of precedence greater than &&/∧ only.
syntax letChainElem := "let " term " := " term:36 -- "&&"/"∧" have precedence 35
syntax (priority := low) "if " sepBy1(letChainElem <|> term:36, "&&", " && " <|> " ∧ ") " then " term " else " term : term
#check if let x := a && p x then c else d -- parsed as elements `[let x := a, p x]` (after removing current `if let` syntax)
#check if let x := a && let y := b then c else d -- parsed as elements `[let x := a, let y := b]`
#check if a || b then c else d -- parsed by basic syntax
#check if a || b && let x := a then c else d -- parse error, incomplete term `let`
#check if (a || b) && let x := a then c else d -- parsed as elements `[a || b, let x := a]`
#check if a then b else c -- parsed by both, disambiguated by priority
Desugaring: obvious, modulo introducing join points
Isn't it possible to use notFollowedBy to parse the && in this case, instead of using high precedence (which would also affect if let x := <low prec expr> then e1 else e2)?
if let x := <low prec expr> then e1 else e2
Oops, now I remember what I thought was the tricky case! The problem with notFollowedBy is that it would yield a pretty unexpected result on if let x := f <| p && q, wouldn't it? But perhaps that's acceptable...
Does this mean that and becomes shortcircuiting? This would be so awesome.
if (← expensive) && (← slow) then
-- does not execute `slow` if `expensive` returns false
plowSnow
We could also use a keyword as separator:
if let .some x := a and let .some y ← f x then
return (x, y)
Oh my, it looks like we're only further diverging from regular &&. In that case a new keyword does seem like the better approach. I wanted to introduce and anyway as mutual infix syntax, which does not collide with use in if. Good thing the type is now called And!
Grepping for it (which is hard...) reveals some uses in inductive types denoting formula syntax. and is a pretty high-demand identifier name.
rec is also a pseudo-keyword, right? Can we do something like that, say that and is not legal unparenthesized inside the condition of an if let statement? That's a much lower fallout compared to making and a keyword, although I think we can't do the same trick if we want an infix command operator for mutual blocks.
By the way, the impact of registering constructor names as tokens has been lowered significantly by accepting them unescaped in inductive declarations and by introduction of the leading dot syntax.
I'm not totally against it, but it would need some publicity on zulip first I think to get people on board with the idea. I expect that for a lot of folks this is just a pure loss because they weren't planning on using if let in the first place.
Despite being generally adverse to new keywords, I think making and a keyword for this is a good idea. For one, Python already uses and as a keyword for stuff like this, so there is a low introduction cost -- even for some mathematicians who may have already dabbled a bit in Python. Second, most of the stuff the identifier and is used for already has more sugary notation, so I would imagine this would break much existing code.
@digama0
I expect that for a lot of folks this is just a pure loss because they weren't planning on using
if letin the first place.
By 'folks', do you mean mathematicians or do you fin if let less useful more generally? I personally use if let a lot in programming code, but it does seem less useful in math code. However, I would still appeal to Python style to argue that and being a keyword is reasonable.
I mean mathematicians. I use if let all the time, and I would use if let chains if they were available, but if you are spending your time doing proofs in lean 4 I would not be surprised if you come across and more often than you come across if let.
An alternative syntax without keywords. We already have a "let chain" syntax:
-- One-linear
let x := a; let y := b; x + y
-- Multi-line
let x := a
let y := b
x + y
Then it seems natural to have a similar syntax in if:
-- One-linear
if let some x := a; let some y := b; then x + y else 0
-- Multi-line
if let some x := a
let some y := b
then
x + y
else
0
-- Mixed let/condition
if let some x := a; x < 10 then x + 1 else 0
By chance, the last syntax is similar to C++'s if with initializer.
Unfortunately, that syntax overlaps with regular let expressions inside the conditional. That is, if let x := a; b then c else d is already valid syntax and means if (let x := a; b) then c else d. I suppose the if could parse the conditional using the regular term parser and then post-process it to treat any unparenthesized top level let in a special way... but let x := a; let y := b is not an expression, and let x <- a certainly isn't an expression.
I found some things in the recent "The Ultimate Conditional Syntax" by Chang and Parreux to be compelling, and I think it would be worth considering a design that could one day support some of their more elaborate forms, at least in principle.
One solution here would be to make let PATT := VAL valid syntax on its own, then make if have its own elaborator for conditionals, with support for &&, this let, and matches. The wrinkle is that you need to write parentheses for chains:
if (let .some x := a) && let .some y ← f x then
return (x, y)
Perhaps this let PATT := VAL syntax would elaborate like a matches expression when it appears outside an if, or maybe it gives an elaboration failure to let you know the pattern would be binding any variables. Though in this example, it's nice if if could be aware of let terms as well, like in the discussion from the previous two comments:
if let .some x := a; let .some y ← f x then
return (x, y)
For an example of the more elaborate forms from the paper, here's a possible Lean version of one from the end of page 2:
if x matches
| .inr none then defaultValue
| .inr (some cached) then f cached
| .inl input && compute input matches
| none then defaultValue
| some result then f result
But as you can see this would be a very big change to the if parser!
