## Stream: general

### Topic: hiding when import?

#### Zesen Qian (Jun 27 2018 at 20:45):

Hi, is there some way to hiding a name when importing a module?

#### Simon Hudon (Jun 27 2018 at 20:46):

You can do that on a namespace scale: open my_namespace hiding (clashing_def)

#### Simon Hudon (Jun 27 2018 at 20:46):

You can also do selective opening of namespaces

#### Zesen Qian (Jun 27 2018 at 20:47):

thank you, I'm still new to the name space space. But what if a name is at the top level of a module?

#### Zesen Qian (Jun 27 2018 at 20:47):

or module itself is a namespace?

#### Simon Hudon (Jun 27 2018 at 20:49):

The top most namespace is called _root_. Anything in that namespace can be hard to deal with. I'm not sure what the best approach is for dealing with name clashes in the root namespace. The best advice I have is: avoid

#### Simon Hudon (Jun 27 2018 at 20:50):

A module itself is not a namespace. It would be interesting if it was though. Maybe we can request that feature

#### Zesen Qian (Jun 27 2018 at 20:52):

OK, maybe I'm wrong, but it seems that parser in data.buffer.parser is at top level.

#### Zesen Qian (Jun 27 2018 at 20:52):

I guess that means this name will be there for all modules recursively importing it,

#### Zesen Qian (Jun 27 2018 at 20:53):

and there is no way to hide it?

#### Mario Carneiro (Jun 27 2018 at 20:53):

hide in what sense?

#### Mario Carneiro (Jun 27 2018 at 20:53):

do you want to name something else parser at the top level?

#### Zesen Qian (Jun 27 2018 at 20:54):

A import B, B has a top level name which clashes with a name A wants to use.

#### Zesen Qian (Jun 27 2018 at 20:54):

@Mario Carneiro exactly.

#### Mario Carneiro (Jun 27 2018 at 20:54):

that's bad, avoid it

#### Mario Carneiro (Jun 27 2018 at 20:55):

hide does not change actual names, this will cause a name conflict

#### Zesen Qian (Jun 27 2018 at 20:55):

maybe we should ask the author of standard library to avoid it first.

#### Zesen Qian (Jun 27 2018 at 20:55):

then we can ask the users to avoid it too.

#### Mario Carneiro (Jun 27 2018 at 20:55):

sadly the core lib is frozen

#### Mario Carneiro (Jun 27 2018 at 20:56):

so you will have to work around it

#### Mario Carneiro (Jun 27 2018 at 20:56):

but it's a global coordination problem, it's not a problem until someone else wants the name

#### Simon Hudon (Jun 27 2018 at 20:56):

If you define your own parser in your local namespace, doesn't that make it the default definition that will be used as parser?

#### Mario Carneiro (Jun 27 2018 at 20:57):

yes, that will work fine

#### Mario Carneiro (Jun 27 2018 at 20:57):

but it means you can never define _root_.parser

#### Mario Carneiro (Jun 27 2018 at 20:57):

since it's been defined already

Right

#### Zesen Qian (Jun 27 2018 at 20:58):

to solve it once and for all, we need qualified import, like in haskell.

#### Mario Carneiro (Jun 27 2018 at 20:58):

The moral of the story is that you should define most of your stuff in your own namespace

#### Zesen Qian (Jun 27 2018 at 20:58):

so you can rename a namespace/module

#### Mario Carneiro (Jun 27 2018 at 20:58):

that way core or mathlib can't get in your way

#### Zesen Qian (Jun 27 2018 at 20:58):

well again, I don't see the std lib doing it, so I don't feel obligated to do it either.

#### Mario Carneiro (Jun 27 2018 at 20:58):

you aren't stdlib

#### Zesen Qian (Jun 27 2018 at 20:59):

why his parser is more fundenmental than mine?

#### Simon Hudon (Jun 27 2018 at 20:59):

I think if we could have a qualification to a module like import data.buffer.parser within buffer as a way of putting all the definitions directly in the parser module in a new buffer namespace, that might help manage this situation

#### Mario Carneiro (Jun 27 2018 at 20:59):

To be fair, I agree that that parser definition should be in the buffer namespace, but in general corelib will take lots of top level names

#### Reid Barton (Jun 27 2018 at 20:59):

Unlike in Haskell, though, modules and namespaces are orthogonal in Lean. A module might define names in many namespaces and many modules might define names in the same namespace. So renaming a module doesn't make a lot of sense, in general.

#### Zesen Qian (Jun 27 2018 at 20:59):

@Simon Hudon that's the "qualified import" I was talking about.

#### Simon Hudon (Jun 27 2018 at 21:00):

That would be a bit different from Haskell though. In Haskell, qualified is a form of renaming

#### Zesen Qian (Jun 27 2018 at 21:01):

@Reid Barton how about this: import A as B. then the top-level def. foo in A becomes B.foo, ns.foo becomes B.ns.foo.

#### Mario Carneiro (Jun 27 2018 at 21:01):

and then you define a top level def?

#### Mario Carneiro (Jun 27 2018 at 21:01):

because then what happens to files C importing A?

#### Zesen Qian (Jun 27 2018 at 21:01):

yes, I'm the king.

#### Mario Carneiro (Jun 27 2018 at 21:02):

Or worse, a file C that imports A and B?

#### Zesen Qian (Jun 27 2018 at 21:02):

it might conflict with the current semantics of import in lean.

it sure does

#### Zesen Qian (Jun 27 2018 at 21:03):

but since lean always break old stuffs, I see that as a good thing.

#### Mario Carneiro (Jun 27 2018 at 21:03):

I mean, what's your solution?

#### Mario Carneiro (Jun 27 2018 at 21:04):

if A has foo, B imports A as A and also defines foo, and C imports A and B, what happens?

#### Reid Barton (Jun 27 2018 at 21:04):

there's also the type-directed . notation to worry about

#### Simon Hudon (Jun 27 2018 at 21:05):

I think like in Haskell, the qualification must only be local

#### Zesen Qian (Jun 27 2018 at 21:06):

a practical solution would need thorough consideration of all factors, esp. the ability of .olean format.

#### Zesen Qian (Jun 27 2018 at 21:06):

but I would naively believe there must be a better way.

#### Reid Barton (Jun 27 2018 at 21:08):

A bigger annoyance IMO is that after you have given up and put your own parser name inside your own namespace, Lean will still consider _root_.parser to be a possible overload for parser (as far as I know?)

#### Mario Carneiro (Jun 27 2018 at 21:09):

Not inside your namespace

#### Mario Carneiro (Jun 27 2018 at 21:10):

and if it gives you trouble you can always make parser a local notation

#### Mario Carneiro (Jun 27 2018 at 21:10):

that will clobber any overloads

#### Reid Barton (Jun 27 2018 at 21:10):

hmm I feel like I've had trouble with this before... but can't recall the details. Maybe inside tactic mode?

#### Reid Barton (Jun 27 2018 at 21:10):

And yeah, I used local notation to work around it

Last updated: May 17 2021 at 22:15 UTC