Zulip Chat Archive

Stream: maths

Topic: Set intervals names


Yaël Dillies (Dec 28 2022 at 12:41):

What do people think of renaming docs#set.interval and docs#set.interval_oc to set.uIcc and set.uIco, with the u standing for "unordered"? This would:

  • fix the unanimously bad name interval_oc
  • make set.interval look closer to docs#set.Icc than it currently is
  • shorten the names
  • match the naming convention I introduced (a while back!) with docs#set.cIcc
  • make clear that we don't have the Ioc and Ioo versions (which would then be called uIoc, uIoo
  • avoid confusion with docs#interval

Yaël Dillies (Dec 28 2022 at 12:43):

The one downside I see so far is that uIcc is a more obscure name than interval, but

  • interval could (and indeed does) refer to many similar concepts
  • the Ixx naming convention is already well-implemented.

Yaël Dillies (Dec 28 2022 at 12:44):

This is relevant to the mathlib4 port: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20clarification/near/315915143 and https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60interval_oc.60.20naming.20scheme

Kevin Buzzard (Dec 28 2022 at 13:19):

What's wrong with just set.Icc etc?

Reid Barton (Dec 28 2022 at 13:26):

set.interval isn't set.Icc

Ruben Van de Velde (Dec 28 2022 at 13:26):

It's [min a b, max a b], yes?

Kevin Buzzard (Dec 28 2022 at 13:28):

Why?

Kevin Buzzard (Dec 28 2022 at 13:29):

Maybe that's the wrong question. Maybe the question is why what we have is called an interval at all? Is this standard terminology?

Kevin Buzzard (Dec 28 2022 at 13:30):

I think Yael's convention sounds great, an incomprehensible name for an incomprehensible construction sounds perfect.

Kevin Buzzard (Dec 28 2022 at 13:32):

I'd also vote for changing the docstring of set.interval_oc to something which actually describes the object being defined

Reid Barton (Dec 28 2022 at 13:38):

I think "incomprehensible" is a bit too far but in general I agree it looks like a good change.

Kevin Buzzard (Dec 28 2022 at 13:41):

So you're happy that {2} and {1,2,3} are in the interval between {1,2} and {2,3}, given the description "interval a b is the set of elements lying between a and b, with a and b included"?

Kevin Buzzard (Dec 28 2022 at 13:42):

Surely "the set of elements lying between a and b" is {x : a<=x<=b}?

Reid Barton (Dec 28 2022 at 13:43):

I mean this is just too much generality gone awry

Reid Barton (Dec 28 2022 at 13:43):

It's clearly a sensible construction in the case of, say, the real numbers

Kevin Buzzard (Dec 28 2022 at 13:43):

Anyway, to answer the question I am definitely for the change :-)

Kevin Buzzard (Dec 28 2022 at 13:44):

Oh I see, the point is that it allows us to talk about the interval from 10 to 1. It could still have been the union of [a,b] and [b,a] but whatever.

Kevin Buzzard (Dec 28 2022 at 13:45):

For linear orders these agree and you can argue that everything else is a junk value

Yaël Dillies (Dec 28 2022 at 14:39):

Reid Barton said:

I mean this is just too much generality gone awry

Well in fact I very recently generalised set.interval to lattices because I need this generality for a combinatorial inequality :sweat_smile: but it has nothing to do with the current discussion.

Pedro Sánchez Terraf (Dec 28 2022 at 16:52):

Kevin Buzzard said:

So you're happy that {2} and {1,2,3} are in the interval between {1,2} and {2,3}, given the description "interval a b is the set of elements lying between a and b, with a and b included"?

Even from the (order) lattice-theoretic point of view I share this concern. The name interval for this construct is misleading. It is more like a “hull” (actually being the sublattice generated by those two elements).

Yaël Dillies (Dec 28 2022 at 23:34):

The world \ {me} only cares about the linear order case, so this is a deliberate lie from the docstring.

Yaël Dillies (Jan 08 2023 at 23:53):

#18104 (it will probably be a while before it builds)

David Loeffler (Jan 09 2023 at 08:11):

The build is broken for #18104 (looks like a search-and-replace over the library caught something it shouldn't).

David Loeffler (Jan 09 2023 at 08:15):

Incidentally, this change will break basically any pre-existing code that uses definite integrals (e.g. my Riemann zeta function project), all for a purely aesthetic gain. Whatever happened to "if it ain't broke don't fix it"?

Yaël Dillies (Jan 09 2023 at 08:23):

My thought is that it shouldn't break so much because we have notation for it. Are you really not using the [a, b] notation?

Johan Commelin (Jan 09 2023 at 08:24):

You are also change a bunch of lemma names, right?

Yaël Dillies (Jan 09 2023 at 08:24):

Yes, that is unavoidable if we want to keep consistency :sad:

Johan Commelin (Jan 09 2023 at 08:25):

Sure, but it means that using the notation isn't going to avoid breakage.

Johan Commelin (Jan 09 2023 at 08:25):

I'm really looking forward to using alias + deprecated for these kind of situations, once we've moved to Lean 4.

Yaël Dillies (Jan 09 2023 at 08:26):

Most of the existing code around interval integrals only uses the notation, thankfully.

Yaël Dillies (Jan 09 2023 at 08:28):

But yeah whatever is not in mathlib is hardly ever considered when mathlib moves on, which is why if you want to reduce your maintenance burden you should PR your code to mathlib.

David Loeffler (Jan 09 2023 at 08:39):

There was a thread recently about differences between mathlib and one of its rivals (Coq?), in which some people tried to argue against the claim that mathlib had a casual approach to backward-compatibility issues. I think this thread here demonstrates that casual attitude rather neatly.

Alex J. Best (Jan 09 2023 at 09:16):

I'm not sure how one would argue mathlib respects backwards compatibility! It definitely doesn't of course, most people here seem to consider the fact we readily revise previous work that isn't sufficient for some reason as a good thing. Maybe they tried to argue it doesn't matter for some reason (all dependents fix a version)?
There are definitely a lot more things we can do to at least help people switch mathlib versions more easily (https://mathlib-changelog.org/ is a good start), but currently adjusting mathlib induced breakage is still quite manual process.

Eric Wieser (Jan 09 2023 at 09:23):

David Loeffler said:

some people tried to argue against the claim that mathlib had a casual approach to backward-compatibility issues.

From my perspective, it's not that our approach is casual; it's that as a community, we have made a deliberate choice that backwards compatibility (in a software sense) is a non-goal.

I think we still try to remain mathematically backwards-compatible; a mathematical idea usually doesn't disappear from mathlib entirely.

Yaël Dillies (Jan 09 2023 at 10:07):

In particular, name changes are not backward-compatible, but in a trivial way. Once you've replaced the modified names, you're guaranteed that your work will still compile.

Eric Wieser (Jan 09 2023 at 11:21):

Well, unless the statement changes too. Your comments amounts to "changes are incompatible in name only, except when they're not"

Yaël Dillies (Jan 09 2023 at 11:21):

What I mean is that there's no work trying to fit new definitions.

Eric Wieser (Jan 12 2023 at 00:28):

Yaël Dillies said:

What do people think of renaming docs#set.interval and docs#set.interval_oc to set.uIcc and set.uIco, with the u standing for "unordered"?

This thread took multiple tangents above, and I think to some extent the question of naming got lost. #18104, which performs this rename, is now passing CI. Were people generally happy with the new names?

David Loeffler (Jan 12 2023 at 08:58):

If there has to be a new name, then this seems a good choice.

Eric Wieser (Jan 12 2023 at 12:00):

Pinging the people who approved/contributed the old names @Sebastien Gouezel and @Yury G. Kudryashov (interval in #1949), @Patrick Massot (interval_oc in #7864); are you happy with these new names?

Sebastien Gouezel (Jan 12 2023 at 12:00):

Yes, I think the new names are better.

Patrick Massot (Jan 12 2023 at 15:34):

Yes, I already wrote somewhere that I'm ok with the renaming.

Eric Wieser (Jan 12 2023 at 16:53):

:merge:


Last updated: Dec 20 2023 at 11:08 UTC