anoma / geb

A Categorical View of Computation
https://anoma.github.io/geb/
GNU General Public License v3.0
28 stars 10 forks source link

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

Open rokopt opened 1 year ago

rokopt commented 1 year ago

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

agureev commented 1 year ago

129 Proposes a straightforward fix but will need major optimization