Conversation

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.

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

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

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

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?

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

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

you still end up essentially defining the either monad manually in the structure of the premises/conclusion which is unfortunate but I don’t think I know how to parameterize rules over an effectful/monadic context yet so here we are