Default Notation Scope Confusion

Stream: lean4

[Mac]

Why is the default Lean scope of notation within a namespace global rather than scoped? It seems like that later would be more natural. If you want global notation, it would make sense to define it outside of a namespace (or, if you really want to still do it inside you could potentially clarify your intention by adding a global attribute). However, generally if you are defining notation within a namespace, you probably are doing so because you want it scoped, and prepending every notation/syntax declaration with scoped is annoying.

[Mac]

Bumping this because I am still really curious about the reasoning behind this.

[Sebastian Ullrich]

Mac said:

However, generally if you are defining notation within a namespace, you probably are doing so because you want it scoped

I would tend to agree with this. However, we should be careful about consistency with other commands. We learned the hard way with Lean 2 that most commands/attributes, such as instance, should not be scoped by default. The experience was painful enough that the feature was removed entirely from Lean 3.

[Mac]

Sebastian Ullrich said:

I would tend to agree with this. However, we should be careful about consistency with other commands. We learned the hard way with Lean 2 that most commands/attributes, such as instance, should not be scoped by default.

I can sympathize with the need to be careful, though I do think this is case where scoped should be the default. I would also note instance is very different beast. Outside of some very few exceptions (such as a Monad instances), if a class could have an instance, it should have the given instance, making adding an instance for an object only a positive, and not something you would want to restrict. However, fundamentally altering the syntax of the language is an entirely different matter, which one can easily want restricted.

Also, more generally many other attributes in Lean 3 were definitional. For example, class and pattern. It makes no sense for these attributes to be separated from their target by a scope as they are key parts of the definition. Syntax, however, is its own kind of definition, and just like defs are scoped by default within their enclosing namespace, it makes sense for syntax to be.

[Brandon Brown]

Is this related to the problem I'm having overriding the default "+" notation?

-- defined my own list.append function
local infixl:65 " + " => list.append
#reduce [1,2] + [3,4]

--- Error:
-- ambiguous, possible interpretations
--  [1, 2] + [3, 4]
 -- [1, 2] + [3, 4]

[Sebastian Ullrich]

You can increase its priority:

local infixl:65 (priority := high) " + " => List.append

Perhaps local parsers should have a higher default priority. Though should scoped parsers as well then? :shrug:

[Mac]

Brandon Brown said:

Is this related to the problem I'm having overriding the default "+" notation?

Sort of? The problem here is that default "+" notation is also present so it clashes with your definition, making it ambiguous. If it was it was scoped to a namespace, you could choose whether or not you wished to enable it, but because its not, you can't.

However, there is a way to solve your issue, just given your notation a higher priority than the default notation:

- defined my own list.append function
local infixl:65 (priority := high) " + " => list.append
#reduce [1,2] + [3,4]

[Sebastian Ullrich]

Hah, high is definitely nicer

[Brandon Brown]

Thanks!

[Mac]

Sebastian Ullrich said:

Hah, high is definitely nicer

I also like default + default, as it keeps on the same tier (i.e., built-in notation with high priority will still override it).

[Gabriel Ebner]

Sebastian Ullrich said:

The experience was painful enough that the feature was removed entirely from Lean 3.

But the feature was so useful that it was subsequently reintroduced in mathlib under the name of "locales": https://leanprover-community.github.io/mathlib_docs/commands.html#localized%20notation

[Sebastian Ullrich]

Well yeah, as well as in Lean 4 :)

[Mac]

Gabriel Ebner said:

Sebastian Ullrich said:

The experience was painful enough that the feature was removed entirely from Lean 3.

But the feature was so useful that it was subsequently reintroduced in mathlib under the name of "locales": https://leanprover-community.github.io/mathlib_docs/commands.html#localized%20notation

I was under the impression that Sebastian Ullrich was referring to the experience with localized instances and the like.

[Gabriel Ebner]

This works just fine and is used in mathlib (but I think it's only a good idea for Prop-valued classes):

localized "instance ..." in classical

[Mac]

Yes, but that fits with his point: that things like that shouldn't generally be scoped by default.

[Sebastian Ullrich]

In any case, I hope we can agree that Lean 4 can natively (i.e. less hackishly) express (sensible) uses of localized. The only question is the matter of defaults.

[Mac]

Sebastian Ullrich said:

Perhaps local parsers should have a higher default priority. Though should scoped parsers as well then? :shrug:

I think differing default priorities would be confusing. Though it might make sense for local/scoped parsers to preferred over global parsers when disambiguating notation (I would have it go local > scoped > global). -- It would also help if Init was in its own namespace that could be open and closed as desired. ;)

[Mac]

Sebastian Ullrich said:

In any case, I hope we can agree that Lean 4 can natively express (sensible) uses of localized. The only question is the matter of defaults.

Well, my position is thus. Notation (i.e. parsers and macros) should be scoped by default. They should only effect syntax if their related def is in scope. Things like class should be global by default. They are permeant properties of their related defs and thus should not generally be able to be turned on and off by changes in scope (in fact, I am not sure if they should ever be). The instance attribute should similarly be global by default, as that is generally the desire (but unlike things like class, it definitely does have cases where being local/scoped is useful).

[Mac]

Brandon Brown said:

Is this related to the problem I'm having overriding the default "+" notation?

-- defined my own list.append function
local infixl:65 " + " => list.append
#reduce [1,2] + [3,4]

Also, there is one thing that I forgot to mention earlier that I am curious about. List concatenation is generally denoted with the ++ operator as opposed to the + operator. In fact, for this reason, there is actually no Add instance for the built-in List. So, technically, if you wanted to use + for a list you could just add an Add instance for it instead of defining new notation. All in all, I'm just a little curious as to why you decided to use + to denote concatenation.

[Sebastian Ullrich]

Yes, the order of priority should probably be

1. define a new typeclass instance for an existing notation (if available)
2. define a new macro rule for an existing notation (overrides the previous semantics)
3. define a new overlapping notation (more work for both the parser and elaborator, unless you want type-based disambiguation)

[Mac]

Sebastian Ullrich said:

Yes, the order of priority should probably be

1. define a new typeclass instance for an existing notation (if available)
2. define a new macro rule for an existing notation (overrides the previous semantics)
3. define a new overlapping notation (more work for both the parser and elaborator, unless you want type-based disambiguation)

How do you do number 2 with notation that is unnamed (like most of the built-in notation is)? I know that there are the auto-generated names, but using those feels very hackish (as I wouldn't be surprised if the generated names changed in the future). I guess another way to phrase this is: should you do number 2 with auto-named notation?

[Mac]

Also, wouldn't number 2 require writing the same rule twice for two different kinds for notation that has both an ASCII and non-ASCII alternative? If number 2 is the preferred sty;e to number 3, I would have though that the built-in notation would be named (and would merge the ASCII and non-ASCII syntaxes into a single kind). Furthermore, the lacked of scoped/local macro_rules means that you would need to write the macro directly if you want either of those attributes.

[Mac]

I guess my point here is: I would never have thought that solution number 2 was preferred to solution number 3 with the way the built-in notation is structured. However, in retrospect, thinking about how parser works, I can see why 2 would technically be the preferable solution. This makes me wonder why the built-in notation is structured the way it is.

[Sebastian Ullrich]

You don't know to know the parser name for macro_rules

macro_rules
  | `($a + $b) => `(List.append $a $b)

[Sebastian Ullrich]

ASCII/Unicode notation is an interesting point, though it applies to both 2) and 3) equally

[Mac]

Oh yeah, I forgot that macro_rules auto-infers kinds! Though, as you noted, my points about the limitations that macro_rules imposes for such a solution still stand (i.e. the doubling of the rule and the lack of scoped/local).

[Sebastian Ullrich]

Yeah, scope/local macro(_rules) seems sensible to me. The duplication issue would be solved by making the ASCII notation use the Unicode notation (seems more sensible that way around), but we explicitly declare them in that order so the pretty printer of the latter wins, oops...

[Sebastian Ullrich]

Anyway, just use 1) for them :) . Where possible.

[Mac]

Sebastian Ullrich said:

The duplication issue would be solved by making the ASCII notation use the Unicode notation (seems more sensible that way around), but we explicitly declare them in that order so the pretty printer of the latter wins, oops...

Why not just have the Unicode notation expand to the ASCII? Then you could still keep the auto-generated pretty printer that prints the Unicode alternative. I also don't see why having the ASCII notation as the base would hurt (as, when it comes to rule-writing, the ASCII notation is quicker to input).

[Sebastian Ullrich]

By that logic, we should prefer the ASCII notation everywhere :frowning: . I don't think that is what the average Lean code looks like.

[Brandon Brown]

Mac said:

Also, there is one thing that I forgot to mention earlier that I am curious about. List concatenation is generally denoted with the ++ operator as opposed to the + operator. In fact, for this reason, there is actually no Add instance for the built-in List. So, technically, if you wanted to use + for a list you could just add an Add instance for it instead of defining new notation. All in all, I'm just a little curious as to why you decided to use + to denote concatenation.

Oh I'm just messing around with Lean4. To test type classes I just defined my own HasAdd typeclass and defined add for nat and decided to make an add for list that was actually append. Just the first thing that came to mind since the second type I made was list after nat. But yes ++ makes more sense.

[Mac]

Sebastian Ullrich said:

By that logic, we should prefer the ASCII notation everywhere :frowning: . I don't think that is what the average Lean code looks like.

Well no, obviously that is not Lean's philosophy. After all, there are many notations without ASCII alternatives. However, for those with them, such an approach seems logical. Anyway, outside of the macro rule, code can pick whatever it wants to use. Also, given how the auto-generated pretty printers work, this seems to be the simplest solution.

[Mac]

Alternatively, the mixfix commands could have some kind of intelligent support for string alternations, i.e.

infix:50 (" <= " <|> " ≤ ") => LE.le

[Mac]

Or it could even use a special syntax so that it is clear which is preferred (i.e. a comma delimited list where the first/last is the symbol use for pretty printing).