dot notation and open

Stream: lean4

[Eric Wieser]

Is this intended behavior?

def Wat.Prod.thd {α β γ} (x : α × β × γ) : γ := x.2.2

open Wat in
#check (1, 2, 3).thd -- works!

[Kyle Miller]

Yes, the idea is supposed to be that you can open some functions for your own library, without polluting another namespace you don't own.

[Eric Wieser]

This ends up a little confusing with things like

import Mathlib

open List
#check #v[1].exists_eq_cons

which is trying to invoke List.Vector.exists_eq_cons on _root_.Vector

[Kyle Miller]

(lean4#6189 was the change)

[Eric Wieser]

For what it's worth, this isn't breaking me, I just was surprised by the feature, and it seems risky in the face of types that share a name in different namespaces.

[Kyle Miller]

That's not good... but I think it's also not good practice sharing name components like this, having the same name for a type in different namespaces.

[Kyle Miller]

At least in this case it's just surprising it resolves at all, right? Not that you're not getting things that you want to resolve to resolve?

[Eric Wieser]

Indeed, I don't have an example where it's harmful, only where it fails confusingly

[Mario Carneiro]

Kyle Miller said:

That's not good... but I think it's also not good practice sharing name components like this, having the same name for a type in different namespaces.

This is a new change to 'good practice' if so. To me it seems quite reasonable if you have several different versions of an API which are separated by their namespace

[Mario Carneiro]

in fact, it largely defeats the purpose of namespaces, it means we have to be globally unique again and worry about name conflicts caused by this

[Eric Wieser]

For what it's worth, C# has this feature via "extension methods", but it's opt in by marking one of the arguments in a special way

[Mario Carneiro]

I don't think C# has the ability to turn extension methods on and off again, or does it?

[Mario Carneiro]

in rust if you use typeclasses to define extension methods then they are available as long as you have opened the typeclass, so you can turn them off and on again to some extent

[Kyle Miller]

Mario Carneiro said:

This is a new change to 'good practice' if so. To me it seems quite reasonable if you have several different versions of an API which are separated by their namespace

It's not a change — I'm expressing a personal opinion.

Let me refine this opinion: if you have multiple namespaces you are working with and you want to open them all, you shouldn't reuse name components. In my experience, it's not good practice, since the name conflicts cause issues. (I personally like to avoid reusing any name components between namespaces that tend to be used in modules together, even if I don't open them, but that's not a strict rule.)

Here we have Vector and List.Vector, with open List. Would you agree that having List.Vector defeats the purpose of being able to open List?

[Mario Carneiro]

I agree that you shouldn't use Vector and List.Vector at the same time if you have used open List

[Mario Carneiro]

Is it the case that all problematic situations here for dot notation are also problematic in the sense of having an ambiguous name in scope?

[Jireh Loreaux]

If I understand correctly, the net effect of this is we could namespace Mathlib and nothing would break (in Mathlib, downstream would then have to open Mathlib a lot). Is that correct? This would obviate the biggest obstacle in my mind to that choice.

[Kevin Buzzard]

+1 to namespacing Mathlib BTW. I don't see why we should be arrogant enough to just take the root namespace for our ideas.

[Eric Wieser]

I don't think that was really the point of Jireh's comment; we could have Mathlib.Group anyway, it's things like docs#Nat.digits that the re-namespacing of is more controversial.

[Niels Voss]

The doc-gen site would display Mathlib before every definition name, though

[Kim Morrison]

Good? Or if it's bad, then change doc-gen? Seems a minor problem!

[Niels Voss]

Out of curiosity, would this allow two different versions of Mathlib based on the same Lean version to be loaded simultaneously by changing one of the namespace names? (I am not claiming this is a good idea, I'm just wondering if it would be possible)

[Niels Voss]

Actually nevermind, there are overlapping tactics and global notations

[Yaël Dillies]

Niels Voss said:

The doc-gen site would display Mathlib before every definition name, though

And loogle too. This is already a big issue when

1. We can't use scoped notation in loogle
2. There are super long namespaces like CategoryTheory

[Eric Wieser]

1: yes we can, open scoped Foo in $your_search

[Sebastian Ullrich]

A user-configurable, persistent set of default opens for Loogle seems like a reasonable feature request to me, I would use it for open Lean!

[Kenny Lau]

It seems like there's another potentially unintended behaviour:

axiom A : Type
axiom B : Type

namespace A

-- comment me out
open A

axiom B.c (x : B) : Type

variable (x : B)

#check x.c

end A

[Kenny Lau]

you have to actually open the namespace to make this bug work, even if you're already in the namespace! (I would have previously assumed that the namespace is automatically opened in the namespace)

[Kyle Miller]

@Kenny Lau I was experimenting with this recently in the unfinished lean4#9636 to try to address issue lean4#6135

The current rules for dot notation ignore the current namespace when resolving the name. Roughly, the way name resolution works in general is that it first uses all prefixes of the current namespace to find a name, and if that doesn't work, it tries all the open namespaces. The PR would make it use the namespaces.

The idea of the PR is to make it possible to be in namespace A, then define A.IO.FS.Stream.foo, and then use it with dot notation. And, while making sure that open IO will always open _root_.IO, even if it might also open A.IO because you're somewhere in the A namespace.

[Martin Dvořák]

I am happy with Mathlib having the monopoly for defining what Group is.
My personal preference is to not namespace everything.

[Kyle Miller]

(Link to an MWE about a possibly related issue: #mathlib4 > dot notation @ 💬 )