Table of operator precedence

[mikeshulman]

From Dan Piponi on G+:

So pretty please can we have a table of operator precedence near the index of symbols in the HoTT book? I know I'm not the only one who has trouble with this when reading papers on computer science and logic. It's nice that the HoTT book does state how tightly operators bind. But why not put all the information together in a table instead scattering it through the text?

[mikeshulman]

I thought in general we were pretty comprehensive about including parentheses whenever there is any potential ambiguity. The only "precedence rules" I can think of offhand that would go in such a table are the fact that quantifiers scope over the rest of a type expression. What else are you thinking of?

[dpiponi]

the fact that quantifiers scope over the rest of a type expression

That's one. There are uses of pairs of infix operators from o, x, ->, ~, =, and : that don't use parentheses (eg. a o b ~ c). When you're learning a whole bunch of new stuff, and you're not 100% sure of what's going on, having a little help when parsing expressions goes a long way, and I think it helps to be able to parse expressions without knowing anything about the semantics.

(HoTT is way better than most logic texts. I have a really hard time with turnstiles, colons and commas but HoTT doesn't have any of that, and you do use parentheses a lot.)

[mikeshulman]

Okay, this seems like a reasonable suggestion, but we need to figure out what the precedences should be. Clearly \circ has higher precedence than ~ or =, and judgments like : and == have lower precedence than anything else. I guess probably \times and + have higher precedence than \rightarrow. I'm not sure about the relative precedence of -> and =, I would probably always include parentheses when mixing those. Hmm. Would it be too much trouble to make a note of whatever examples you come across in your reading?

Another option would be to just insert parentheses everywhere, I guess.

I'm glad to hear you appreciate the avoidance of turnstiles and commas. We made a conscious decision to avoid those entirely, and it's nice to get feedback that it was a good decision (although I didn't really have any doubt myself).

[mdnahas]

There is a quote I like from an O'Reilley book about C. It goes something like "The real C gurus don't need to know all the operator precedences, because they assume the people reading their code know only the most common rules of precedences. The gurus stick in parens in all other cases."

So, I would say define only the most common ones and encourage everyone (esp. HoTT book authors) to use parentheses.

Mike N.

On Jul 1, 2013, at 8:19, Mike Shulman notifications@github.com wrote:

Okay, this seems like a reasonable suggestion, but we need to figure out what the precedences should be. Clearly \circ has higher precedence than ~ or =, and judgments like : and == have lower precedence than anything else. I guess probably \times and + have higher precedence than \rightarrow. I'm not sure about the relative precedence of -> and =, I would probably always include parentheses when mixing those. Hmm. Would it be too much trouble to make a note of whatever examples you come across in your reading?

Another option would be to just insert parentheses everywhere, I guess.

I'm glad to hear you appreciate the avoidance of turnstiles and commas. We made a conscious decision to avoid those entirely, and it's nice to get feedback that it was a good decision (although I didn't really have any doubt myself).

— Reply to this email directly or view it on GitHub.

[dpiponi]

Great idea. I'll keep notes about precedence as I read the book.