hiding the prelude? and the open/import distinction

Stream: new members

[JJ]

I would like to hide some of the identifiers in Init.Prelude: specifically Type, Monad, Functor, Applicative. How might I go about doing so?

Ordinarily I would do open Namespace hiding Idents, but since Init.Prelude is opened by default, I do not know how to do this.

[JJ]

Ah hm. I must have been holding the search wrong, because I swear I looked and nothing popped up. Past threads:

• #lean4 > Lean Hide Root Names/Macros
• #new members > hiding from prelude
• #lean4 > ✔ How to hide something from `_root_` using `open`?

These are all decently old. Is there any better way (than putting my code in a namespace) now? I would quite like it if something like open Init.Prelude hiding X was special-cased to let you hide stuff from the prelude...

[JJ]

Well, sticking prelude at the top of my file does work, despite the docs advising against doing so. However, I can only import Init.Prelude afterwards, not open Init.Prelude hiding X.

prelude
import Init.Prelude

class Monad' where
  pure : sorry
  bind : sorry

Why is this? The documentation says that "importing a module has no effect on the set of currently open namespaces". This import Init.Prelude line seems like it is certainly having an effect on the set of currently open namespaces, given it gives me naming conflicts with Monad...

[Kyle Miller]

I don't believe so. Maybe with the new module system it will eventually be possible, but I'm not sure.

By the way, open is for namespaces, not modules. Lean's name hierarchy is global. Importing modules installs declarations into this name hierarchy. Using open is for being able to refer to names somewhere in this hierarchy without needing to fully qualify them. It's sort of like adding a temporary symbolic link for the current section.

I assume you want to do this to use these top-level names for your own uses. That is not possible, due to the fact that Lean uses this global name hierarchy to identify declarations. The only way this is possible is if you use the prelude keyword and do not import Init at all, but then you lose much of Lean's functionality.

The closest you can get is to put things into your own namespace and work from within that namespace.

[Kyle Miller]

I didn't say it explicitly, but Init.Prelude is a module, not a namespace.

[JJ]

Hmm, interesting. That explains why I can't use open on it, then. How come stuff gets imported without a prefix when I type import Init.Prelude, though? Is that just how modules work? I guess that makes sense, given the line "Modules may add names to any namespace" from the documentation.

[JJ]

Where can I read about the new module system, by the way?

[JJ]

Sticking my stuff in a namespace is probably what I'll end up doing :thumbs_up:

[Kyle Miller]

JJ said:

How come stuff gets imported without a prefix when I type import Init.Prelude, though?

It's because the declarations in that module are in the root namespace.

If you're used to languages like Python, orthogonal namespace and module systems might be unfamiliar. This is like C++, Common Lisp, and and some others. It's convenient because libraries can add extensions into the name hierarchy.

Prefixing would be complicated. Remember that in each compiled module, the expressions have hard-coded references to fully-qualified constant names. All of these would need to be updated while importing, instead of mmaping the object files in, unless there were some sophisticated system to dynamically remap things. Or, all names would need to start with a module prefix, and then it would be up to name resolution to keep track of the mapping from module prefix to namespace prefix.

[Kyle Miller]

https://lean-reference-manual-review.netlify.app/The-Module-System/#module-system

[JJ]

Thanks! I'll read through that.

[JJ]

The decoupling of namespaces and modules is unintuitive to me, yeah. I would expect the second behavior you outlined to be how things work. In particular this sort of thing has always struck me as an issue with decoupling them:

-- Test/Foo.lean
namespace Bazinga
  def foo : Nat := 1
end Bazinga

-- Test/Bar.lean
namespace Bazinga
  def foo : Nat := 2
end Bazinga

-- Test.lean
import Test.Foo
import Test.Bar
-- import Test.Bar failed, environment already contains 'Bazinga.foo' from Test.Foo

#eval foo

But I suppose given I have not hit this issue yet before just now trying to explicitly trigger it might mean that it is not a problem in practice. Interesting.

[Kyle Miller]

The new module system currently lets you control whether imported modules are re-exported, and to control whether imports are for compile time or compile time and run time.

[JJ]

Very fancy!

[Kyle Miller]

That's certainly an issue, but we think that's a programmer error.

Using private declarations is a way to avoid collisions, for one-off auxiliary definitions you wouldn't use again.

[JJ]

I think I mostly share that view. I would be really interested to see how the new module system interacts with dynamic linking, tbh! Especially the comptime/runtime dependency split.

Also, my understanding is this sort of namespacing being tied to modules is important there, for coherence purposes, i.e. https://toot.cat/@Gankra/113522745584196985