Automatic attribute localization

Stream: general

[Yaël Dillies]

Would it be possible/desirable to have a tag on ìnstance declarations to make it a def with the instance attribute in the specified locale? Something like

@[locale foo]
instance : bar baz := sorry

--same as

/-- Blabla I'm required to write a docstring because this is technically not an instance. -/
def baz.bar : bar baz := sorry

localized "attribute [instance] baz.bar" in foo

Of course, it doesn't have to be restricted to instance, that's just the most obviously useful example. We could make it support any attribute, kind of like derive.

[Yaël Dillies]

I'm working on the instances in file#algebra/pointwise and managing the manual attribute declarations is slightly more bookkeeping than I can bear. With added pain because of to_additive.

[Yaël Dillies]

One advantage I see is that declaring instances in locales will more closely resemble declaring instances globally, meaning that it might nudge people into using locales more.

[Kyle Miller]

I wonder if we can backport the scoped instance feature from Lean 4 to Lean 3. This ties the instance to a particular namespace, and then when you open the namespace it becomes available.

[Kyle Miller]

I looked into what it would take to support scoped instances in Lean 3, if it's something we wanted. A simplish implementation might be:

• introduce a scoped_instance attribute
• when the scoped_instance attribute is present when defining an instance, prevent the definition command from adding the instance attribute and (not sure how exactly) have it add instance as a local attribute
• modify the namespace and open commands to find definitions with the scoped_instance in the relevant namespace and locally give them the instance attribute.

@Yaël Dillies's example would then look like

namespace foo
@[scoped_instance]
instance : bar baz := sorry
end foo

Then for mathport, I think this would be translated to

namespace foo
scoped instance : bar baz := sorry
end foo

[Yaël Dillies]

We don't want definitions to be attached to a namespace though. People might want to speak about pointwise operations without opening set, finset, submodule, etc... and reciprocally people might want to work on set without being polluted with the pointwise operations.

[Kyle Miller]

I forgot to mention something nonobvious -- you can put your instances in, say, the set.extra_instances namespace

[Kyle Miller]

And then open set.extra_instances to get the scoped instances.

[Kyle Miller]

Whatever the solution, getting the locale attribute to work on an instance will involve modifying Lean, and I figure it'd be better to backport Lean 4 features to make things easier for mathport.

[Yaël Dillies]

That only addresses the second part of my rebutal. I still don't know how that will make it possible to work with pointwise operations on more complicated objects without opening the namespaces of all simple ones.

[Kyle Miller]

Doesn't that rebuttal also apply to your original proposal?

[Yaël Dillies]

No, because all instances are still put in one single pointwise locale. Or several if you want. The point is that you have the choice.

[Yaël Dillies]

In general, overloading namespaces with such functionalities means losing in flexibility.

[Kyle Miller]

Then you better let Leo know that scoped is a bad idea :smile:

[Yaël Dillies]

Oh yeah my criticism is not much about you backporting scoped than about scoped itself. If scoped wasn't interfering with namespaces but instead let you decide which locale to dump stuff into, I'd be happy!

[Kyle Miller]

What's preventing you from putting things into the pointwise namespace?

[Kyle Miller]

You have the freedom to do that.

[Yaël Dillies]

That still mixes up worlds...

[Kyle Miller]

There's scoped notation too in Lean 4. I'm pretty sure localized will eventually be phased out.

[Kyle Miller]

We'll probably have open big_operators instead of open_locale big_operators for example.

[Kyle Miller]

Or maybe open locale.big_operators, who knows.

[Yaël Dillies]

I really liked locales...

[Kevin Buzzard]

They were confusing for users. If I import big_operators then of course I want to open_locale big_operators.

[Yaël Dillies]

You will have to open big_operators instead. Is that really more user friendly?

[Kevin Buzzard]

Yes it is, because the students already know about open.

[Eric Wieser]

If you call the namespace locale.pointwise then you can write open locale.pointwise if you really want to