Comment by klibertp
5 years ago
> As a programmer, you know first hand that repeating oneself is bad practice
Yes, but we're talking about the syntax/notation here, not the underlying concepts. I see it like this: imagine a function which has a single argument, in a dynamic language so that we have no type annotation. Let's say I named the argument "pair_of_ints". Following your logic, I should have named it "i2" instead, because then I wouldn't have to repeat myself by writing all the p,a,r,o,f,n,t,s characters all over the function!
Another way of saying this: yes, it's good to encapsulate pieces of logic in subroutines/functions/methods/etc. It's not good, however, to name the functions (let's add: in global scope) f, g, h, f2, f3, gh, etc. just to avoid typing more characters. Instead, we choose a name which can be understood with as little additional context as possible.
> having vocabulary to embody reccuring ideas helps us discuss complex ideas more easily.
Yes. My problem is when all the entries in the vocabulary are one (Unicode) character long.
> I guess you would want these characters, like Gamma (Γ), Delta (Δ), tau (τ) or sigma (σ) to be replaced by their ascii equivalent (eg. G, D, t, s), or perhaps even more evocative names?
The latter, preferably. If something is meant to denote a context, I see little reason to name it "Γ" instead of, I don't know, "context"?
> But even if this would be done, you'd still have to understand the underlying concepts they represent, such as the typechecking context which is usually represented by Gamma.
Yes, but then I wouldn't need to work to understand the syntax, making the process of understanding the concepts easier.
> It's not good, however, to name the functions (let's add: in global scope) f, g, h, f2, f3, gh, etc. just to avoid typing more characters. Instead, we choose a name which can be understood with as little additional context as possible.
Ah, you're not talking about the same things: you speak code, he speaks type theory.
You are completely correct on that: a good naming convention is better for readability, particularly with a large codebase.
So, let's try to find a compromise. It really depends on the size of the lexicon in the language considered: if all you have is 50 rules in your type theory, do you really need to give each of them a name fully describing its semantics? Of course you don't, so calling them inl1, sub2 etc. shouldn't be an issue, if the name can still act as a reminder of the rule meaning. In the same spirit, rules usually connect together few objects: a context, at most half a dozen of type variables which come up all the time in the rule set, a few operators. Maybe someone with some experience with functional programming would find it easier to understand. In fact, I think I pretty much paraphrased the quote above.
> Yes, but then I wouldn't need to work to understand the syntax, making the process of understanding the concepts easier.
I very much agree with that, but I also think that it's a question of training. In software engineering, people routinely devise DSLs, learn new languages to handle a specific problem or adapt to new working conditions. Once you get the hang of it, it should become easier.
Here's a small tip: Gamma in the greek alphabet corresponds to the letter C in the Roman one, so it sort of makes sense, if one's using Greek letters, to use Gamma for Context - like one would use Delta for difference in math, for instance. It's confusing at first, but it might also help in learning the Greek alphabet - again, same as what we have to go through in math classes.
This discussion reminds me of the style guide for a Coq PL formalization project:
> No unicode or infix operators for judgement forms. When I use them in my proofs they make perfect sense, but when you use them in yours they're completely unreadable.
Computers (parsers, rather) are extremely sensitive to notation, and indeed in this project they eschew greek letters and unicode altogether, however it makes things more verbose, but it is almost certain that the authors communicate the ideas in paper with notation like Γ ⊢ e : σ instead of `TYPE Gamma e s`.
> [...] in a dynamic language so that we have no type annotation.
We're talking about type theory and you took the escape hatch.
> Let's say I named the argument "pair_of_ints". Following your logic, [...]
You spoke of conciseness, that's the logic you introduced, not hers.
> It's not good, however, to name the functions (let's add: in global scope) f, g, h, f2, f3, gh, etc. just to avoid typing more characters. Instead, we choose a name which can be understood with as little additional context as possible.
That's perfectly reasonable to expect programmers to use long enough, meaningful names in a complex program. But here the topic is type theory, which are made at most of a few dozen rules (unless you already want to tackle on a complex type system, but that would be like trying to learn how to drive on an indycar). In such a setting, long comprehensive words are not really needed.
If you allow me to transpose this issue of yours to your domain, software engineering newcomers might see this arcane notation of using brackets everywhere quite confusing. Why not simply use plain English to describe a program?
> Yes. My problem is when all the entries in the vocabulary are one (Unicode) character long.
It's not so bad, why limit yourself to 52 characters when you can have so many more to choose from? Korean has more than 20 different characters for vowels alone (luckily they don't have capital letters), Japanese has 2000 kanjis to convey meaning, not counting the (200 or so) kanas used for spelling and connecting words. Chinese has 10k symbols in everyday use, and so many more obscure ones.
The good thing about these Unicode characters is that they have a short notation, but a long pronunciation, a bit like the spelling alphabet (Alpha, Bravo, ...).
I guess that my point is: English speakers have it easy at the morphological level, learning a few more character cannot be that difficult.
> The latter, preferably. If something is meant to denote a context, I see little reason to name it "Γ" instead of, I don't know, "context"?
If there's only one context being considered, one might as well use Gamma (that letter corresponds to C in the roman alphabet, btw). Perhaps the hidden secret of all this discussion is that Type Theory is more a math subject than an engineering one. Of course at some point a type system has to cross this boundary to be implemented, but that doesn't mean that math people have to speak pseudo-code.
> Yes, but then I wouldn't need to work to understand the syntax.
Math uses Greek letters by tradition, perhaps because the first occidental ones where Greek? As for the horizontal bar to separate the premises from the conclusion, it's an inheritance from Gentzen notation for natural deduction (iirc). Obviously, our knowledge builds up incrementally from former discoveries/inventions, because (at the risk of this discussion to become absurd) how would you be able to extend something if you have to start from scratch every time? Conversely, what would be the point of using a different language once you've done the effort of learning the one used all through the literature?
Sometimes things do change however. A few centuries ago, scientific articles were still written in Latin, or sometimes French. In a sense, it has to be a step up in the right direction for native English speakers now that papers are in English (for those devoted to an international readership at least), perhaps not so much for Latinists and French speakers though. Maybe someone like you will do the extra effort of learning the old way, and push for a new way without the fancy typography? But you'd probably have to publish significant papers for that.