Surprising syntax error

Stream: lean4

[Gabriel Ebner]

I wouldn't have guessed where the error is reported here:

partial def frob : Nat → Nat | i =>
if i > 10 then frob 5 else frob (i-1)

The error is expected 'else' right at the 5. It works if you write (frob 5).

But apparently I have no intuition for indentation-sensitive syntax.

[Andrew Kent]

Interestingly the same error doesn't occur when the function is written like this:

partial def frob (i : Nat) : Nat :=
if i > 10 then frob 5 else frob (i-1)

[Julian Berman]

Might be a much simpler thing, but I also noticed a bit of differing syntactical behavior with else, specifically this works: #check (do if true then return PUnit.unit : PUnit) because it macro expands to an if/then/else with the else present, but otherwise outside of do the else is always required

[Leonardo de Moura]

@Gabriel Ebner The weird error message is due to the whitespace-sensitive indentation rules. I added a missing constraint, and the error message is now at the if, and it says

2:0: error: expected alternative right-hand-side to start in a column greater than or equal to the corresponding '|'

Does it make sense to you?

[Gabriel Ebner]

Anything that points towards indentation is great. I didn't make that connection at all.

[Leonardo de Moura]

Julian Berman said:

Might be a much simpler thing, but I also noticed a bit of differing syntactical behavior with else, specifically this works: #check (do if true then return PUnit.unit : PUnit) because it macro expands to an if/then/else with the else present, but otherwise outside of do the else is always required

These are two different if-terms. You should view the do-notation as a domain-specific language for writing effectful code. The if without an else is the equivalent of Haskell when.

[Julian Berman]

I see, thanks, that makes sense!

[Leonardo de Moura]

Gabriel Ebner said:

Anything that points towards indentation is great. I didn't make that connection at all.

Do you think this restriction is reasonable? There are different ways to address this issue, but we don't want to give up on whitespace sensitivity.
If you are interested I can describe the parser combinators we use to specify these constraints.

[Mario Carneiro]

It's on one line though. Why would whitespace sensitivity come in? I thought that was just for multiline expressions

[Mario Carneiro]

it's not even in a do block

[Leonardo de Moura]

It is two lines. The alternative | i => starts in the first line.

[Gabriel Ebner]

There are always tradeoffs when it comes to indentation-sensitive syntax. I think we can get used to it.

[Mario Carneiro]

is the else somehow associating to the | i =>?

[Mario Carneiro]

that's the part I'm not getting

[Mario Carneiro]

Or is it just that the if starts in the first column and you aren't allowed to do that anymore (at least if you use the equation compiler syntax)

[Mario Carneiro]

Do you think this restriction is reasonable? There are different ways to address this issue, but we don't want to give up on whitespace sensitivity.

I at least would like to find a way to preserve this kind of pattern (assuming we can figure out what the pattern is) while also keeping whitespace sensitivity when code is formatted to take advantage of it

[Leonardo de Moura]

@Mario Carneiro The issue is not really the if, but the application frob 5. The application parser enforces that the next argument must occur in a column greater than the one in "the context". This is how we can parse code such as

@[simp] theorem List.length_cons {α} (a : α) (as : List α) : Eq (cons a as).length as.length.succ :=
  let rec aux (a : α) (as : List α) : (n : Nat) → Eq ((cons a as).lengthAux n) (as.lengthAux n).succ :=
    match as with
    | nil       => fun _ => rfl
    | cons a as => fun n => aux a as n.succ
  aux a as 0 -- This is not part of the previous application

[Leonardo de Moura]

The "context" is updated using the combinator withPosition p where p is a parser

[Mario Carneiro]

One observation I can make about the difference between that example and Gabriel's is that in your example the | .. => is the first thing on the line, i.e. it has higher indentation than the aux a as 0 on the following line

[Mario Carneiro]

What kind of trouble do we get into if we use the first non-whitespace character in the line instead of the | character to define the baseline?

[Mario Carneiro]

One thing that comes to mind is alignment like:

fun | 0 => f x
    | n+1 => f x
f x

[Gabriel Ebner]

Mario Carneiro said:

I at least would like to find a way to preserve this kind of pattern (assuming we can figure out what the pattern is) while also keeping whitespace sensitivity when code is formatted to take advantage of it

This particular pattern is no longer necessary in Lean 4. When you write a function with well-founded recursion, you no longer need to indicate which of the arguments change in the recursive call. This works now:

def foo (n : Nat) : Nat :=
if h : n > 0 then foo (n - 1) else 42

[Mario Carneiro]

A slight variant on this indentation pattern is when matching on something, i.e.

def foo : A x B -> C | (a, b) :=
f a b

I don't think preserving this is particularly important though, since it's less common than

def foo : A x B -> C
| (a, b) := f a b

[Leonardo de Moura]

Note that we can use

def foo : A x B -> C := fun (a, b) =>
f a b