Conversation

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.

Brendan Zabarauskas

@brendanzab

Apr 17, 2021

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.

Brendan Zabarauskas

@brendanzab

Apr 17, 2021

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.

Replying to

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?

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

Replying to

hmm… no reason why you shouldn’t have error judgements Γ ⊢ s type Γ ⊢ t type ______________________ Γ ⊢ s → t type Γ ⊢ s error e _________________ Γ ⊢ s -> t error e

Rob Rix‎

@rob_rix

Apr 17, 2021

this specific example would be tedious as fuck if done this way tho it does allow you to be extremely precise about how you *collect* errors. I think I’d actually try to model the type formation judgement here with a sum instead: Γ ⊢ τ type success Γ ⊢ τ type fail e

Show replies