Conversation

Rob Rix‎
@rob_rix
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.
1
1
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.
2
1
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.
1
1
Rob Rix‎
@rob_rix
hmm… no reason why you shouldn’t have error judgements Γ ⊢ s type Γ ⊢ t type ______________________ Γ ⊢ s → t type Γ ⊢ s error e _________________ Γ ⊢ s -> t error e
1
1
Rob Rix‎
@rob_rix
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
1
1
Rob Rix‎
@rob_rix
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
1
1
Rob Rix‎
@rob_rix
I guess you could always just say “yo errors are thrown back up through the derivation tree and we make some effort to collect multiple such when data dependencies allow” and drop the mic
2
1
Brendan Zabarauskas
@brendanzab
I know Ulf Norell's thesis on Agda defines a macro over the elaboration rules (in prose) that allows him to thread the metacontext through all the rules. Not sure if that is similar! But kind of reminds me a bit.
1
1