Exceptions #1
Exceptions #1
Conversation
| is compiled into a `throw` statement: | ||
|
|
||
| ``` | ||
| throw new Exception(dafnyStringToNativeString(someErrorMsg)); |
There was a problem hiding this comment.
If instead of hardcoding the type Result<T>, we allow a user-defined type, then that user-defined datatype could have several constructors for the failure case. If we additionally allow some kind of Throw member of the datatype, then that Throw member could decide on different C# exceptions to throw, according to the constructor used.
|
|
||
| *Q:* What about target languages which do not have exceptions, such as Go? | ||
| *A:* Go uses a pattern of returning an additional return value to report success/failure, and the Dafny-to-Go compiler would use this pattern too. In general, the idea is to compile `Result<T>` to the idiomatic way of dealing with failure in the target language, be it exceptions, extra return values, `Option`, `Maybe`, ... | ||
|
|
There was a problem hiding this comment.
Yep. In Go, the signature of the target method would have 2 out-parameters, one for the success value (intended to be used only if the second value is non-nil) and an outcome indication (which is the error, or is nil for success).
Go sometimes uses a boolean instead of an error. It would be good if the Dafny-to-Go compiler treated this case, too.
| ``` | ||
| If this happens, and the compiler compiled `operation1` into a `public T1 operation1(args) throws Exception`, then the code generated for the above snippet would have to catch the exception and materialize it into a `Result<T1>`. | ||
| In most cases, this is probably not the code which the user meant to write, so the questions are: Should this still be supported? Should it emit a warning? Should it emit an error? | ||
|
|
There was a problem hiding this comment.
I like the idea of still supporting this, because it then seems that the Dafny code is more meaningful. That is, everything would work as you'd expect in Dafny, except if you start using the :- operator. But since this behavior would involve compiling to try catch blocks that do the switch from exceptions to a Dafny Result<T>, a warning may be good.
Also, something like:
var res: Result<T> := ...;
return res;
would compile into code like:
var res: Result<T> := ...; // no special handling here
if res.Failure? {
throw new Exception(dafnyStringToNativeString(res.error));
} else {
return res.value;
}
| The most straightforward way of supporting this would be to surround `someMethodCall` and `someOtherMethodCall` with a `try/catch` block, materialize their result into a `Result<int32>`, and at the end of the method body, to return `res.get` or throw `res.error`. | ||
| This seems inefficient, can we do better? | ||
| Should it be supported at all, or would we only allow `return` in methods returning `Result`, but no assignment to the result variable? | ||
|
|
There was a problem hiding this comment.
I think it would be nice to support.
Would it be possible to never involve any exception throwing/handling (or the Go equivalent pattern) except for methods marked with {:extern} in some way? If so, then maybe it could be clear what to do in these cases.
|
@RustanLeino is this RFC ready to be merged? It's very hard to find right now and AFAICT there's no documentation for |
|
No, this PR (on the compilation of failure-compatible types and But perhaps you're more interested in the |
|
Thanks, yes that PR is what I was looking for. |
No description provided.