Zulip Chat Archive

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

Simon Hudon (Jun 27 2018 at 20:57):

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.

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

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: Dec 20 2023 at 11:08 UTC