Zulip Chat Archive

Stream: general

Topic: Notation and namespace

Kevin Buzzard (Jul 01 2021 at 12:54):

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 (Jul 01 2021 at 13:02):

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 (Jul 01 2021 at 13:41):

How is src#additive.of_mul currently implemented?

Eric Wieser (Jul 01 2021 at 13:42):

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

Eric Wieser (Jul 01 2021 at 13:44):

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 (Jul 01 2021 at 14:48):

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

Yakov Pechersky (Jul 01 2021 at 14:51):

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 (Jul 01 2021 at 14:54):

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 (Jul 01 2021 at 14:55):

And then use abbreviations for typeclass_id

Eric Wieser (Jul 01 2021 at 14:56):

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 (Jul 01 2021 at 14:57):

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

Eric Wieser (Jul 01 2021 at 14:57):

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

Eric Wieser (Jul 01 2021 at 14:58):

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 (Jul 02 2021 at 05:46):

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 (Jul 02 2021 at 05:51):

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 (Jul 02 2021 at 05:52):

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

Eric Wieser (Jul 02 2021 at 05:52):

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

Last updated: Aug 03 2023 at 10:10 UTC