namespace field notation

Stream: general

[Sean Leather]

Before I disappeared for a month to handle a visiting-family exception, I was experimenting with using more “namespace field notation.” That is, instead of using list.map f l, I would use l.map f. I like the conciseness gained by removing the namespace list.

However, I had started to sour on it then, and, after returning to my code and trying to refresh my working cache, I find that I no longer like it. Since the field notation differs from the definition notation and from the pretty-printed lean output in errors, going back and forth between notations requires repeatedly reorienting on the positions of arguments. (While list.map is a nice example for advocating use of the notation, when a definition has more than 2 parameters or typically needs bracketed arguments, the notation does not help.)

If we could write definitions using namespace field notation and if the notation were used by lean to pretty-print, I believe the benefit would become clear. Otherwise, I don't think I'll be using it much.

What do you think?

[Mario Carneiro]

It doesn't really make sense to use projection notation in definitions, since it requires that the variable already be declared and have known type. You certainly won't get this before you've even stated the theorem name

[Mario Carneiro]

projection in pretty printing would be nice, but I don't know how hard it is

[Mario Carneiro]

also it's one more thing that can break in inconvenient ways if the pretty printed expression doesn't quite typecheck due to too many implicit things

[Sean Leather]

It doesn't really make sense to use projection notation in definitions, since it requires that the variable already be declared and have known type. You certainly won't get this before you've even stated the theorem name

Perhaps there could be some alternative notation-like operation to allow being explicit about the projection instead of using the built-in rule that now exists.

[Mario Carneiro]

I don't follow

[Sean Leather]

In other words, perhaps the implicit projection rule could be replaced with an explicit projection declaration.

[Sean Leather]

It would (a) be more flexible and (b) add documentation of the projection notation for a particular definition.

[Sean Leather]

also it's one more thing that can break in inconvenient ways if the pretty printed expression doesn't quite typecheck due to too many implicit things

@Mario Carneiro What is “it” referring to here?

[Mario Carneiro]

What kind of flexibility are you thinking? Also I don't relish the idea of adding thousands of annotations for what is essentially redundant information, and having to keep it up to date. The current projection algorithm is easy to learn and completely uniform

[Mario Carneiro]

"it" is pp projection notation. The elaborator has less to go on with projection notation, so if it can't solve for the type of a variable immediately projections just halt the whole type inference process. I'm saying that this situation may occur with pp expressions, assuming you aren't using some pp.all type option

[Sean Leather]

What kind of flexibility are you thinking?

Declaring which parameter should be used for projection is the main one that comes to mind. I recall running into an issue where projection didn't work, but I think it would if I could explicitly declare how to do it. (I don't remember the exact issue, unfortunately.)

[Sean Leather]

"it" is pp projection notation. The elaborator has less to go on with projection notation, so if it can't solve for the type of a variable immediately projections just halt the whole type inference process. I'm saying that this situation may occur with pp expressions, assuming you aren't using some pp.all type option

Yes, I could see how that could be a problem if pretty-printing involves inferring the projection notation. But, given the above idea of an explicit projection notation, it would not need to infer anything.

[Mario Carneiro]

Projection was less powerful early in its history, because you could only project with the first explicit argument. That restriction has since been dropped, so make sure that isn't the issue you are thinking of

[Mario Carneiro]

it would still need to infer stuff even with projection annotations, since x.bar could mean either list.bar x if x : list a or multiset.bar x if x : multiset a, or even x.bar if x is a namespace

[Sean Leather]

Projection was less powerful early in its history, because you could only project with the first explicit argument. That restriction has since been dropped, so make sure that isn't the issue you are thinking of

No, I don't think that's relevant. My issue is with going back and forth between two different notations.

[Mario Carneiro]

That just sounds like a pp problem

[Mario Carneiro]

I just always use projections in the code, and replace anything I copy after pp with projections

[Sean Leather]

That just sounds like a pp problem

A bit too simplistic of a view, I think. I'm pretty sure we don't want to pretty-print everything in projection notation.

[Mario Carneiro]

so there's no back and forth unless I'm doing a lot of copy paste from pp anyway, which produces non-human output for several reasons, that's not the only thing I want to change in general

[Sean Leather]

Here's a simple example:

1. Projection:

t.open ts = subst_list xs ts (t.open (xs.map varf))

2. No projection:

typ.open ts t = subst_list xs ts (typ.open (list.map varf xs) t)

The first option is less verbose, but I only ever see it in code I write. The second is what the pretty-printer shows.

[Sean Leather]

Here are some questions and thoughts prompted by the discussion above:

Why shouldn't I be able to tell Lean to pretty-print the projection notation as in 1? I can already tell it to use some other notation or infix. I don't see how the inference problem is different.

Once I am allowed to say I want definition d to be pretty-printed with projection notation, why shouldn't I be able to declare which parameter is the projection target? Consequently, the declaration to “use projection notation” becomes another notation or infix but specialized to projection.

[Mario Carneiro]

The first option is less verbose, but I only ever see it in code I write. The second is what the pretty-printer shows.
Why shouldn't I be able to tell Lean to pretty-print the projection notation as in 1?

Like I said, a pp problem. There's nothing wrong with this in principle, except this is a core lean issue so it's not going to happen until lean 4, and that only if Leo thinks of this himself

[Mario Carneiro]

Once I am allowed to say I want definition d to be pretty-printed with projection notation, why shouldn't I be able to declare which parameter is the projection target? Consequently, the declaration to “use projection notation” becomes another notation or infix but specialized to projection.

There isn't really any choice in what argument can be the projection argument, except in definitions which, say, take in more than one list parameter. If you think the second argument is a better projection target than the first, then I suggest you reorder the parameters

[Sean Leather]

Like I said, a pp problem. There's nothing wrong with this in principle, except this is a core lean issue so it's not going to happen until lean 4, and that only if Leo thinks of this himself

Right, but I don't think that means that I can't bring it up here and discuss it, does it? :wink:

[Sean Leather]

There isn't really any choice in what argument can be the projection argument, except in definitions which, say, take in more than one list parameter. If you think the second argument is a better projection target than the first, then I suggest you reorder the parameters

I disagree. You could expand projection to include things outside the namespace of the definition.

[Mario Carneiro]

No, that doesn't really work with the way projections are resolved. It gets the type of the argument, and uses that as a namespace to look up projections. If you want a projection to work on a certain argument, make sure the namespace lines up

[Sean Leather]

But it could work that way with explicit projection notation. :simple_smile:

[Mario Carneiro]

It obviously has to key on something, since otherwise it has to go through all the definitions, and the only available information at that point is the type of the variable

[Mario Carneiro]

I don't see the difference between an explicit projection notation and naming the definition appropriately so the automatic method picks out the desired argument. Do you have a concrete example where you think it would be difficult to do otherwise?

[Sean Leather]

I did at one point. It had to do with a list parameter, I think, but I don't remember it now.

[Sean Leather]

Generally, though, suppose you have a definition that is not for general lists but has a list parameter and you want projection on an list argument, you would need to put the definition in the list namespace. Slightly more concretely, suppose you have something like def n.d : list n → Prop. So, to get projection notation, you would need to rename n.d to list.d. That seems wrong.

[Patrick Massot]

Sean, since you seem to care about this projection notation, have you seen https://github.com/leanprover/mathlib/pull/96 ? Don't hesitate to propose any further clarification or new tricks in the relevant section

[Sean Leather]

@Patrick Massot I saw it. It was part of the reason, other than that I've been thinking about it for a while, that I brought up the subject.

I think the only change I would make is that “first explicit argument” is not correct. As @Mario Carneiro said, the argument (or what I prefer to call “parameter”) need not be explicit. In other words, you could have this:

def sum (α : Type) [has_add α] : point α → α := λ p, p.x + p.y
#reduce p.sum α

[Patrick Massot]

What would you write then?

[Sebastian Ullrich]

@Sean Leather

So, to get projection notation, you would need to rename n.d to list.d. That seems wrong.

But this is how it works in OOP languages the notation was borrowed from, if you interpret classes as introducing namespaces. How would we know to look in the namespace n for d?

[Sean Leather]

@Patrick Massot The simplest change would be to remove “explicit” and to give an example in which the argument is not explicit. You could use the one above, though you should check it first to make sure I didn't make a mistake.

[Sebastian Ullrich]

@Gabriel Ebner Btw, have we ever discussed a notation like xs.(map f).(filter g) to solve the chaining issue? I might have to experiment with a macro for that in Lean 4 :laughing: .

[Patrick Massot]

Actually I don't know how to call that kind of argument that lingers right of the colon. My explicit was rather referring to (x : X) vs {x : X}.

[Patrick Massot]

But this is how it works in OOP languages the notation was borrowed from, if you interpret classes as introducing namespaces. How would we know to look in the namespace n for d?

At last, someone confess FP is trying to mimic OOP greatness

[Sean Leather]

@Patrick Massot Ah, okay. I may have misinterpreted it then. :simple_smile:

[Sean Leather]

@Sebastian Ullrich:

But this is how it works in OOP languages the notation was borrowed from, if you interpret classes as introducing namespaces. How would we know to look in the namespace n for d?

I don't follow. In OOP, you wouldn't find a method with the type list n in a list class.

[Patrick Massot]

But I'm interested in explaining how far that projection notation extends. So I'll definitely try that def sum (α : Type) [has_add α] : point α → α := λ p, p.x + p.y

[Patrick Massot]

But right now I'm typing notes on the Nash-Kuiper embedding theorem, not playing with Lean or chatting on Zulip

[Sebastian Ullrich]

@Sean Leather In Java, x.f will look up f in the class of x and pass x as the this argument. Basically what happens in Lean.

[Sebastian Ullrich]

The whole point of field notation is to hide the namespace. I don't see the benefit of p.sum over sum p.

[Sean Leather]

In Java, x.f will look up f in the class of x and pass x as the this argument. Basically what happens in Lean.

Right. It also extends the lookup to superclasses. But still, that's rather limiting, I think.

[Sebastian Ullrich]

It also extends the lookup to superclasses.

As we do

[Sean Leather]

What's a superclass in Lean?

[Sebastian Ullrich]

The thing after extends :)

[Sean Leather]

Are you talking about class or namespace? I wasn't aware a namespace could extends something.

[Gabriel Ebner]

@Gabriel Ebner Btw, have we ever discussed a notation like xs.(map f).(filter g) to solve the chaining issue? I might have to experiment with a macro for that in Lean 4 :laughing: .

No I don't think so. I think the only proposal that aimed to simplify chaining was my Agda-like xs .map f .filter g, which many people apparently found abhorrent.

[Sebastian Ullrich]

@Sean Leather Ah sorry, I was thinking of the basic field notation, which will pick up fields from super structures as well. But it doesn't work with functions in the namespace... yet