Lean Hide Root Names/Macros

Stream: lean4

[Mac]

Is there any why to hide the names/macros from the root namespace to prevent pollution?

I know I can start a file with prelude to prevent the auto-import of Init, but this doesn't help if I still need to access some of the names from it. What I really would like is if all the stuff in Init was in a Prelude namespace of some kind that I could toggle whether or not it was open, thus keeping the names available through qualification but preventing pollution when desired. However, I may also just be missing that there some simple way to hide names/macros and that is why such a Prelude namespace is unnecessary.

[Mario Carneiro]

You can put your code in a namespace; it will override the names from the global namespace in case of a conflict

[Mac]

Mario Carneiro said:

You can put your code in a namespace; it will override the names from the global namespace in case of a conflict

That only works within the exact same namespace. You cannot then open the definition in a peer namespace and still use it. For example:

namespace Test
namespace Defs

class Add (T : Sort _) :=
  add : T -> T -> T

infix:65 " + "  => Add.add

-- Works: Test.Defs.Add overrides _root_.Add
def addComm {T : Sort _} [Add T] {a b : T} := a + b = b + a

end Defs
open Defs

-- Errors
def addAssoc {T : Sort _} [Add T] {a b c : T} := (a + b) + c = a + (b + c)
/-
ambiguous, possible interpretations
  Add T

  Defs.Add T
-/

end Test

I am looking for something that would the above work.

[Daniel Selsam]

@Mac AFAIK there is no way to do this right now. I hit a similar issue opening Mathlib and trying to use set, since it clashes with MonadStateOf.set which is exported into _root_. This issue may or may not be addressed in the future. Init's _root_ is pretty small, and my particular issue will go away once Mathlib.set becomes Mathlib.Set.

[Mac]

Daniel Selsam said:

Mac AFAIK there is no way to do this right now. I hit a similar issue opening Mathlib and trying to use set, since it clashes with MonadStateOf.set which is exported into _root_. This issue may or may not be addressed in the future. Init's _root_ is pretty small, and my particular issue will go away once Mathlib.set becomes Mathlib.Set.

This is why I think Init's _root_ should be put into a Prelude namespace which is auto imported and opened unless the file begins with prelude, similar to Haskell.

[Mario Carneiro]

By the way mathlib also has Set

[Mario Carneiro]

not to be confused with set

[Mario Carneiro]

More generally, mathlib has been using camel casing for bundled things and categories, meaning that we will hit a naming clash if we start camel casing everything

[Mario Carneiro]

Mac said:

Daniel Selsam said:

Mac AFAIK there is no way to do this right now. I hit a similar issue opening Mathlib and trying to use set, since it clashes with MonadStateOf.set which is exported into _root_. This issue may or may not be addressed in the future. Init's _root_ is pretty small, and my particular issue will go away once Mathlib.set becomes Mathlib.Set.

This is why I think Init's _root_ should be put into a Prelude namespace which is auto imported and opened unless the file begins with prelude, similar to Haskell.

I think it would make more sense to call the namespace Init

[Daniel Selsam]

Mario Carneiro said:

More generally, mathlib has been using camel casing for bundled things and categories, meaning that we will hit a naming clash if we start camel casing everything

Is there a proposal yet for naming in Mathlib4? Ideally Lean4 and Mathlib4 agree. It is still an open issue in Lean4: https://github.com/leanprover/lean4/issues/402

[Mac]

Mario Carneiro said:

I think it would make more sense to call the namespace Init

That works too! Though I would then suggest that the prelude command be renamed to something like no_implicit_init (snake case because it is a command like nat_lit).

[Daniel Selsam]

@Mac It may also be possible to just expose #hide _root_.Add or even #overload_priority Defs high

[Daniel Selsam]

With user-hat I like Init namespace, but right now I have no sense of how much trouble that change would cause.

[Mario Carneiro]

Another issue with Init.* and Mathlib.* is that we will be bringing back the issue where you don't know whether foo is Init.foo or Mathlib.foo, since mathlib often extends theories from core. In lean 3 mathlib this manifests as not knowing whether something is in init.data.nat.lemmas or data.nat.basic, or data.vector (core) vs data.vector2 (mathlib). Lean 4 has Nat.mul_one, and I'm sure mathlib will want to have Nat.div_one. If these are actually Init.Nat.mul_one and Mathlib.Nat.div_one it will be a nightmare to guess the names

[Mario Carneiro]

In short, mathlib has the policy that file / module namespaces are not tied to theorem namespaces, any file can add theorems to any namespace, and while this has some downsides, I think the flexibility is important (see Gabriel's point about 31 files with namespace List)

[Mario Carneiro]

Daniel Selsam said:

Mario Carneiro said:

More generally, mathlib has been using camel casing for bundled things and categories, meaning that we will hit a naming clash if we start camel casing everything

Is there a proposal yet for naming in Mathlib4? Ideally Lean4 and Mathlib4 agree. It is still an open issue in Lean4: https://github.com/leanprover/lean4/issues/402

I never fell out of love with the snake case naming convention, so it's hard to say. Are we assuming that's not on the table?

[Daniel Selsam]

Mario Carneiro said:

Daniel Selsam said:

Mario Carneiro said:

More generally, mathlib has been using camel casing for bundled things and categories, meaning that we will hit a naming clash if we start camel casing everything

Is there a proposal yet for naming in Mathlib4? Ideally Lean4 and Mathlib4 agree. It is still an open issue in Lean4: https://github.com/leanprover/lean4/issues/402

I never fell out of love with the snake case naming convention, so it's hard to say. Are we assuming that's not on the table?

The plan is to use camelCase for programs and snake_case for theorems, but there are still some corner cases to work out.

[Johan Commelin]

So what will group and ring be?

[Johan Commelin]

In Lean 3, we have group G for the class of group structures on G (so semi-bundled) and Group for the type that is the category of bundled groups.

[Johan Commelin]

Mario Carneiro said:

In short, mathlib has the policy that file / module namespaces are not tied to theorem namespaces, any file can add theorems to any namespace, and while this has some downsides, I think the flexibility is important (see Gabriel's point about 31 files with namespace List)

I agree that decoupling filenames and namespaces give mathlib/Lean 3 an important flexibility.

[Mac]

Mario Carneiro said:

Another issue with Init.* and Mathlib.* is that we will be bringing back the issue where you don't know whether foo is Init.foo or Mathlib.foo, since mathlib often extends theories from core. In lean 3 mathlib this manifests as not knowing whether something is in init.data.nat.lemmas or data.nat.basic, or data.vector (core) vs data.vector2 (mathlib). Lean 4 has Nat.mul_one, and I'm sure mathlib will want to have Nat.div_one. If these are actually Init.Nat.mul_one and Mathlib.Nat.div_one it will be a nightmare to guess the names

Isn't that kind of the point of documentation? To tell you where things are? Furthermore, couldn't you just export the names from Init.* into Mathlib.* that should also belong there? For example:

namespace Mathlib
export Init.Nat (mul_one)
end Mathlib

More generally, while I do think it is a bad idea for libraries to toss anything in the root namespace (as long as there remains no way to hide polluting names/macros), that is a decision for mathlib and its users. I think Lean itself forcing things into root is a much bigger problem, because it makes writing alternative foundations very inconvenient. Right now, I am working on my own logical system and having Lean eat common names and notations is quite annoying.

Daniel Selsam said:

Mac It may also be possible to just expose #hide _root_.Add or even #overload_priority Defs high

This is a good middle ground if an Init namespace proves too much trouble. However, I personally would strongly suggest the use of a namespace. Also, I don't see why it would be much trouble. Wouldn't it just involving wrapping the Init files in namespace Init and then altering the auto-import of Init to also open Init? For most end users (who don't need name hiding), wouldn't this change be virtually unnoticeable?

[Kevin Buzzard]

Just another random data point (although I have absolutely no idea how reasonable this is): when I'm teaching with Lean 3 I have the following problem. I want all tactics accessible so I import tactic and this imports group. But maybe I want to teach groups from first principles and so I want to define groups again from first principles. So I go into the xena namespace and make groups there. Me and students have made a group theory library which contains things like Sylow's first theorem all with our own definition of group. But because things like mul_assoc are in the root namespace we have to be careful to avoid naming clashes and ambiguity. We usually muddle through though and I'm not sure if much can be done about it.

[Daniel Selsam]

Daniel Selsam said:

Mac AFAIK there is no way to do this right now. I hit a similar issue opening Mathlib and trying to use set, since it clashes with MonadStateOf.set which is exported into _root_. This issue may or may not be addressed in the future. Init's _root_ is pretty small, and my particular issue will go away once Mathlib.set becomes Mathlib.Set.

Here is another example: you can't use Lean.Parser.optional outside of Lean.Parser namespace, since it clashes with https://github.com/leanprover/lean4/blob/master/src/Init/Control/Basic.lean#L34-L35