Conversation

re. github.com/jonsterling/dr, have you considered how error reporting might work with the refiner? Seems like a really neat approach - but just a little worried about providing a nice diagnostics about the surface syntax and supporting error recovery, etc.

github.com

GitHub - jonsterling/dreamtt: A pedagogic implementation of abstract bidirectional elaboration for...

A pedagogic implementation of abstract bidirectional elaboration for dependent type theory. - GitHub - jonsterling/dreamtt: A pedagogic implementation of abstract bidirectional elaboration for depe...

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Brendan Zabarauskas

@brendanzab

Replying to

@jonmsterling

Idea is that you don't want your type checker to stop at the first error. You'd prefer it if it could continue type checking, giving you more than one error.

12:14 PM · Apr 12, 2021Twitter Web App

Replying to

and

I do this in a bit of a bodgy way with an 'error' variant in my ASTs, but you run into issues where error sentinels pop up in type errors if you aren't careful. Leading to the fun of Rusts 'error: expected `type error` found `type error`' back in the day 😂

Brendan Zabarauskas

@brendanzab

Apr 12, 2021

I think most of those bugs have been squished though. But yeah, I'd prefer it if it was a bit more thought out - like something like exceptional type theory perhaps?

Show replies

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Brendan Zabarauskas

@brendanzab

Apr 12, 2021

It's incredibly useful, especially for interactive editing. Where you might be in the middle of a refactor and you want to have an understanding of the bits of code that are broken (there might be multiple bits at once).

Replying to

and

Would you truly prefer that?

Brendan Zabarauskas

@brendanzab

Apr 12, 2021

Yeah! I'd like it to be able to do the best it can, given the information it is confident about.

Show replies