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.
Conversation
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…
1
1
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?