global mathlib namespace

Stream: mathlib4

[Tomas Skrivan]

Would it be possible to put everything in mathlib in Mathlib namespace? I often run into problem that I want to use some name in a project depending on mathlib but it is already used by mathlib. Recent example: both Rand and Random are claimed by mathlib.

[Sébastien Gouëzel]

We shouldn't namespace everything in the Mathlib namespace, no. But we should namespace everything which is too short and could create conflicts. Your two examples are very good examples of this: these ones should definitely be namespaced, and it's very good that you mention them here so that we can fix it.

[Ruben Van de Velde]

Hm, if we're going to namespace parts, I think we might as well namespace everything, no?

[Tomas Skrivan]

What is the argument against namespacing everything? You just add namespace Mathlib at the top of every file and you are done. In every math formalization project depending on mathlib you just add open Mathlib at the top of every file.

[Sébastien Gouëzel]

I don't want to put CompactSpace in a namespace, because no user should want to introduce another notion than the one we have. But Gen or Rand, I definitely want to namespace them because they are way too generic.

[Tomas Skrivan]

I agree that the likelihood that someone might want to define a new CompactSpace is very low. However, it is hard to judge what passes the bar and what not and in my opinion would lead to more confusion then putting everything in one namespace.

[Kevin Buzzard]

In lean 3 putting things in a namespace could cause some confusion when there were multiple interpretations but in lean 4 this seems to work really well. For CompactSpace the argument that it shouldn't be the only one is "what if one of my students decides to make compact spaces themselves as a project?" but we already have a good answer for this, namely the student puts it in their own namespace.

[Enrico Borba]

It would be nice if there was a lean 4 equivalent of python's "import .. as ..". Something like:

namespace Mathlib
import Mathlib.Data.Set.Basic
end Mathlib

[Tomas Skrivan]

Kevin Buzzard said:

In lean 3 putting things in a namespace could cause some confusion when there were multiple interpretations but in lean 4 this seems to work really well. For CompactSpace the argument that it shouldn't be the only one is "what if one of my students decides to make compact spaces themselves as a project?" but we already have a good answer for this, namely the student puts it in their own namespace.

Yes this works but I still want to use mathlib's Rand and use my own Rand. I end up writing

namespace MyRand
structure Rand (X : Type) [MeasurableSpace X] where
  μ : Erased (Measure X)
  rand : _root_.Rand X

Having mathlib namespace I would write Mathlib.Rand vs _root_.Rand. I would prefer the former but I can live with the later.

[Mario Carneiro]

maybe don't call it Rand?

[Tomas Skrivan]

What else? Maybe RandVar but I don't like it.

[Mario Carneiro]

Oh I thought it was a probability space or something

[Mario Carneiro]

or a monad

[Tomas Skrivan]

It is almost a monad

[Mario Carneiro]

docs#Rand

[Mario Carneiro]

mathlib's Rand is definitely a monad

[Tomas Skrivan]

Yes it is the same as mathlibs Rand is just has the measure that should specify the random number generator. There is no connenction between the two yet

[Sébastien Gouëzel]

@Mario Carneiro , do you agree that claiming Rand in mathlib is excessive? What namespace should we put it in in this case?

[Mario Carneiro]

seeing StdGen and MeasurableSpace in the same definition looks really weird

[Mario Carneiro]

I'm still trying to understand the purpose for which it is being used

[Mario Carneiro]

I don't think Mathlib.Rand is any better of a name than Rand

[Mario Carneiro]

Looking at the definition, I think the name Rand is defensible, although I think we should avoid the Random class

[Mario Carneiro]

We could also call it RandM

[Mario Carneiro]

It seems to be similar to State and Reader monads, which are also unnamespaced

[Mario Carneiro]

RandM seems like a nice compromise which solves the immediate problem

[Mario Carneiro]

I do wonder if we should just remove this file entirely though, it's only used once

[Tomas Skrivan]

Mario Carneiro said:

I'm still trying to understand the purpose for which it is being used

I want to write a program in the Rand monad and then reason about it.

[Kevin Buzzard]

I guess one could also ask: should List be in the Core namespace and should [some basic std thing] be in the Std namespace?

[Mario Carneiro]

Tomas Skrivan said:

Mario Carneiro said:

I'm still trying to understand the purpose for which it is being used

I want to write a program in the Rand monad and then reason about it.

I guess this is like your Real -> Float trick, where you are making claims that are provably false if you poke at them too hard but it doesn't matter because programmers do it in practice anyway

[Mario Carneiro]

in this case, it is the claim that StdGen is a true random number generator

[Tomas Skrivan]

Yup, it is definitely not going to be aimed to prove some privacy security or crypto.

[Tomas Skrivan]

Mario Carneiro said:

in this case, it is the claim that StdGen is a true random number generator

Yes exactly

[Eric Rodriguez]

Kevin Buzzard said:

I guess one could also ask: should List be in the Core namespace and should [some basic std thing] be in the Std namespace?

this is absolutely not unprecedented, see C# and using System. similarly with c++ and using namespace std. Lean core itself is mostly all namespaced under Lean

[Mario Carneiro]

I think we should only do this if and when lean switches to some kind of module system where import Foo as Bar works

[Mario Carneiro]

I would not mind the internal name of List being something like Init.List.Basic.List but it would have to be something that I never ever write explicitly

[Mario Carneiro]

This would be a large language change, and I don't think it's on the near term or even mid term roadmap

[Mario Carneiro]

But there have been general noises in that direction for a long time

[Kyle Miller]

Eric Rodriguez said:

Lean core itself is mostly all namespaced under Lean

The Lean namespace is generally for the Lean system (metaprogramming, elaborator, compiler, etc.), vs the prelude (where you'd find List). Just want to be sure we have the fact there are multiple types of things in "core" in mind. I guess this is Init vs Lean in the docs.

In mathlib I try to make sure all the meta code is in a namespace, to keep it out of the way of the theory. Some goes in Lean if it extends core, and the rest goes in Mathlib.

[Tomas Skrivan]

Another data point. Now I'm using SciLean in a different project thus I'm no longer in SciLean namespace. To use SciLean.Rand I can't just say open SciLean and use Rand as I get unambiguity between _root_.Rand and SciLean.Rand. I'm forced to write out SciLean.Rand everywhere.

Also recently @Joe Hendrix had issue with _root_.Associative.

[Yaël Dillies]

All those examples are mostly unused in mathlib, so I'm not sure how strong of an argument you're making

[Tomas Skrivan]

Yeah probably not very strong ... yet. I will just keep collecting them and post them here :)

[Eric Wieser]

Rand is not unused, but I don't think it would matter much if it moved to a namespace

[Eric Wieser]

docs#Associative is not Mathlib's fault, that name is in the root namespace because it came from Lean itself as docs3#associative

[Eric Wieser]

(It's also fairly reasonable to argue that docs#Associative is the only possible thing that Associative could mean)

[Kim Morrison]

I don't think "it would be reasonable to argue this is the only possible definition" is the right criterion. The loser of that argument still has to write SciLean.Rand everywhere.

[Eric Wieser]

Maybe we should have something like open _root_ hiding Associative (we already have open Std hiding Associative, right?); irrespective of what is considered "well-behaved" for a package and whether Mathlib conforms to it, inevitably there will be things in the wider ecosystem which do not, and it's nice to have tools to deal with those cases.

[Tomas Skrivan]

I really do not really care about the particular instances where this is an issue. Arguing if we should rename/move Rand or Associative is sort of pointless. I'm just pointing out that such name clashes will be an issue if mathlib is used by other projects and there should be a way to deal with it.

[Kevin Buzzard]

I'm still unclear about why we don't just put everything from mathlib in a mathlib namespace. I don't agree that mathlib's definition of CompactSpace is the only definition which is allowed in Lean.