Zulip Chat Archive

Stream: general

Topic: Naming our variables


view this post on Zulip Kenny Lau (Apr 06 2018 at 22:23):

For consistency, please change your upper case type names to α, β, γ etc.

https://github.com/leanprover/mathlib/pull/89#discussion_r179398893

view this post on Zulip Kenny Lau (Apr 06 2018 at 22:23):

@Kevin Buzzard :)

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 22:49):

I am skeptical about this approach being always the best idea. Rings are called R in mathematics, groups are called G and so on. Schemes are called S and their structure sheaves are called OS\mathcal{O}_S. They're all types.

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 22:49):

That was supposed to be a calliagraphic O

view this post on Zulip Kenny Lau (Apr 06 2018 at 22:49):

I triggered the right person :P

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 22:50):

My index sets are called things like alpha, beta, because they are just random types so I stick to the conventions.

view this post on Zulip Kenny Lau (Apr 06 2018 at 22:50):

what happened to iota

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 22:50):

But for readability isn't it better to have math objects called what mathematicians call them?

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 22:50):

i.e. depends on the typeclass

view this post on Zulip Simon Hudon (Apr 06 2018 at 23:21):

@Kevin Buzzard I'd be tempted to agree with you on groups and rings but I'm also hesitant to add any exception to style rules. The more exceptions there are, the harder they are to understand, enforce and agree to. I guess the next question is: what would be a good reason to create an exception?

view this post on Zulip Simon Hudon (Apr 06 2018 at 23:24):

Not answering my own question yet ... I can think of good reasons to not call type variables R or G. Being a ring or a group is not necessarily all that they are. If they conform to independent structures, which one should dictate the name?

view this post on Zulip Simon Hudon (Apr 06 2018 at 23:27):

I think the reason for naming them R or G is somewhat undermined by the fact that the information is already conveyed by [group α]

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 08:09):

I want to argue that mathematicians have solved these problems. I am currently writing a bunch of stuff about topological spaces and I call my topological spaces X and Y, because this is what mathematicians tend to call them, but if I had a topological ring I would call it R, because this is what mathematicians tend to call them. I would definitely never call any of them alpha.

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 08:10):

Given that many mathematical objects are types, it seems like a very strange rule to demand that they're all called alpha etc. Isn't this analogous to someone saying "OK so in this code, everything that is a variable needs to be called standard variable names like x,y,z etc"? [regardless of what they're doing]

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 08:10):

If we weren't using type class inference and things like groups, rings etc were their own specialised types then nobody would bat an eyelid if groups were all called G

view this post on Zulip Mario Carneiro (Apr 07 2018 at 08:13):

I think it is just like that though. For me, when writing lean code the "sort of thing" the type represents seems less important since it's not being directly associated to the notations and such like it is in math. (Instead, the typeclass parameters do all the heavy lifting here.) From what I can tell, the current convention is to use G H etc for Groups, but still to use greek letters for unbundled group-types.

view this post on Zulip Mario Carneiro (Apr 07 2018 at 08:14):

It's just that Group hasn't needed to play a big role (yet) in mathlib, so you don't see it much

view this post on Zulip Kenny Lau (Apr 07 2018 at 09:33):

@Kevin Buzzard what will happen if I call a group alpha and a ring beta in the m1p2 test?

view this post on Zulip Kenny Lau (Apr 07 2018 at 09:33):

I mean, alpha[beta] doesn’t look so bad as a group ring does it

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 09:34):

Just don't get me started.

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 09:34):

I'm trying to prove an affine scheme is a scheme

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 09:34):

Lean has notational irrelevance

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 09:34):

so notation is irrelevant

view this post on Zulip Kenny Lau (Apr 07 2018 at 09:36):

it’s my PR; of course i will get you started

view this post on Zulip Kenny Lau (Apr 07 2018 at 09:37):

let alpha be a real number... let beta be a sequence with limit to gamma

view this post on Zulip Mario Carneiro (Apr 07 2018 at 09:37):

now that's a bridge too far

view this post on Zulip Mario Carneiro (Apr 07 2018 at 09:38):

I kid, but in the lean convention only things of type Type are greek letters

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 09:50):

My gut instinct is to be completely happy with _restrictions_ of this form -- "we use alpha to be something of type Type so don't use it to be anything else"

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 09:50):

because mathematicians typically have more than one notation for things

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 09:50):

e.g. if you told me I couldn't use G for groups because mathlib conventions were that G was always for rings

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 09:50):

then I would just use H for groups

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 09:51):

so that sort of rule is easy to abide by


Last updated: May 14 2021 at 05:20 UTC