Zulip Chat Archive

Stream: maths

Topic: Renaming normed_group

Sebastien Gouezel (Jul 22 2022 at 07:41):

Currently, normed_group is a typeclass for an additive group with a norm. In the geometric group theory thread, the need for multiplicative groups with a norm came up naturally. Would anyone object if one renames normed_group to normed_add_group?

Yaël Dillies (Jul 22 2022 at 08:00):

And maybe even to normed_add_comm_group, given that in geometric group theory we are interested in the noncommutative setting.

Eric Wieser (Jul 22 2022 at 08:15):

If we're going to add noncommutative versions, is it time to change normed_group to not extend add_comm_group but rather take it as an argument?

Yaël Dillies (Jul 22 2022 at 08:16):

Yes, a mixin is starting to make sense here.

Eric Wieser (Jul 22 2022 at 08:17):

My intuition would be that we should

Rename normed_group to normed_add_group for now, to keep things short
Consider changing to a "mixin" at a later date, to support non-commutativity and additive monoids (nnreal)

Oliver Nash (Jul 22 2022 at 08:17):

I vote for renaming normed_group to normed_add_group (without adding the comm_) and leaving it at that. IIUC using a mixin may create performance issues for important paths through the typeclass hierarchy. Eric's comment arrived as I sent this.

Eric Wieser (Jul 22 2022 at 08:19):

Do we have any way to measure performance issues besides counting deterministic timeouts?

Oliver Nash (Jul 22 2022 at 08:20):

Me personally, no but I expect someone does.

Eric Wieser (Jul 22 2022 at 08:21):

I'd be very on board with Yaël attempting such a refactor (I've already done my time refactoring normed_space!), with the understanding that if performance sucks we might have to throw it away.

Eric Wieser (Jul 22 2022 at 08:21):

But not before we do the simple rename first

Yaël Dillies (Jul 22 2022 at 08:25):

#15619

Yaël Dillies (Jul 22 2022 at 08:27):

If you want, I'm happy to even turn normed_group into norm_add_group and seminormed_group into seminorm_add_group.

Yaël Dillies (Jul 22 2022 at 08:28):

I will fix line breaks once we are settled on this.

Sebastien Gouezel (Jul 22 2022 at 09:38):

I'd even go for normed_add_comm_group. But I agree that the mixin idea is probably bad performancewise.

Eric Wieser (Jul 22 2022 at 09:53):

Are you ambivalent as to whether the comm should be included?

Sebastien Gouezel (Jul 22 2022 at 09:58):

I would include the comm for the following reason. For performance, I'd keep the current definition (with whatever name we come up with, say X), and in parallel I'd introduce a class normed_group and its addivized version normed_add_group -- and then prove an instance from X to normed_add_group. This works fine and should minimize the refactor pain if the name we choose is different from normed_add_group:-)