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.
Conversation
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
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.
1
2
Is this implemented in elaboration-zoo? Just curious if there's any place I can look to understand this approach better.
3
Sixty does postponing!
1
2
Do you use it for error recovery? Curious to see how that works!
1
No, just for better inference. Errors in elaboration result in sentinel error terms to be able to keep going.
1
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!
1
Ahh, I found it! github.com/ollef/sixty/bl
It's neat how you make a new metavariable for errors. In the past I put an error sentinel in my values and it ended up getting really confusing and unmanageable! 😬
1
1
There it is! Also note that the sentinel Builtin.fail unifies with anything without error in an attempt not to get cascades of errors due to errors.
1
Oh yeah, I’ve been doing that for the sentinels when I’ve had them as part of my values. What happens if you evaluate a Builtin.fail during type checking?