Zulip Chat Archive

Stream: general

Topic: hiding when import?


view this post on Zulip Zesen Qian (Jun 27 2018 at 20:45):

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

view this post on Zulip Simon Hudon (Jun 27 2018 at 20:46):

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

view this post on Zulip Simon Hudon (Jun 27 2018 at 20:46):

You can also do selective opening of namespaces

view this post on Zulip 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?

view this post on Zulip Zesen Qian (Jun 27 2018 at 20:47):

or module itself is a namespace?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Zesen Qian (Jun 27 2018 at 20:52):

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

view this post on Zulip Zesen Qian (Jun 27 2018 at 20:53):

and there is no way to hide it?

view this post on Zulip Mario Carneiro (Jun 27 2018 at 20:53):

hide in what sense?

view this post on Zulip Mario Carneiro (Jun 27 2018 at 20:53):

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

view this post on Zulip 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.

view this post on Zulip Zesen Qian (Jun 27 2018 at 20:54):

@Mario Carneiro exactly.

view this post on Zulip Mario Carneiro (Jun 27 2018 at 20:54):

that's bad, avoid it

view this post on Zulip Mario Carneiro (Jun 27 2018 at 20:55):

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

view this post on Zulip Zesen Qian (Jun 27 2018 at 20:55):

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

view this post on Zulip Zesen Qian (Jun 27 2018 at 20:55):

then we can ask the users to avoid it too.

view this post on Zulip Mario Carneiro (Jun 27 2018 at 20:55):

sadly the core lib is frozen

view this post on Zulip Mario Carneiro (Jun 27 2018 at 20:56):

so you will have to work around it

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 27 2018 at 20:57):

yes, that will work fine

view this post on Zulip Mario Carneiro (Jun 27 2018 at 20:57):

but it means you can never define _root_.parser

view this post on Zulip Mario Carneiro (Jun 27 2018 at 20:57):

since it's been defined already

view this post on Zulip Simon Hudon (Jun 27 2018 at 20:57):

Right

view this post on Zulip Zesen Qian (Jun 27 2018 at 20:58):

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

view this post on Zulip 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

view this post on Zulip Zesen Qian (Jun 27 2018 at 20:58):

so you can rename a namespace/module

view this post on Zulip Mario Carneiro (Jun 27 2018 at 20:58):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 27 2018 at 20:58):

you aren't stdlib

view this post on Zulip Zesen Qian (Jun 27 2018 at 20:59):

why his parser is more fundenmental than mine?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Zesen Qian (Jun 27 2018 at 20:59):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 27 2018 at 21:01):

and then you define a top level def?

view this post on Zulip Mario Carneiro (Jun 27 2018 at 21:01):

because then what happens to files C importing A?

view this post on Zulip Zesen Qian (Jun 27 2018 at 21:01):

yes, I'm the king.

view this post on Zulip Mario Carneiro (Jun 27 2018 at 21:02):

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

view this post on Zulip Zesen Qian (Jun 27 2018 at 21:02):

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

view this post on Zulip Mario Carneiro (Jun 27 2018 at 21:03):

it sure does

view this post on Zulip Zesen Qian (Jun 27 2018 at 21:03):

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

view this post on Zulip Mario Carneiro (Jun 27 2018 at 21:03):

I mean, what's your solution?

view this post on Zulip 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?

view this post on Zulip Reid Barton (Jun 27 2018 at 21:04):

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

view this post on Zulip Simon Hudon (Jun 27 2018 at 21:05):

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

view this post on Zulip Zesen Qian (Jun 27 2018 at 21:06):

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

view this post on Zulip Zesen Qian (Jun 27 2018 at 21:06):

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

view this post on Zulip 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?)

view this post on Zulip Mario Carneiro (Jun 27 2018 at 21:09):

Not inside your namespace

view this post on Zulip Mario Carneiro (Jun 27 2018 at 21:10):

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

view this post on Zulip Mario Carneiro (Jun 27 2018 at 21:10):

that will clobber any overloads

view this post on Zulip 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?

view this post on Zulip 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