hiding when import?

Stream: general

[Zesen Qian]

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

[Simon Hudon]

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

[Simon Hudon]

You can also do selective opening of namespaces

[Zesen Qian]

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]

or module itself is a namespace?

[Simon Hudon]

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]

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

[Zesen Qian]

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

[Zesen Qian]

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

[Zesen Qian]

and there is no way to hide it?

[Mario Carneiro]

hide in what sense?

[Mario Carneiro]

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

[Zesen Qian]

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

[Zesen Qian]

@Mario Carneiro exactly.

[Mario Carneiro]

that's bad, avoid it

[Mario Carneiro]

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

[Zesen Qian]

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

[Zesen Qian]

then we can ask the users to avoid it too.

[Mario Carneiro]

sadly the core lib is frozen

[Mario Carneiro]

so you will have to work around it

[Mario Carneiro]

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

[Simon Hudon]

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]

yes, that will work fine

[Mario Carneiro]

but it means you can never define _root_.parser

[Mario Carneiro]

since it's been defined already

[Simon Hudon]

Right

[Zesen Qian]

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

[Mario Carneiro]

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

[Zesen Qian]

so you can rename a namespace/module

[Mario Carneiro]

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

[Zesen Qian]

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

[Mario Carneiro]

you aren't stdlib

[Zesen Qian]

why his parser is more fundenmental than mine?

[Simon Hudon]

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]

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]

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]

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

[Simon Hudon]

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

[Zesen Qian]

@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]

and then you define a top level def?

[Mario Carneiro]

because then what happens to files C importing A?

[Zesen Qian]

yes, I'm the king.

[Mario Carneiro]

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

[Zesen Qian]

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

[Mario Carneiro]

it sure does

[Zesen Qian]

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

[Mario Carneiro]

I mean, what's your solution?

[Mario Carneiro]

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

[Reid Barton]

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

[Simon Hudon]

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

[Zesen Qian]

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

[Zesen Qian]

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

[Reid Barton]

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]

Not inside your namespace

[Mario Carneiro]

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

[Mario Carneiro]

that will clobber any overloads

[Reid Barton]

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

[Reid Barton]

And yeah, I used local notation to work around it