RFC: optionally disable automatic namespace based on prefix

[madvorak]

I would like to have a project-wide setting to disable automatic opening of a namespace for the declaration's name prefix.
Consider the following definition:

def List.uppcaseLetters (l : List Char) : List Char :=
  l.map Char.toUpper

The above is a nice syntax and I want it to stay allowed.
The next definition is less nice but also acceptable:

def List.uppcaseLetters (l : List Char) : List Char :=
  List.map Char.toUpper l

And here comes what I would like to change; the following definition compiles but I would like it to be (with the aforementioned project-wide setting) a syntax error instead:

def List.uppcaseLetters (l : List Char) : List Char :=
  map Char.toUpper l

Note that it is a fragile style of programming. The following code does not compile:

def Liszt.uppcaseLetters (l : List Char) : List Char :=
  map Char.toUpper l

I would rather want (with the aforementioned project-wide setting) both List.uppcaseLetters and Liszt.uppcaseLetters to be parsed the same way (here, giving a syntax error).

Similarly, I would like every theorem to be parsed the same way as if it was example instead, including its proof.

theorem List.map_comp_comp {α β γ δ : Type}
    (l : List α) (f : α → β) (g : β → γ) (h : γ → δ) :
    l.map (h ∘ g ∘ f) = ((l.map f).map g).map h := by
  -- I want `map (g ∘ f) l` to be a syntax error
  have fg : map (g ∘ f) l = (l.map f).map g := by simp
  rw [←fg]
  simp

In the example above, with the new settings, I would be forced to write List.map (g ∘ f) l or l.map (g ∘ f) because map (g ∘ f) l would cause a syntax error.
Currently map (g ∘ f) l is allowed, which is what I would like to change (optionally, for the entire project).

With the setting I suggested, it would be easier to maintain a project so that its code stays readable.
Reading l.map (g ∘ f) makes it immediately clear what function is called.
Reading map (g ∘ f) l does not make it immediately clear what function is called.
Reading List.map (g ∘ f) l is not problematic.

It can be argued that map (g ∘ f) l should be rejected by a custom linter rather than by a custom Lean setting.
However, such a change is not only a matter of style.
The status quo can have real negative consequences!
Here, the letter a is printed:

def Foo.bar : Char := 'a'

def bar : Char := 'b'

def Foo.gimmeLetter : Char := bar

#eval Foo.gimmeLetter

Here, after changing only the spelling of the last definition, the letter b is printed:

def Foo.bar : Char := 'a'

def bar : Char := 'b'

def Fooo.gimmeLetter : Char := bar

#eval Fooo.gimmeLetter

I conclude that the suggested new setting would both;

• make it easier to enforce a good style of writing code that sparks joy in people who read the code afterwards; and
• help avoid bugs.

User Experience would not change for the users who keep the default project settings.
User Experience would improve for users who change the project settings, assuming they have similar preferences as I outlined above.

Maintainability would worsen for the Lean 4 repository, as it would be an additional setting that would need to be maintained.
Maintainability would improve for project written in Lean 4, because a name change would not change the statement of a theorem or what a function does.

Discussion:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Disable.20automatic.20namespace

[eric-wieser]

Similarly, I would like every theorem to be parsed the same way as if it was example instead

example is parsed as def which has different semantics to theorem (with respect to elaboration order), in ways that occasionally trip up newcomers. I don't think what you've written is what you actually want.

[madvorak]

example is parsed as def which has different semantics to theorem (with respect to elaboration order)

I didn't know. Is it documented somewhere?

[lambda-fairy]

The way I see it, def List.uppercaseLetters ... is shorthand for

namespace List
def uppercaseLetters ...

This flag would break that correspondence, and so would make the language less consistent.

[madvorak]

It should be viewed the other way around. Opening namespaces should not be the default way to write code.

[madvorak]

As a matter of fact, I wouldn't mind at all if the same flag simultaneously forbade the syntaxes namespace and open for the entire project. All these things make the code harder to read and I want to avoid them in my projects entirely. However, I am not saying that the same flag should do those things.

[madvorak]

Note that you can avoid opening namespaces (for instance, I don't open them at all, as I find them confusing). I believe we should similarly have a choice to opt-out of this namespace-like behavior.

[Kha]

Thanks for writing up a comprehensive RFC. We looked at it again in the triage team meeting and reached consensus on my initial suspicion in #6436 (comment) that this kind of language semantics should not be toggleable with an option. If you feel strongly about disallowing a core syntax in your own projects, the best solution is to write a custom linter.