❤️❤️ the responses
Quote Tweet
PL twitter: quick, what's the scariest screenshot you can find of a paper with an overwhelming amount of inference rules?
Show this thread
1
1
20
Conversation
Serious question: do people (outside of the paper authors) actually understand what these rules mean?
7
4
I consume PL papers as part of my job, and I do actually get a lot of value out of these rules! Sometimes as a reader they can be hard to parse at first. Like anything it takes a bit of taste to use them effectively as a form of communication.
1
10
This said, I *do* think it would be cool to take a step back and think about how we design PL notation in a way that makes communication easier. I definitely think it's an unfortunate barrier to entry, and can be hard to deal with even if you are experienced with it.
3
6
I wonder how we could improve it. part of the issue is the tension between concision and completeness, I think. as indecipherable as judgment rules &c can be at first, I don't think people would prefer, like, 10 pages of English text thoroughly explaining the mechanism.
3
7
maybe part of it is just consistency. seems like many authors like to use slightly different notation, so you have to be careful to read their specific flavor notes prior to engaging with the material. maybe we need a PL standards office 😂
2
1
YES! Clear labels for the judgement forms in boxes would go a long way to reducing the overhead of reading unfamiliar rules.
I still also think we could somehow work on making the distinction between bits of 'syntax' and 'non-terminals' clearer. Like `_⊢_⇒_` vs `Γ`, `e`, `t`. Perhaps making a more uniform notation, like `synth(_, _, _)` would help with reducing the mental overhead?
2
4
I just know when notations get very complicated I lose track of how to mentally parse the symbols into a properly grouped AST, partly due to forgetting the original notations halfway through. This then results in lots of backtracking while reading.
1
4
Show replies
There was a time, which seems to have ended around when I entered grad school, when people consistently explained how to read each and every judgement: ~"G|-e:t is read as under type environment G, expression e has type t." Now many papers don't even explain specific rules. :-(
1
6
I don't want each of the rules explained but I do want the author to say why I was supposed to care about that part of their paper
3
11
Show replies