Notation and namespace

Stream: general

[Kevin Buzzard]

notation `additive` := id -- this might be fun to experiment with

but I can't experiment with it because I am not allowed an additive namespace now so all the code breaks. Is dot notation extensively used by the additive fans? My current thoughts on additive are that it should be tagged @[canonical]. I was wondering if we could make id do the work of equiv somehow.

[Kevin Buzzard]

abbreviation additive := @id

abbreviation multiplicative := @id

def additive.of_mul : α ≃ additive α := equiv.refl α

def additive.to_mul : additive α ≃ α := equiv.refl α

is another interesting opening

[Eric Wieser]

How is src#additive.of_mul currently implemented?

[Eric Wieser]

I think using id is probably identical providing src#id is reducible id isn't reducible so that version may cause trouble

[Eric Wieser]

notation `additive` := id is definitely a bad idea though, because that means to typeclass inference additive x and multiplicative x are the same thing which seems very wrong

[Kevin Buzzard]

They are the same thing though? They're just alpha

[Yakov Pechersky]

Yes, but the non-abbreviation def approach makes a type alias that TC inference does not see though. But TC does see through abbreviation. IIUC

[Kevin Buzzard]

Does the kernel have any special support for id, or can I just define typeclass_id by copying the definition of id and making it a typeclass

[Kevin Buzzard]

And then use abbreviations for typeclass_id

[Eric Wieser]

I don't understand that question - are you asking about writing instance : id (group A) or instance : group (id A)? Only the former is "making id a typeclass", the latter is "associating an instance with id A which is considered a different type to A by typeclass search".

[Eric Wieser]

Today's definition of multiplicative and additive are both semireducible meaning typeclass search cannot see through them

[Eric Wieser]

Your := @id version probably behaves the same way, but is more work for the elaborator

[Eric Wieser]

Your notation version is the most reducible something can be, and typeclass resolution would see right through it makeing multiplicative and additive indistinguishable

[Kevin Buzzard]

I had this vision where using id instead of additive would somehow be perfect because you could leave it there if you wanted the elaborator not to see through it but simplify it away whenever you needed to. It still sort of sounds appealing but I don't really know how you keep the ids there iff you want them there

[Eric Wieser]

I mean whatever you can do with id you can do with additive already, I don't think there's anything special about id that distinguishes it from other identity functions

[Eric Wieser]

src#id is pretty much the same as src#additive

[Eric Wieser]

Oh, also using def additive := @id permits nonsense like additive 1