Undeclare variables

Stream: general

[Yaël Dillies]

Can we and how to undeclare variables? I'm working on data.equiv.basic where mostly {α β γ : Sort*} is used, but I have a series of lemmas that instead need {α β γ : Type*}.

[Kevin Buzzard]

AFAIK you just need to use new variables. One might argue that this would be good practice anyway so that the reader can see that the type has changed, except that the computer scientists seem to want to call every variable by the next available Greek letter and are happy to let the user guess whether alpha is a group or a linear order or something-which-might-be-a-Prop.

[Eric Wieser]

This doesn't seem to be possible, but certainly it would be nice if it was

[Eric Wieser]

Usually the approach is to have different sections when you want to reuse a name for something else

[Yaël Dillies]

Yeah of course. I just don't feel entitled to resection all of data.equiv.basic, but maybe I should.

[Mario Carneiro]

You can also shadow the variables in the statement itself, this is what I usually do (although you have to repeat any typeclass arguments; on the other hand this is useful for getting a different set of typeclass args as well)

[Yaël Dillies]

Yeah, and that's what's currently done. But it's annoyingly making the line slightly go over 100 chars, which is why I'm trying to pull them out in the first place.

[Yury G. Kudryashov]

You can split the file into 2 sections, one about Sort*, another about Type*.

[Eric Taucher]

Is undeclared variables the same idea as functional code with recursion where each call to the function is a push on the stack with new variables? If so then should there not be a library for such? This sounds a lot like monads.

Also in other programming languages when lines get long the use of term rewriting comes in handy to shorten the visible code (input for the term rewriter) but the rewritten code (output from the term rewriter) is still the really long lines one has to manually enter and is what is passed to the parser/compiler.

[Mac]

Kevin Buzzard said:

except that the computer scientists seem to want to call every variable by the next available Greek letter and are happy to let the user guess whether alpha is a group or a linear order or something-which-might-be-a-Prop.

Very true! :laughter_tears:

I suspect this may be due to clashing conventions. The convention is for types to be Greek letters in Lean, which I suspect is inherited from math, and math tends to use letters that have some historical and/or logical connection to the type/set/object in question. Computer scientists, on the other hand, tend to either use multi-character or multi-word names for meaningful type names or essentially meaningless capital letters like T, U, V (in alphabetic order) for generic types (e.g. fully polymorphic types like that of id). As Greek letters are generally unheard of in practical computer science, it is likely hard for such individuals to draw meaningful connections from such letters. Thus, I imagine users of that ilk tend to liken Lean's convention to the meaningless usage of the alphabetical T, U, V names in other languages than to meaningful symbols and thus name their variables accordingly. After all, if Greek letters are all just meaningless symbols to such a user, why not just use the next available one?

On the flip side, one place in the computer science oriented part of the Lean core where meaningful Greek letters are used is in monads (e.g., sigma for state and rho for read-only contexts).

[Kevin Buzzard]

Yes exactly. I noticed very early on that this greek letter convention was less than ideal for more "advanced" (if you want to call it that) mathematical files. There's things in maths called rings, and there are certain functions between rings called ring homomorphisms (maps that preserve the ring structure). There are special kinds of rings called fields, and there are certain theorems you can prove about ring homomorphisms between fields which are not true for general rings. In a gigantic mathlib file about ring homomorphisms, if every ring and field is called alpha, beta, gamma etc then this can get confusing to a mathematician, because they see some lemma about ring homomorphisms from alpha to beta and think "well this isn't true! What is going on!" and it turns out that 200 lines further up there's [field alpha] [field beta] variables, and the lemma is true for fields. The mathematical convention is that there are "ringy" variables such as R and A and B, and there are "fieldy" variables such as K and L (and of course there are "groupy" variables G, H, "topological space" variables X Y etc), and using these variable conventions in the more mathy parts of mathlib really helps with readability as far as mathematicians are concerned.