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.

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).

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

Yeah, I generally find Rust does a pretty good job of this - like it will do as much as it can (although it's not perfect). There is ultimately a little heuristics involved to avoid it everything haywire on big things - I think Rust has a cut-off on how many errors it dumps?

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

Replying to

and

Definitely not familiar how OCaml handles it, but definitely got frustrated with Purescript, which seemed at the time to be implemented in terms of a monadic parser and type checker - ie. bail on the first error it found.

Brendan Zabarauskas

@brendanzab

Apr 12, 2021

The bits where I get frustrated in Rust is where it won't continue on to lifetime analysis if type checking fails. So you might think everything is fine, but suddenly you fix the last error and get a bunch of lifetime issues to sort through.

Replying to

and

Rust doesn't have an explicit cutoff. When encountering "serious enough" errors it would stop at the stage boundary. What it does now is to recover as much as possible from what's encountered and mark it as an Error, so that the following stages ignore it entirely.

Esteban K�ber –

@ekuber

Apr 12, 2021

If the parser has a failure inside of a function, for example, the parser will try a couple of common substitution mistakes, and if they don't apply, consume everything until it find a matched closing }. Then that AST node gets marked as recovered so that it doesn't get typechkd.

Show replies