name of "syntax sugar of simple function"

Stream: general

[Asei Inoue]

https://lean-lang.org/lean4/doc/lean3changes.html#sugar-for-simple-functions

-- this notation.
-- syntax sugar of lambda expression
def sample : Nat → Nat := (· + 1)

what should we call this function of Lean4? I have never seen this feature called by its short name.
"sugar for simple function" is the official name?

[Asei Inoue]

I call this function "Emoji-like lambda expression" usually...

[Edward van de Meent]

my mind jumped to dot-notation, but that's a different thing...

[Asei Inoue]

(deleted)

[Asei Inoue]

these are emoji-like!

def sample : Nat → Nat → Nat := (· + ·) -- cute

def sample1 : Nat → Nat → Nat := (· - ·) -- cute

def sample2 : Nat → Nat → Nat := (· ^ ·) -- cute

[Asei Inoue]

(deleted)

[Asei Inoue]

(deleted)

[Mario Carneiro]

In the code it's just referred to as the cdot parser. I don't think it has any official name

[Mario Carneiro]

docs#Lean.Parser.Term.cdot uses the name "implicit lambda abstraction", although this sounds too similar to fun {x y} => _ implicit lambdas

[Kyle Miller]

In error messages, it's called "· notation" (cdot notation). I sometimes call them "anonymous lambdas" but I don't like that name. "Cdot function" seems reasonable.

[Kyle Miller]

I know there are other languages with a similar feature, but I can't remember what they are -- what do they call it?

[Mario Carneiro]

Haskell has (+) which I think are called "sections"

[Mario Carneiro]

named after the categorical notion IIUC

[Kyle Miller]

There are languages that have this style where placeholders are considered in left-to-right order, like perhaps (# + # * #) or (_ + _ * _), though they might require a sigil to indicate where the lambda is supposed to be.

[Mario Carneiro]

oh yes scala has something like that

[Asei Inoue]

You know that _ is sometimes called hole. The cdot in this notation shall simply be referred to as cdot?

[Mario Carneiro]

https://www.geeksforgeeks.org/placeholder-syntax-in-scala/ suggests it's called "placeholder syntax", although this terminology sounds specific to the usage of underscore (which has many other meanings in scala as well)

[Mario Carneiro]

in lean there are basically two usages of cdot, this one and the one in tactic syntax for focusing goals

[Mario Carneiro]

and in both cases you can use . in place of · (so it's not necessarily a cdot "central dot")

[Kyle Miller]

oh yes scala has something like that

Yeah, Scala must be one of the languages I've seen this in.

I found that PureScript has (_ * 2), (2 * _), (_ * _) for sections. I'm not sure how much this generalizes to other expressions, but it does work for records as well.

[Kyle Miller]

so it's not necessarily a cdot "central dot"

Too bad "dot function" could also mean things like .cons, etc.

[Asei Inoue]

It makes sense to call the cdot in this notation a "placeholder dot" (similar to "focusing dot").

[Mario Carneiro]

I think "placeholder" is more commonly used to refer to _

[Mario Carneiro]

or ?_

[Asei Inoue]

I think "placeholder" is more commonly used to refer to _

I see ... Then perhaps cdot in this notation deserves a completely new name?

[Mario Carneiro]

Kyle Miller said:

so it's not necessarily a cdot "central dot"

Too bad "dot function" could also mean things like .cons, etc.

yes, this syntactic construction is very much lacking unique syntax. The things that make it distinctive are the use of "parentheses" and "dot" and both of those are used in other places

[Mario Carneiro]

so it's pretty hard to name it just after these components

[Asei Inoue]

What about 'eye'?

[Kyle Miller]

Yeah, _ is a placeholder, but ?_ is a "synthetic hole" (according to the docstrings). In lean4#3494 I was trying to add the terminology "synthetic placeholder" for ?_ to parallel _ better. (While also adding notation for delayed assignment metavariables.)

There's (eventually) going to be an official glossary of all Lean concepts with their recommended names.

[Asei Inoue]

summary

"cdot" → It is not necessarily a cdot, can be a period.
"placeholder" → conflicts with _
"dot" → overused

[Mario Carneiro]

well the trouble is that we aren't just trying to name the character · / . itself, I think "cdot" is fine for that, but rather the whole construction involving · and ( ... ) in some combination that produces a lambda

[Mario Carneiro]

maybe we should just use the "section" name

[Asei Inoue]

Since there are no variable names, we could say that it is an "anonymous lambda".

[Mario Carneiro]

that's a possibility, although lambdas are already "anonymous functions" for a different notion of anonymous

[Asei Inoue]

"dot lambda"... "hidden lambda"...

[Asei Inoue]

"arrowless lambda"...

[Asei Inoue]

"operation dot"...

[Asei Inoue]

I like "arrowless lambda" among the ones I just mentioned.

[Yaël Dillies]

"placeholder lambda"?

[Trebor Huang]

lambdaless lambda

[Joachim Breitner]

Implicit parameters.
Pattern function.
Partial expression.
Nameless binders.
No-fun-function.
Dot product.
Hidden variables.
Mutlivalued expression.
Template.

[Asei Inoue]

I guess we need voting..?

[Asei Inoue]

I like "Pattern function" and "lambdaless lambda"....