dot notation reference

Stream: general

[Patrick Massot]

Is there any paper one can cite to explain dot notation to readers unfamiliar with Lean?

[Patrick Massot]

I mean this in the context of an academic paper, not a tutorial.

[Sebastian Ullrich]

I guess I am to blame for the notation, but I don't know any papers explaining it

[Patrick Massot]

Not even vaguely?

[Yaël Dillies]

Bhavik and I explain it quickly in our SRL paper.

[Patrick Massot]

Thanks, but it's indeed very quick. Citing that instead of including the sentence would be a bit weird.

[Sebastian Ullrich]

This is the only relevant mention of "dot" in the official Lean publications image.png https://leanprover.github.io/papers/do.pdf

[Patrick Massot]

Citing a Lean 4 paper would also be weird. I guess it's too late to include this in a Lean 3 paper.

[Patrick Massot]

But it reminds me that I think it's explained in Rob's Hensel lemma paper

[Sebastian Ullrich]

There is also https://leanprover.github.io/lean4/doc/struct.html?highlight=dot#structures, which is a bit better than a tutorial, but still Lean 4

[Patrick Massot]

Yes, Rob's paper has a full paragraph about it!

[Eric Wieser]

I think @Kyle Miller has made dot notation more intelligent since that paper

[Kyle Miller]

Patrick Massot said:

Citing a Lean 4 paper would also be weird. I guess it's too late to include this in a Lean 3 paper.

The extended field notation for Lean 3 is now (mostly) based on Lean 4's, so maybe this is not too weird?

The "mostly" is because it is still slightly different in the way it handles implicit arguments, but it should eventually converge to Lean 4 here.

[Kyle Miller]

I'm not completely sure what the official name of dot notation is. It seems to be called (generalized/extended) dot/field notation depending where you look.

[Tomas Skrivan]

I would call it uniform call syntax

[Mario Carneiro]

uniform call syntax is @f ...

[Mario Carneiro]

generalized field notation sounds the most correct

[Tomas Skrivan]

The wiki example on uniform function call syntax in D shows:

    // all the following are correct and equivalent
    int b = first(a);
    int c = a.first();
    int d = a.first;

To me that looks like the dot notation

[Mario Carneiro]

based on the description, it's not type dependent. If by "uniform function call syntax" is meant "a uniform syntax for calling functions" that's @f

[Tomas Skrivan]

It might be that Lean uses the term uniform call syntax for @f .... But for me, coming from C++/D, uniform function call syntax is than f(x) is the same as x.f() or x.f.

[Tomas Skrivan]

The point is that it makes uniform syntax between functions and object's methods.

[Anne Baanen]

Kyle Miller said:

I'm not completely sure what the official name of dot notation is. It seems to be called (generalized/extended) dot/field notation depending where you look.

I've seen some names like that in the C++ source code. But there are some more unusual names in the code that we don't use in practice so I vote for "dot notation".

[Kyle Miller]

@Tomas Skrivan I see the similarity to UFCS, but in Lean f x and x.f usually don't mean the same thing. There are mildly complicated rules for which namespaces are used to resolve f using the type of x, and this information is also used to determine which argument x will be used for.

[Kyle Miller]

@Anne Baanen I think the error messages in both Lean 3 and 4 mention field notation. Maybe it would be good to go through the error messages sometime and make sure it's all using consistent terminology...