Comment by smlkrdrmlk

> 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.