Conversation

Brendan Zabarauskas
@brendanzab
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
Brendan Zabarauskas
@brendanzab
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
Pierce Darragh 🍴🥄 | 🦆
@pl_pierce
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
Pierce Darragh 🍴🥄 | 🦆
@pl_pierce
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
Rob Rix‎
@rob_rix
I mean, when you’re defining classes of judgements you could do worse than just label them clearly. [ Γ ⊢ x ⇐ T ] checking … [ Γ ⊢ x ⇒ T ] synthesis … would go a long way, without requiring people adhere to any particular notation or whatever.
1
13
Brendan Zabarauskas
@brendanzab
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
Rob Rix‎
@rob_rix
I actually give mixfix signatures for sequents/judgements in my notes a lot like that, most of the time. Only with types, too: _ ⊢ _ ⇐ _ : (Context, Term, Type) (tupled because it’s a relation rather than a function in general, tho I use -> à la fundeps for pure outputs.)
3
4
Rob Rix‎
@rob_rix
an example of a functional dependency might be synthesis: _ ⊢ _ ⇒ _ : (Context, Term, Type) | (Context, Term) -> Type what’s really fun is, this translates surprisingly well into code, following
@bentnib
’s /An Algorithmic Approach to Typechecking and Elaboration/.
2
2
Brendan Zabarauskas
@brendanzab
relation check(_ : context, _ : term, _ : type). relation synth(_ : context, _ : term, _ : type). mode check(_ : in, _ : in, _ : in) is semidet. mode synth(_ : in, _ : in, _ : out) is semidet. 😊
1
3
Brendan Zabarauskas
@brendanzab
More just pointing out that there are some neat things about how logic programming does things. Eg. with modes and determinism. Could possibly be a handy perspective perhaps when coming up with a general notation for this stuff, but I dunno.
2
1
Show replies