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

7:00 AM · Apr 17, 2021Twitter Web App

maybe we should just use Twelf or Mercury 🙃

suit yourself :)

Replying to

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.

Replying to

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…

Replying to

for sure. I have frequently considered writing my rules up in a datalog 😊 thing is, I tend to care enough about the precise structure and strategy for proof search that I don’t think I’d gain anything by that means for my typesystems’ real implementations.