Syntax for partially applied functions

[valis]

Implement a notation for partially functions such as f(a,-,c). I suggest __ because - and _ are already taken.

The lambda should be inserted only in specific positions such as the argument of an application (but not in infix operator).

f a __ c == (\lam x => f a x c)
(\lam c => f __ c) == (\lam c x => f x c)
pmap __.1 s == pmap (\lam t => t.1) s
__ a == (\lam f => f a)
x + __.2 == (\lam t => x + t.2)
field {__} + y == (\lam s => field {s} + y)
a * __ + b * c == (\lam x => a * x + b * c)
f __ + 3 == (\lam x => f x + 3)
(__.1, __.2) == (\lam t => t.1, \lam t => t.2)
(\case f __ \with { }) == (\lam x => \case f x \with { })

If __ occurs more than once in an expression, this can be interpreted either as a lambda with two parameters or as a lambda with one parameter which is used twice. For example, __ * a + __ * b could be interpreted as either \lam x y => x * a + y * b or \lam x => x * a + x * b. The first interpretation looks more natural to me.

[ice1000]

__ * a + __ * b may also be (\lam x => x * a) + (\lam x => x * b), no?

[ice1000]

If it shall desugar app exprs recursively, how about parentheses? Say, f (a __ b), should it become \lam x => f (a x b) or f (\lam x => a x b)?

[valis]

__ * a + __ * b may also be (\lam x => x * a) + (\lam x => x * b), no?

It could be, but it shouldn't be.

[valis]

If it shall desugar app exprs recursively, how about parentheses? Say, f (a __ b), should it become \lam x => f (a x b) or f (\lam x => a x b)?

Parenthesis is not part of the AST. In you example, it's an argument of an application. The original messages mentions this:

The lambda should be inserted only in specific positions such as the argument of an application (but not in infix operator).

[ice1000]

So, IIUC, a * (__ + b) should be \lam x => a * (x + b), right?

[valis]

Basically, it should be inserted immediately except for a few special cases. I list a few of them in my original message (there might be more though). So, if it does not make sense to insert lambda in some place, it should be inserted higher. For example, this happens in \case expressions. It also happens in \Pi and \Sigma types, which I did not mention.

Binops is a special case. It certainly possible to have a lambda under binop, but it rarely happens in practice and it is more natural to desugar __ * a + b into \lam x => x * a + b than (\lam x => x * a) + b.

[valis]

So, IIUC, a * (__ + b) should be \lam x => a * (x + b), right?

Yes

[ice1000]

1 + \case __ \with {} is translated to \lam i => i + \case i \with {}

[ice1000]

Shall be fixed by #199?