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

Apr 12, 2021

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.

Brendan Zabarauskas

@brendanzab

Apr 12, 2021

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?

Brendan Zabarauskas

@brendanzab

Apr 12, 2021

But yeah, I'd like to be able to run my programs even if they have type errors in them - I just accept that if I do they'll crash if they run into ill-typed code fragments. But then on a release build I want to be sure all code paths are well-typed.

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

András Kovács

@andrasKovacs6

Jun 8, 2021

If we have postponing in elaboration, deferred errors come almost for free. The "guarded constants" in Agda could support this with minimal effort. Not sure why it hasn't been implemented.

Brendan Zabarauskas

@brendanzab

Jun 8, 2021

Is this implemented in elaboration-zoo? Just curious if there's any place I can look to understand this approach better.

Olle Fredriksson

@ollfredo

Jun 9, 2021

Sixty does postponing!

Replying to

and

Do you use it for error recovery? Curious to see how that works!

4:39 AM · Jun 9, 2021Twitter Web App

Replying to

and

No, just for better inference. Errors in elaboration result in sentinel error terms to be able to keep going.

Brendan Zabarauskas

@brendanzab

Jun 9, 2021

Oh gotcha! Is there a place you can point me to to see that? Just planning on plopping in a sentinel/poison value to my new elaborator prototype now, so looking for ideas!

Show replies