Zulip Chat Archive

Stream: general

Topic: dot notation confusion


Kevin Buzzard (Feb 01 2019 at 09:46):

I have always been confused about dot notation. I don't use it as much as other people, because I don't understand it as well as other people. I've read Patrick's notes on this and TPIL but I think there's more to it.

I understand that if I make a new structure structure point (α : Type) := (x : α) (y : α) then for p : point I can use p.x instead of point.x p. I also understand that if we make more functions in the structure's namespace like point.blah (which for simplicity takes as input one point and possibly some other stuff) then p.blah is shorthand for point.blah p (or perhaps point.blah _ _ p if the point happens not to be the first thing that point.blah eats).

What threw me yesterday when working on the perfectoid project was that my proof that if neg was a continuous function on a topological ring then it was also a continuous function on a subring looked like this:

continuous_neg := continuous_subtype_mk _ $
                    continuous.comp
                      continuous_subtype_val $
                      topological_ring.continuous_neg A

and then Patrick took one look at this code and pointed out that this could be written

continuous_neg := continuous_subtype_mk _ $
                      continuous_subtype_val.comp $
                      topological_ring.continuous_neg A

It took me a while to realise that he wasn't talking about some fancy new function in the topology directory in mathlib but was in fact advocating the use of the dot notation. It would never have occurred to me to try to use dot notation here. In the examples above, which I understand, we have p : point, i.e. a term whose type is a structure and then a function in the corresponding namespace. But here continuous_subtype_val has type ∀ {α : Type u} [_inst_1 : topological_space α] {p : α → Prop}, continuous subtype.val which is definitely not a structure, and even if I remove all the implicit arguments then it becomes continuous subtype.val which is also not a structure, and even if I look at the head function then it's continuous which is also not a structure. But Patrick's code does work. I am fast coming to the conclusion that my understanding of dot notation is nowhere near complete.

Investigating further, I find that #check continuous_subtype_val.comp works, even though there appears to be no function continuous_subtype_val.comp. Moreover, this seems to have nothing to do with structures at all, because continuous is not a structure, it's just a plain old definition. What seems to be going on in this situation is that if p has type {implicit stuff} [more implicit stuff] foo x and foo happens coincidentally to be both a function and a namespace (which is something that continuous seems to be, for some reason I don't understand) then p.blah is defined to mean foo.blah p . In some sense I am surprised that this is ever useful beyond the case I understand, i.e. structures. If continuous_subtype_val had happened to just take one explicit argument, which in a parallel universe it could have done, I am assuming that this trick would stop working.

So is the philosophy something like "if foo is any old function, and if I'm defining a function f : foo x -> y, then I might want to consider calling the function foo.fbecause then I can write f.p if p : foo x? What I don't get is that if I had just called it f then I could have written f p which is just as many characters as f.p anyway.

I guess I can understand that if foo is a structure and I wanted to define a neg on foo x then I would instinctively called it foo.neg. But I wouldn't do this for continuous. Is this evidence that continuous should be a structure? Are our naming conventions treating it like it is one?

Confused in London.

Sebastian Ullrich (Feb 01 2019 at 10:08):

To spell it out, the full semantics of dot notation is, roughly, "if e is a term of type t ..., and there is a function t.f, then e.f ... is syntax sugar for t.f ... e ..., where e has been inserted as the argument for the first parameter of type t ...". e being a variable of a structure s and s.f being a projection is just a special case of that.

Sebastian Ullrich (Feb 01 2019 at 10:13):

Note that the term continuous_subtype_val has type continuous subtyp.val. The type you gave is the type of @continuous_subtype_val! So dot notation doesn't think "oh, this is a function", but "oh, this is a continuous"

Mario Carneiro (Feb 01 2019 at 10:13):

Originally, continuous.comp was called continuous_comp. It was renamed because it is "eligible" for projection notation like this

Mario Carneiro (Feb 01 2019 at 10:14):

You can't just call it comp because that overlaps with a million other things

Mario Carneiro (Feb 01 2019 at 10:16):

There is a danger in using non-structures with projection notation, because regular defs can be unfolded, and once they are unfolded they no longer have that name anymore (continuous in this case) so the projections won't find the namespace. In practice I haven't had too much issue with this unless you are solving some weird unification problem

Mario Carneiro (Feb 01 2019 at 10:17):

and in that case it's not too bad to just say continuous.comp ...

Kevin Buzzard (Feb 01 2019 at 10:21):

continuous.comp was "eligible" because it took continuous f as an input. It seems to me that the real coincidence is that continuous_subtype_val has type continuous ... and every other input can be inferred.

Mario Carneiro (Feb 01 2019 at 10:21):

If continuous_subtype_val had happened to just take one explicit argument, which in a parallel universe it could have done, I am assuming that this trick would stop working.

No, it would be written (continuous_subtype_val _).comp in that case

Mario Carneiro (Feb 01 2019 at 10:22):

it's not a coincidence that continuous_subtype_val returns a continuous; that's the whole point of the function, we are proving things are continuous. Possibly some hypotheses would be necessary but those can be dealt with as above

Kevin Buzzard (Feb 01 2019 at 10:23):

Ok I think I now understand. Thanks to Sebastian and Mario as ever. Would I be right in thinking that the complete list of functions that aren't structures but which have an associated namespace is quite small? continuous being one. Or does this happen everywhere and I've just not noticed it yet (and this is the reason I underuse dot notation)?

Mario Carneiro (Feb 01 2019 at 10:23):

You can basically always use continuous.comp with projection notation, because the first argument will be a continuous

Kevin Buzzard (Feb 01 2019 at 10:24):

Oh!

Kevin Buzzard (Feb 01 2019 at 10:24):

So in fact it's utterly commonplace and this is why Patrick spotted it so quickly

Kevin Buzzard (Feb 01 2019 at 10:25):

You basically never write continuous.comp at all!

Kevin Buzzard (Feb 01 2019 at 10:25):

It does hamper readability though

Mario Carneiro (Feb 01 2019 at 10:25):

it's a pretty simple and common trick, enough that I can't say how many times it's been used in mathlib. If a theorem about foo things has an argument of type foo x, you should consider calling it foo.bar instead of foo_bar

Kevin Buzzard (Feb 01 2019 at 10:26):

And now I understand why

Mario Carneiro (Feb 01 2019 at 10:26):

Personally I like having .comp as a sort of infix operator. If you turn your head and squint it looks like the

Kevin Buzzard (Feb 01 2019 at 10:26):

It's to maximise obfuscation :-)

Kenny Lau (Feb 01 2019 at 10:27):

I can read it perfectly without any problem

Kevin Buzzard (Feb 01 2019 at 10:27):

You should have called it continuous.o

Kevin Buzzard (Feb 01 2019 at 10:28):

Wait

Mario Carneiro (Feb 01 2019 at 10:28):

you are about to point out the order is wrong, I'm sure

Kevin Buzzard (Feb 01 2019 at 10:28):

its inputs are in the...

Kevin Buzzard (Feb 01 2019 at 10:28):

Yeah :-)

Mario Carneiro (Feb 01 2019 at 10:29):

not sure there is any big reason for that

Mario Carneiro (Feb 01 2019 at 10:30):

also not sure I care about it

Mario Carneiro (Feb 01 2019 at 10:31):

I will let Scott have his hobby horse

Johan Commelin (Feb 01 2019 at 10:45):

I guess we can still define continuous.o with arguments in the right order...

Kevin Buzzard (Feb 04 2019 at 14:31):

it's a pretty simple and common trick, enough that I can't say how many times it's been used in mathlib. If a theorem about foo things has an argument of type foo x, you should consider calling it foo.bar instead of foo_bar

The crucial point is that the function has as _input_ things of type foo, like continuous.comp, rather than just outputting things of type foo like continuous_subtype_val. Dots for the input, underscores for the output.

Sebastien Gouezel (Feb 04 2019 at 15:26):

Cute example in #PR657

theorem isometry_on.uniform_embedding (h : isometry_on f univ) : uniform_embedding f :=
(emetric_isometry_on_iff_isometry_on.2 h).uniform_embedding

lemma isometry_on.continuous
  (hf : isometry_on f univ) : continuous f :=
hf.uniform_embedding.embedding.continuous

Kevin Buzzard (Feb 04 2019 at 15:33):

So both the theorem and the lemma are in the isometry_on namespace and have an input of type isometry_on ..., so dot notation is appropriate.

I guess what happens in practice is that users of a particular theory instinctively know which functions this works for, and use it. I guess we can also infer from this example that there are theorems uniform_embedding.embedding : uniform_embedding f -> embedding f and embedding.continuous : embedding f -> continuous f. I think understand this properly now; thanks for posting the example, it is very neat. The example shows that the concept seems to concatenate in good cases (when there's only one input, unlike continuous.comp which takes two).

Mario Carneiro (Feb 04 2019 at 15:38):

well, like I said, it still works in the n-ary case, you just have to put parentheses

Mario Carneiro (Feb 04 2019 at 15:39):

but this kind of "dot-chaining" is exactly what projections are great at. It's intentionally similar to method chaining in OO languages like Java

Kevin Buzzard (Feb 04 2019 at 17:05):

What is a "projection"?

Mario Carneiro (Feb 04 2019 at 17:11):

f.x is called projection notation, foo.x is a projection on f

Mario Carneiro (Feb 04 2019 at 17:11):

in a structure, the fields are also called projections - the origin is the first and second projections of a pair


Last updated: Dec 20 2023 at 11:08 UTC