Change the runtime behavior of then
#1304
Conversation
| @@ -1273,7 +1277,19 @@ export class CompilerVisitor implements IRVisitor { | |||
| // as evaluation was not successful. | |||
| this.recoverNextVars(savedValues) | |||
| this.resetTrace(just(rv.mkList(savedTrace))) | |||
| break | |||
|
|
|||
| if (kind === 'then' && nactionsLeft > 0 && result.isJust() && !(result.value as RuntimeValue).toBool()) { | |||
There was a problem hiding this comment.
Because of the way toBool is implemented, this can hide type errors if they make it through to here.
https://github.com/informalsystems/quint/blob/main/quint/src/runtime/impl/runtimeValue.ts#L523-L529
toBool(): boolean {
if (this instanceof RuntimeValueBool) {
return (this as RuntimeValueBool).value
} else {
return false
}
}
That is, if the result.value is, e.g., a string, then the final conjunct will be false, and we'll end up hiding the error. This could make it really hard to catch such a problem.
To work around this, we should add a test of result.value instanceof RuntimeValueBool.
There was a problem hiding this comment.
The whole code base of the simulator assumes that the IR is well-typed, which is ensured by the type checker. Sure, I will add an extra test, but what I should do in the case this test is failing.
There was a problem hiding this comment.
RuntimeValue encapsulates the types of the concrete values, so result.value instanceof RuntimeValueBool simply would not work here.
There was a problem hiding this comment.
We could introduce a predicate just for this test, but I don't see any value in doing so. Actions and runs are always returning Booleans. This has to be enforced by the type checker.
There was a problem hiding this comment.
I have improved the code a bit. However, adding defensive code to this very method does seem overkill to me. For starters, it would be harder to read. On top of that, we would have to ensure type correctness in the whole compiler then, which is not the purpose of this phase.
There was a problem hiding this comment.
If the assumption is that everything is well typed and behavior is undefined otherwise, those conversions should be raising exceptions not returning undefined?
There was a problem hiding this comment.
I guess this is a larger scale
Design problem and not limited of this pr, so I'm ok deferring this.
I would not surprised if this end up biting us tho, as we still send stuff that fails type checking to the simulator via the repl and we still have holes in the type system.
There was a problem hiding this comment.
If the assumption is that everything is well typed and behavior is undefined otherwise, those conversions should be raising exceptions not returning undefined?
Agree. I think the easiest thing we could do is to throw exceptions in runtime values, e.g., RuntimeValueBool could throw an exception when it is converted to something else. That would help us to defend from subtle typing errors and prevent us from introducing too much defensive code.
Co-authored-by: Shon Feder <[email protected]>
Closes #594. Similar to the behavior described in #594, @josef-widder and I have noticed that the current semantics of
A.then(B)is tricky whenA.then(B)evaluates tofalse. In this case, it is not clear whetherAorBevaluated tofalse. This makes it hard to debug long runs. In general, engineers expect that a sequence of steps cannot just stop somewhere in the middle, which is howA.then(B)works now. This looks a bit like a deadlock, especially when we have non-deterministic choices orany.This PR is changing the runtime semantics of
A.then(B)in the simulator to the behavior that I believe is more consistent with normal programming languages. Namely, ifAevaluates tofalse, thenA.then(B)emits a runtime error saying that a computation cannot continue.This is a breaking change. Some tests may fail. But this is good, these tests may catch problems that were not caught previously.
CHANGELOG.mdfor any new functionality