## Stream: lean4

### Topic: Surprising syntax error

#### Gabriel Ebner (Mar 12 2021 at 16:06):

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)


#### Andrew Kent (Mar 12 2021 at 17:26):

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 (Mar 12 2021 at 17:45):

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 (Mar 12 2021 at 18:17):

@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 (Mar 12 2021 at 18:19):

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

#### Leonardo de Moura (Mar 12 2021 at 18:23):

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 (Mar 12 2021 at 18:24):

I see, thanks, that makes sense!

#### Leonardo de Moura (Mar 12 2021 at 18:27):

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 (Mar 12 2021 at 18:39):

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

#### Mario Carneiro (Mar 12 2021 at 18:40):

it's not even in a do block

#### Leonardo de Moura (Mar 12 2021 at 18:40):

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

#### Gabriel Ebner (Mar 12 2021 at 18:41):

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

#### Mario Carneiro (Mar 12 2021 at 18:41):

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

#### Mario Carneiro (Mar 12 2021 at 18:41):

that's the part I'm not getting

#### Mario Carneiro (Mar 12 2021 at 18:42):

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 (Mar 12 2021 at 18:45):

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 (Mar 12 2021 at 18:46):

@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 (Mar 12 2021 at 18:48):

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

#### Mario Carneiro (Mar 12 2021 at 18:48):

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 (Mar 12 2021 at 18:50):

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 (Mar 12 2021 at 18:51):

One thing that comes to mind is alignment like:

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


#### Gabriel Ebner (Mar 12 2021 at 19:11):

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 (Mar 12 2021 at 19:15):

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 (Mar 12 2021 at 19:27):

Note that we can use

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


Last updated: May 18 2021 at 22:15 UTC