Nested namespaces

Stream: lean4

[Michael Stoll]

import Mathlib

lemma A.a : 1 = 1 := rfl
lemma A.B.b : 2 = 2 := rfl
lemma B.b : 3 = 3 := rfl

namespace A

-- want to access `B.b` as `b`, but:

open B

#where -- `open A.B`
#check b -- `A.B.b : 2 = 2`

open _root_.B -- `unknown namespace '_root_.B'`

Is there a way to open namespace B (and not A.B) while in namespace A?

[Kyle Miller]

I don't believe so. Here's an issue you could :+1: lean4#3045

[Kyle Miller]

(You could also add your example as a comment if it would be a helpful test case.)

[Michael Stoll]

I don't think the example really adds something here.

[Richard Osborn]

Would there be problems with open always using the root namespace by default? I would think that's the behavior that most people would expect.

[Michael Stoll]

I think this was the lean3 behavior.
If you really want A.B, you can write open A.B, I suppose... But this may be less nice when A is very long.

[Richard Osborn]

If we needed notation for that open .B might be a solution, but I would hope namespaces don't become that cumbersome.

[Kyle Miller]

It's used pretty often, writing things like open Lean Meta Elab Term PrettyPrinter Delaborator, rather than open Lean Lean.Meta Lean.Elab Lean.Elab.Term Lean.PrettyPrinter Lean.PrettyPrinter.Delaborator.

Writing open Lean .Meta .Elab .Term .PrettyPrinter .Delaborator wouldn't be so bad, though using _root_ for absolute names is already a solution elsewhere in Lean.

[Michael Stoll]

What happens when there are namespaces A, B, A.C, B.C and I do open A B C?

import Mathlib

lemma A.a : 0 = 0 := rfl
lemma B.b : 1 = 1 := rfl
lemma A.C.c : 2 = 2 := rfl
lemma B.C.c : 3 = 3 := rfl

open A B C
#where -- `open A B B.C A.C`

Is this what people would expect?

[Michael Stoll]

I think one problem is that after namespace A, open B one potentially has a different set of open namespaces than after open A B:

import Mathlib

lemma A.a : 0 = 0 := rfl
lemma B.b : 1 = 1 := rfl
lemma A.B.c : 4 = 4 := rfl

namespace A
open B
#where -- `namespace A, open A.B`
end A

#where -- In root namespace with initial scope

open A B
#where -- `open A B A.B`

[Michael Stoll]

... and that the set of open namespaces can change by adding or removing declarations further up in the file.
E.g., removing the lemma A.B.c above replaces open A.B in the first #where by open B.

[Kyle Miller]

To tell the truth, I never really feel like I know what will be open. However, while I have few expectations on what open does, I do feel some surprise that open A B C opens four namespaces. There's a logic to it, but it's still unexpected.

[Michael Stoll]

...actually five when A.B also exists.

[Michael Stoll]

In any case, the mental model that namespace A includes the effect of open A is clearly wrong.

[Kyle Miller]

I should mention that a feature we rely on for this to not be total madness is that name resolution is partly type directed, so even if the same name is used across multiple namespaces, it can still often be disambiguated.

[Michael Stoll]

Indeed,

import Mathlib

lemma A.a : 0 = 0 := rfl
lemma B.b : 1 = 1 := rfl
lemma A.B.c : 4 = 4 := rfl
lemma C.c : 37 = 37 := rfl
lemma A.C.d : 43 = 43 := rfl
lemma B.C.e : 389 = 389 := rfl
lemma C.A.f : 55 = 55 := rfl -- not this one, though!
lemma A.B.C.x : 5077 = 5077 := rfl

open A B C
#where -- `open A B A.B C A.B.C B.C A.C`

[Damiano Testa]

For that, you can probably add another A after C.

[Michael Stoll]

Kyle Miller said:

I should mention that a feature we rely on for this to not be total madness is that name resolution is partly type directed, so even if the same name is used across multiple namespaces, it can still often be disambiguated.

I think the problem is not so much that too much is opened, but rather, too little (in the namespace case).

[Damiano Testa]

My usual approach is to try to avoid pushing the limits of open/namespace and try to rely on them in a conservative way.

[Michael Stoll]

So, would it be problematic if namespace A, open B would open B and A.B?

[Michael Stoll]

(so as to be consistent with open A B)

[Michael Stoll]

Damiano Testa said:

My usual approach is to try to avoid pushing the limits of open/namespace and try to rely on them in a conservative way.

How do you deal with the problem that you cannot access a declaration B.b unqualified in namespace A when namespace A.B also exists?

[Damiano Testa]

If I really had to do that, I would probably close all namespaces and then use fully qualified names. In my experience, I have not ran into this issue often enough to really be more than amused by it.

[Michael Stoll]

(One can do open B, namespace A, but this does not work locally with open B in.)

[Damiano Testa]

Well, if you bring in open ... in, would you also then not expect namespace X in ... to work? That's another "feature" that creates more asymmetries.

[Michael Stoll]

Why should this not work? (I know it doesn't, but is there a good reason?)

[Damiano Testa]

The reason is that in really expands to section [unnamed] command end and then if command has a namespace, it wants to close itself, not the unnamed end.

[Damiano Testa]

If you actually remove the in and add section before and end after, it will become clear.

[Damiano Testa]

Btw, this could be a "fix" for namespace in:

macro_rules
  | `(namespace $id in $cmd) => `(section namespace $id $cmd end $id end)

namespace X in  -- works
theorem hi : True := .intro

#check X.hi  -- works

[Kyle Miller]

I think that's equivalent to theorem X.hi : True := .intro

[Kyle Miller]

(minus the extra section)

[Kyle Miller]

Take a look at the first case in the match in docs#Lean.Elab.Command.elabDeclaration

[Damiano Testa]

Yes, I also think that it is -- I was not seriously proposing it as an addition, just a way of "restoring symmetry".

[Damiano Testa]

Kyle Miller said:

Take a look at the first case in the match in docs#Lean.Elab.Command.elabDeclaration

Indeed, this is something that confused me very much the first time I ran into it.

[Damiano Testa]

(And, after the confusion, I find it useful!)

[Damiano Testa]

Another point of view is that the asymmetry is that open X "cannot be closed", while namespace X can.

[Kyle Miller]

That reminds me, there was an idea for namespace X in that would resolve X first, so that you could reliably add methods for dot notation, even if things got refactored. Implementation: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/More.20reliable.20.22methods.22.3F/near/399819556

[Michael Stoll]

Consider the following scenario.

File Y.lean contains

import X

namespace B

lemma bar1 ... : ... := ...
lemma bar2 ... : ... := ...
lemma bar3 ... : ... := ...

end B

namespace A

open B in
theorem foo ... : ... := (proof uses bar1, bar2, bar3)

end A

and everything works.

Now at some later point, somebody adds a declaration A.B.ohno in file X.lean. The result is that the proof of theorem A.foo in Y.lean will break down, and whoever looks at it will have a hard time figuring out what the problem is. (Of course, it doesn't have to be X.lean; it could be any file in the transitive import closure, and whoever added A.B.ohno will likely have no idea of the ripple effects.)

I think that adding stuff to imports leading to declarations no longer being available (without namespace qualification) downstream is rather bad behavior and should be avoided. (I know that , say, adding simp lemmas can also break proofs downstream if they use non-terminal simp, but this is a different matter.)

I think a reasonable solution would be to have open B within namespace A behave like open B within open A, i.e., open all existing namespaces among B and A.B. Then the namespace A.B coming into existence will not remove access to B.

[Michael Stoll]

I also don't think it is good that, assuming namespaces A, B, A.B and B.A all exist, there is no way to open just A and B and not also A.B (with open A B) or B.A (with open B A).

(This goes somewhat against what I suggested above, but my main point there is to avoid that establishing a namespace has surprising effects downstream.)

Essentially, I would want to be able to figure out exactly which namespaces are open at a given location just by looking at the file it is in.

[Michael Stoll]

:up: Can perhaps one (or more) of the developers comment on this? (Not sure who to ping here...)

[Kim Morrison]

Doesn't seem particularly high priority to me? At least, I haven't been bitten by it.

[Michael Stoll]

I'm not asking for an immediate fix, but I'd like to know if others also see this behavior as problematic.