Unexpected overloading with export command

Stream: lean4

[François G. Dorais]

I was a bit surprised that the following shows two definitions for rfl instead of some kind of error message.

class Reflexivity {α} (r : α → α → Prop) : Prop where refl : (x : α) → r x x

abbrev Reflexivity.rfl {α r x} := @Reflexivity.refl α r x

export Reflexivity (refl rfl)

#print rfl

But #check rfl does give an error:

Dev/Relations.lean:11:7: error: ambiguous, possible interpretations
rfl
rfl

I would expect an error at the export but maybe there is something deeper going on.

[Mario Carneiro]

That works also in lean 3

[Mario Carneiro]

When you have open namespaces you can get into a situation where a name is overloaded; this will cause an error if you try to use it

[Mario Carneiro]

def A.foo := 1
def B.foo := 2
open A B
#check foo
-- ambiguous overload, possible interpretations
--   B.foo
--   A.foo

[Mario Carneiro]

an export is just a global open

[François G. Dorais]

Oh, I see. So export works as a global open.

[François G. Dorais]

(As opposed to a new declaration.)

[François G. Dorais]

That's not what I expected. I think I'll avoid exports from now on. Nobody should have that much power!

[Mario Carneiro]

Yes, I don't think it's used in mathlib at all, and the few uses in core are for things like option.some

[Mario Carneiro]

usually we just put things in the root namespace if we want them to be used without a qualifier in all contexts

[Mario Carneiro]

I guess you can't do that for constructors of a data type like option though

[François G. Dorais]

Wouldn't an abbreviation work just as well?

[Mario Carneiro]

As you observed, an export is not the same as an abbreviation, the latter creates a new definition, meaning that tactics and so on see a different term and can do different things

[François G. Dorais]

I think I would prefer a new definition, but that's just my personal opinion. I'm happy writing a bunch of abbreviations instead of exports. And I could probably write a macro to automate this if necessary... (Lean 4 macros rock!)

[Mario Carneiro]

I just feel bad for the kernel sometimes, seeing and typechecking all these useless definitions that are equal to other named things

[Mario Carneiro]

I prefer parser-only abbreviations, which you can mostly get via notation and macros

[François G. Dorais]

Good point but the kernel doesn't feel anything... though _you_ could feel your cpu overheating. :smiley: Thanks for the help Mario!

[Kyle Miller]

I think what open and export do specifically is something like the following. At any given moment you have a list of known symbols along with a current namespace.

• open foo takes all the names in the foo namespace and adds them to the list of known symbols. This way you can reference those symbols without qualifying them with foo
• export foo (symbols...) does open foo (symbols...) and also adds all those symbols to the current namespace. The effect is that whoever then later opens or exports this namespace will get those symbols. (And if it's at the top level, everyone gets them!)

For example, the export below essentially creates a symbol foo.x. You still have to open foo if you're not in the foo namespace to have an x that stands for foo.bar.x.

namespace foo

structure bar where
    x : Nat
export bar (x)

end foo

It can be useful when you want to curate a namespace.

[Sebastian Ullrich]

open foo takes all the names in the foo namespace and adds them to the list of known symbols. This way you can reference those symbols without qualifying them with foo

Not quite; this is how Lean 3 worked, but in Lean 4, open makes symbols available that haven been declared in the namespace even after the open command.

[Kyle Miller]

What I said ends up being incorrect for Lean 3 as well -- I thought I had tested it before, but it seems that export only makes symbols available when you later re-enter or open the namespace. That's to say, in the Lean 3 version of that code the export does not imply the existence of a foo.x.

(Something I've been wondering is where the idea for Lean's namespaces might have come from. They are very similar to Common Lisp's symbol packages, simplified for the better, but I could imagine they might also have come from an Algol/Pascal-syntax version of Agda modules, especially with there being parameter variables.)