open unscoped

Stream: mathlib4

[Kenny Lau]

#31086 introduces a new syntax:

open unscoped Foo1 Foo2 Foo3 ...

which opens the namespaces without activating its scope (i.e. instances or notations)

Example usage:

namespace Nat

def pi : Nat := 3
scoped notation "π" => pi

end Nat

open unscoped Nat

#check pi
#check π -- error

[Kenny Lau]

do we want this?

[Sébastien Gouëzel]

I'd say we shouldn't need this. If there is a feeling we need this, it's probably because we have too specific notations in too general namespaces, and then I'd say the solution would rather be to scope more these specific notations.

[Kenny Lau]

let me add the context was #lean4 > Why "scoped notation" for Euler's totient function?

[Kenny Lau]

specifically φ in the Nat namespace for totient

[Kenny Lau]

Sébastien Gouëzel said:

I'd say we shouldn't need this. If there is a feeling we need this, it's probably because we have too specific notations in too general namespaces, and then I'd say the solution would rather be to scope more these specific notations.

but then I would also say that π is a very important symbol so it deserves to be in the Real namespace and not hidden any further like Real.PiNotation

[Kenny Lau]

φ and ψ (golden ratios) are currently hidden in deeper namespaces btw

[Kenny Lau]

and yeah the golden ratio clashes with totient...

[Sébastien Gouëzel]

I agree with you that pi deserves to be in the Real namespace. On the other hand I would scope more phi for totient, it's too specific to be in the Nat namespace.

[Kenny Lau]

I feel like "hiding in deeper namespaces" is precisely the workaround that arises from the fact that we don't currently have open unscoped...

[Sébastien Gouëzel]

I'd rather say that hiding in deeper namespaces gives more flexibility. With open or open scoped or open unscoped, it's always an all or nothing mechanism. If we consider that some notations are more important than others (for instance pi is a more important real number than phi or psi), then deeper namespaces look like a good solution to me. Some Nat notations are important (like factorial), some are less important (like totient), so I'd go for deeper namespaces there.

[Kenny Lau]

that is a good point about flexibility, so what about instead of hiding in deeper namespace (which would require one to remember which namespace each notation is in, which is bad (e.g. look at Spec)), what if we modify the open syntax so that we can specify which notations to open?

[Kenny Lau]

that is, a third solution outside "deeper namespace" and "open unscoped"

[Kenny Lau]

so e.g. we can write open Nat (hiding φ)

[Chris Henson]

Downstream of Mathlib, we have less immediate control over moving notation to a deeper namespace, so having a command like this would be nice.

I do also like the idea of also being able to hide specific notations, is this hard to implement?

[Kenny Lau]

i haven't tried

[Kenny Lau]

@Chris Henson on the other hand, maybe your downstream project can just use my code for open unscoped

[Kenny Lau]

@Robin Arnez do you know which part of the parser is responsible for looking at a syntax (e.g. π) in a scope (e.g. Real) and then finding the corresponding notation identifier (e.g. Real.termπ)?

[Lua Viana Reis]

Kenny Lau said:

so e.g. we can write open Nat (hiding φ)

how would this support hiding notation that is not composed of a single token?

[Lua Viana Reis]

since notation definitions don't have a "name", it makes a lot sense to me that they are associated to their namespace

[Kenny Lau]

good point

[Floris van Doorn]

Notation definitions do have a name. We should probably not write those in the source code though...

[Lua Viana Reis]

yes, I meant that they are usually autogenerated

[Markus Himmel]

Floris van Doorn said:

We should probably not write those in the source code though...

Core does this for the recommended_spellings (example) and so far I don't think it's been a problem.

[Lua Viana Reis]

for some things, the generated name can look pretty strange imo
image.png

[Kenny Lau]

what if we force mathlib to name all notations

[Kenny Lau]

ok we have at least 2k notations so maybe that's not a good idea

[Lua Viana Reis]

But if hiding... happens to be implemented, I think it should use the names, so your example would be open Nat (hiding termφ)

[Kenny Lau]

I would have to look into it, I think scope works differently

[Floris van Doorn]

I personally would be happy with a command where you can open a namespace, except explicitly mentioned scoped notation (I guess for attributes it's even trickier how to specify that you don't want them).

I agree with Sébastien Gouëzel that we should also keep uncommonly-used scoped notations out of widely used namespaces. But the flexibility of such a command seems useful.

[Kim Morrison]

Kenny Lau said:

what if we force mathlib to name all notations

ok we have at least 2k notations so maybe that's not a good idea

On the contrary, that fact that Mathlib has so many notations increases the value of asking that they be named. :-)

[Eric Wieser]

Didn't we require they be named during the port?