Control namespaces

Stream: lean4

[Andrej Bauer]

Is there an option (such as autoImplicit) that means "arbitrary namespaces which are likely typos should not be silently accepted"? I get bitten by stuff like this:

structure STree := ...

def Stree.map := ...  -- this should be an error, I mispelled Stree

Even this works -- and it's not a good idea:

def once.upon.a.time.there.was.a.kingdom := 42

[Mario Carneiro]

unfortunately not, because namespaces are never really "declared" in lean, their existence is inferred from first use, kind of like using mkdir -p when writing a declaration

[Andrej Bauer]

Oh my.

[Mario Carneiro]

they are actually a thing that can be declared in the sense that open STree works and open Stree doesn't (until after your typo'd declaration), but there is no def namespace command

[Mario Carneiro]

A linter might be able to catch your example, but this simple syntactic fact about implicit namespace creation in idiomatic code prevents catching all cases without a biggish refactoring of lean and the ecosystem

[Chris Bailey]

Andrej Bauer said:

I get bitten by stuff like this:

structure STree := ...

def Stree.map := ...  -- this should be an error, I mispelled Stree

Fwiw the way people usually seem to do this (which also gets rid of the class of errors you're running into) is:

structure STree := ...

namespace STree

def map := ..
def fold := ..

end STree

[Andrej Bauer]

That's a good idea, thanks. BTW, I have learned through pain that open is evil.

[Adam Topaz]

Would you consider open Foo in ... less evil?

[Kyle Miller]

(I once cut my hand with a knife while carving and learned that knives are evil too :wink:)

[Kyle Miller]

Though open is definitely similar to Python's from Foo import *, which I pretty much never use. It's able to do some type-based disambiguation at least, which Python doesn't give you, and Lean gives you static checking. Usually in Lean I open namespaces (within a section/namespace) if I'm working with something that could have been in another namespace, but for whatever reason it's better to be in a new namespace.

[Kyle Miller]

One painful thing is that there are a couple of key namespaces with the same function name, like there's both docs4#Lean.Elab.Term.elabTerm and docs4#Lean.Elab.Tactic.elabTerm with essentially the same type signature if you're in the TacticM monad due to lifting.

[Andrej Bauer]

If ... is less than a screenful of code, yes.

[Chris Bailey]

Andrej Bauer said:

That's a good idea, thanks. BTW, I have learned through pain that open is evil.

What's the beef with open? I feel like most languages have a similar mechanism.

If you're using VScode, the current namespce and section information for your cursor will show up in the breadcrumbs line, which is at the top/under any tabs. You can get nice results with open commands by using them within sections (thanks Mario) :

section
open STree
/- closes STree -/
end

section Named
open STree
/- closes STree -/
end Named