Conversation

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.

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?

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.)

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/.

relation check(_ : context, _ : term, _ : type). relation synth(_ : context, _ : term, _ : type). mode check(_ : in, _ : in, _ : in) is semidet. mode synth(_ : in, _ : in, _ : out) is semidet. 😊