Re: if vs. when vs. and: style question

[Stefan Monnier]

> What is α?  What is β?

> Wouldn't have it been better to name those variables number-of-rows
> or tree-height or some other words denoting their actual meaning?

Usually, within the context where the mathematical formula is used,
these variables *are* names denoting their meaning.  These depend on
notational conventions used within specific communities (and usually not
formalized), but they are convenient.  So instead of

    has_type env exp type

you say

    Γ ⊢ e : τ

and it is just as explicit, because τ does mean "a type", and Γ means "a
type environment", and ":" means "has type", and "⊢" means "based on
hypotheses such and such".  Some of those letters/signs have meaning
shared within a fairly large mathematical community while others are
much more specific to a specialized subfield.

Of course, if you're not familiar with the local conventions, it looks
like line noise, but otherwise it offers people much higher concision,
so they can focus on the important aspects.


        Stefan