Naming our variables

Stream: general

[Kenny Lau]

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

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

[Kenny Lau]

@Kevin Buzzard :)

[Kevin Buzzard]

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 $\mathcal{O}_S$. They're all types.

[Kevin Buzzard]

That was supposed to be a calliagraphic O

[Kenny Lau]

I triggered the right person :P

[Kevin Buzzard]

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

[Kenny Lau]

what happened to iota

[Kevin Buzzard]

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

[Kevin Buzzard]

i.e. depends on the typeclass

[Simon Hudon]

@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?

[Simon Hudon]

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?

[Simon Hudon]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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]

[Kevin Buzzard]

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

[Mario Carneiro]

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.

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kevin Buzzard]

Just don't get me started.

[Kevin Buzzard]

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

[Kevin Buzzard]

Lean has notational irrelevance

[Kevin Buzzard]

so notation is irrelevant

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

now that's a bridge too far

[Mario Carneiro]

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

[Kevin Buzzard]

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"

[Kevin Buzzard]

because mathematicians typically have more than one notation for things

[Kevin Buzzard]

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

[Kevin Buzzard]

then I would just use H for groups

[Kevin Buzzard]

so that sort of rule is easy to abide by