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.

Brendan Zabarauskas

@brendanzab

Apr 17, 2021

YES! Clear labels for the judgement forms in boxes would go a long way to reducing the overhead of reading unfamiliar rules.

Brendan Zabarauskas

@brendanzab

Apr 17, 2021

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

Apr 17, 2021

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

Apr 17, 2021

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

Brendan Zabarauskas

@brendanzab

Apr 17, 2021

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

Brendan Zabarauskas

@brendanzab

Apr 17, 2021

maybe we should just use Twelf or Mercury 🙃

suit yourself :)

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.

Rob Rix‎

@rob_rix

Apr 17, 2021

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.

Replying to

Oh yeah, definitely thinking more in terms of 'high level specifications for communication' rather than an actual implementation. I definitely care about the precise proof search strategy too, however.

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

Replying to

That said, Mercury would be able to generate pretty efficient code for a bidirectional type checker defined using the modes above. I wouldn't want to use it for an implementation though - more because I'd want an actual implementation to do error recovery, and give nice errors.

Brendan Zabarauskas

@brendanzab

Apr 17, 2021

It would be neat if you could somehow 'decorate' the high level spec with stuff to do with errors though - kind of like how ornaments work?

Show replies

Replying to

yeah that distinction is pretty handy, e.g. replace all the ⇒/⇐s in a bidi typesystem with : and you recover the nondeterministic specification of it (which sounds annoying to have to prove correct if you’ve gone in the other direction by bidirectionalizing an existing theory)