Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Geb should expose VampIR error conditions through its STLC API #90

Open
rokopt opened this issue Mar 15, 2023 · 1 comment
Open

Geb should expose VampIR error conditions through its STLC API #90

rokopt opened this issue Mar 15, 2023 · 1 comment

Comments

@rokopt
Copy link
Member

rokopt commented Mar 15, 2023

@lukaszcz made an interesting observation and request:

We’re wondering if there is some failure/error mechanism in VampIR that could be exposed through GEB. This probably doesn’t make much categorical sense, but what we would like to have is some “error” node in STLC that would make the whole computation fail when evaluated. Or some other way of signalling an error. Is it possible to have something like this? This would be useful to e.g. signal that the recursion is too deep - otherwise you need to give some arbitrary element of the right type when you run out of “gas” after recursion unrolling. Or to signal that the user didn’t cover all cases in a match - otherwise one needs to return some arbitrary element of the right type in the unhandled cases. Or to compile debugging assertions.

In other words, we want some way of signalling to the user that a situation occurred which should’ve been impossible but we can’t or don’t want to prove its absence at compile time. Or how otherwise should such situations be handled? Does VampIR have any way of handling them?

To make it clearer, we view these “failure” nodes (that we have in our extended lambda-calculus Core language) more like a debugging facility than a formal part of the language. There is no way to handle failure programmatically. It’s just to signal the user that something went very wrong and their assumptions are not satisfied and to immediately crash the program instead of continuing evaluation with some arbitrary value.

I'll need to learn more than I currently know about VampIR errors and how it exposes them, so I'm pinging @lopeetall to let him know I'll probably be asking him for help. :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants