Zulip Chat Archive

Stream: lean4

Topic: Surprising syntax error


view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (Mar 12 2021 at 18:19):

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

view this post on Zulip 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.

view this post on Zulip Julian Berman (Mar 12 2021 at 18:24):

I see, thanks, that makes sense!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 12 2021 at 18:40):

it's not even in a do block

view this post on Zulip Leonardo de Moura (Mar 12 2021 at 18:40):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 12 2021 at 18:41):

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

view this post on Zulip Mario Carneiro (Mar 12 2021 at 18:41):

that's the part I'm not getting

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Leonardo de Moura (Mar 12 2021 at 18:48):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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