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.
Conversation
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.
2
7
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
Maybe we do need a standard office: to me this reads as "that's a triple", while relations are functions from inputs to propositions (aka Prop).
2
3
What you have is good for Haskellers or DB people, but I'm used to input/output modes from logic programming (& Twelf, Coq typeclasses, ...); unsure the two are equally expressive.
Neither notation is "obvious", & I have no experience presenting either for real.
2
1
Yeah, was a bit unsure about this here:
Quote Tweet
Replying to @brendanzab @rob_rix and 3 others
Not sure if Twelf's mode checking (cs.cmu.edu/~twelf/guide-1) can let you describe all of what you want for functional dependencies though…
Ok, they seem incomparable on maybe weird cases: modes let you say "all inputs" (like typing in checking mode) and "all outputs", fundeps let you say "in Foo A B C D, B depends on A and D depends on C" (but do you ever need this instead of two TCs? And what of relations?)
1
2
I know that Mercury's modes are less expressive than what you might want - I've I think I remember Peter Stuckey saying he'd recommended some sort of 'dependent modes' for Mercury at one point but I don't know if that went anywhere, and if that is somehow related?
1