Make `AppExpr` binary

[ice1000]

Currently, AppExpr is already semibinary (the generated AppExpr from binary operator parser is already kinda binary, f a b is translated into (f a) b), and why not make it entirely binary?

[ice1000]

I should insert some pun, but I don't find a good one.

[tonfeiz]

What do you mean by "entire binary"?

[ice1000]

@tonfeiz Just "binary".

[ice1000]

@imkiva what do you think about this

[imkiva]

What is 'just binary'

[re-xyr]

have you found your pun?

[ice1000]

What is 'just binary'

Like, AppExpr(Expr func, Expr arg) instead of AppExpr(Expr func, Seq<Expr> arg)

[ice1000]

have you found your pun?

No. I wanted to make a joke 'bout gender nonbinary but I failed.

[re-xyr]

It's analog

[tonfeiz]

What is 'just binary'

Like, AppExpr(Expr func, Expr arg) instead of AppExpr(Expr func, Seq<Expr> arg)

I think this is a kind of refactor, however it seems that we still have some places filled AppExpr with more than 1 argument.

For example,

else return new Expr.AppExpr(
      computeSourcePos(op.expr.sourcePos(), lhs.expr.sourcePos(), rhs.expr.sourcePos()),
      op.expr,
     ImmutableSeq.of(lhs.toNamedArg(), rhs.toNamedArg())
   );

in BinOpParser, around line 120. What does that mean?

I can take this, but I'll have to ask you guys if I find situations similiar to the one above. :rofl:

[ice1000]

It's analog

I'm pretty sure I was using the right words

[re-xyr]

I'm pretty sure I was using the right words

i'm just helping you find some jokes

[ice1000]

What does that mean?

I think it's pretty obvious from the names of the variables. If you wanna know more, it's a good idea to run TestRunner and set a breakpoint here.

[tonfeiz]

What does that mean?

I think it's pretty obvious from the names of the variables. If you wanna know more, it's a good idea to run TestRunner and set a breakpoint here.

Maybe I'm not expressing myself very well...I can understand the code, but how shouid I deal with this kind of code?

I mean if this is just a kind of refactor, then I expect all AppExpr should only have one argument, which is not the situation here.

Or is this exactly what you want —— change the code to deal with all these kinds of situations using just binary ops?

[ice1000]

@tonfeiz Just use currying

[ice1000]

@tonfeiz App(e, [a, b]) → App(App(e, a), b)

What's the problem?

[tonfeiz]

@tonfeiz App(e, [a, b]) → App(App(e, a), b)

What's the problem?

That's what I want to ask :joy:. I don't know why we didn't just use currying in makeBinApp before, and there are many conditions in the method. So I want to know is there any special reason for this? If so I should deal with those in other places.

[tonfeiz]

Anyway, I'll start to do this from tomorrow. It's a good chance to know the desugar process after all.

[ice1000]

@tonfeiz App(e, [a, b]) → App(App(e, a), b)

What's the problem?

That's what I want to ask :joy:. I don't know why we didn't just use currying in makeBinApp before, and there are many conditions in the method. So I want to know is there any special reason for this? If so I should deal with those in other places.

Probably no special reason lol

[re-xyr]

I'm also curious why. If binary application is so good, we won't go another way without a specific reason. I guess a long time ago, we did have binary AppExprs, but then we changed them for parsing convenience.

[ice1000]

I'm also curious why. If binary application is so good, we won't go another way without a specific reason. I guess a long time ago, we did have binary AppExprs, but then we changed them for parsing convenience.

Yes. Initially, we parse a list of terms as an application term. Then, all of a sudden, with binop parser and the desugaring phase introduced, the spine application concrete expr became unpleasant to work with.

[tonfeiz]

Is it possible for AppExpr's function to be a instance of RawUnivExpr? I've tried all test cases and could't find one.

The only case I can think of is Type u v, which I think it's meaningless...

[ice1000]

Is it possible for AppExpr's function to be a instance of RawUnivExpr? I've tried all test cases and could't find one.

Yes but only before desugar.

The only case I can think of is Type u v, which I think it's meaningless...

This syntax is gone, only Type u is available

[tonfeiz]

Yes but only before desugar.

Could you give me a case in concrete syntax? I couldn't think of any. I've added a breakpoint at the corresponding place before desugar, but all cases just don't enter there.

[ice1000]

Yes but only before desugar.

Could you give me a case in concrete syntax? I couldn't think of any. I've added a breakpoint at the corresponding place before desugar, but all cases just don't enter there.

Write Type 0 and you get an AppExpr right after parsing

[tonfeiz]

Sorry, I didn't describe the situation correctly.

The correct question is: Is it possible for an AppExpr's function to be a instance of RawUnivExpr, and the AppExpr is an application operator's lhs?

[re-xyr]

Write Type 0 and you get an AppExpr right after parsing

I forgot why we can't just make the parse rule be 'Type' NUMBER??

[ice1000]

Write Type 0 and you get an AppExpr right after parsing

I forgot why we can't just make the parse rule be 'Type' NUMBER??

That will be more code IMO. You have to deal with Type ID anyway

[ice1000]

Sorry, I didn't describe the situation correctly.

The correct question is: Is it possible for an AppExpr's function to be a instance of RawUnivExpr, and the AppExpr is an application operator's lhs?

I think this is a type error, but why?

[imkiva]

Sorry, I didn't describe the situation correctly.

The correct question is: Is it possible for an AppExpr's function to be a instance of RawUnivExpr, and the AppExpr is an application operator's lhs?

I think this is a type error, but why?

BinOpParser always produces binary AppExpr. So the outdated syntax 'Type u v' becomes 'App[App[RawUniv, u], v]' by default.

That's why there exists instanceof check in BinOpParser#makeBinOp to avoid this case and make level desugarer work. they could be safely removed now I think.

[ice1000]

That's why there exists instanceof check in BinOpParser#makeBinOp to avoid this case and make level desugarer work. they could be safely removed now I think.

Geez

[tonfeiz]

OK, understand it now. Thanks a lot.