## Stream: lean4

### Topic: Lean Hide Root Names/Macros

#### Mac (Apr 15 2021 at 00:41):

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 (Apr 15 2021 at 01:28):

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

#### Mac (Apr 15 2021 at 19:31):

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

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

-/

end Test


I am looking for something that would the above work.

#### Daniel Selsam (Apr 15 2021 at 19:45):

@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 (Apr 15 2021 at 20:34):

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 (Apr 15 2021 at 23:35):

By the way mathlib also has Set

#### Mario Carneiro (Apr 15 2021 at 23:35):

not to be confused with set

#### Mario Carneiro (Apr 15 2021 at 23:36):

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 (Apr 15 2021 at 23:38):

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 (Apr 15 2021 at 23:58):

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 (Apr 16 2021 at 01:21):

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 (Apr 16 2021 at 01:38):

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

#### Daniel Selsam (Apr 16 2021 at 01:40):

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

#### Mario Carneiro (Apr 16 2021 at 06:34):

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 (Apr 16 2021 at 06:37):

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 (Apr 16 2021 at 06:38):

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 (Apr 16 2021 at 14:45):

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 (Apr 16 2021 at 14:46):

So what will group and ring be?

#### Johan Commelin (Apr 16 2021 at 14:47):

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 (Apr 16 2021 at 14:49):

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 (Apr 16 2021 at 19:18):

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 (Apr 16 2021 at 23:34):

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.

Last updated: May 18 2021 at 22:15 UTC