3 ms·

> My main question here is: why is conciseness a good thing? Going through a single line of text to understand a concept is much better than having to go throu

> My main question here is: why is conciseness a good thing? Going through a single line of text to understand a concept is much better than having to go through two or more. I believe you should understand that, if your definition of conciseness matches mine. As a programmer, you know first hand that repeating oneself is bad practice: it's better to define a function which will encapsulate this computation you need to repeat rather than using copy and paste. The same goes for any language: having vocabulary to embody reccuring ideas helps us discuss complex ideas more easily. > Do you really need to express concepts with a single strange character? It is only strange to you because you don't speak greek. Of course many don't: my pedantic point is that Greeks might disagree with you about these characters being strange, and less pedantically, the scientific community will argue that it's not that strange when you belong to their group. There are only a handful of them to remember in the context of type theory. 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? 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. These concepts are indeed not easy to understand: you would have to learn to become a Gorilla in order to be able to hold that banana you languish for, or survive in the Jungle that surrounds it. One good thing about using a different character set is that they stand out. There's little chance to confuse them with words of vernacular English. Greek mathematicians actually might have a harder time with these notations than you do :)

klibertp 5y 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.
- siraben 5y ago
  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`.
- smlkrdrmlk 5y ago
  > 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.
- 5y ago

klibertp 5y 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.

siraben 5y ago
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`.
smlkrdrmlk 5y ago
> 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.
5y ago