dot notation confusion

Stream: general

[Kevin Buzzard]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

Oh!

[Kevin Buzzard]

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

[Kevin Buzzard]

You basically never write continuous.comp at all!

[Kevin Buzzard]

It does hamper readability though

[Mario Carneiro]

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]

And now I understand why

[Mario Carneiro]

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

[Kevin Buzzard]

It's to maximise obfuscation :-)

[Kenny Lau]

I can read it perfectly without any problem

[Kevin Buzzard]

You should have called it continuous.o

[Kevin Buzzard]

Wait

[Mario Carneiro]

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

[Kevin Buzzard]

its inputs are in the...

[Kevin Buzzard]

Yeah :-)

[Mario Carneiro]

not sure there is any big reason for that

[Mario Carneiro]

also not sure I care about it

[Mario Carneiro]

I will let Scott have his hobby horse

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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]

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

[Mario Carneiro]

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]

What is a "projection"?

[Mario Carneiro]

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

[Mario Carneiro]

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