The recoverable operator mechanism is buggy

[AbdallahS]

In the compile engine, when a operation with non-recoverable operator and some bad argument is evaluated, we may obtain two results: the value bad because the operator is not recoverable, and some other value coming from the operator definition itself. Ideally, a non-recoverable operator wouldn't have to ever have to examine bad arguments in its definition.
Unit tests bool_equivalence_bad and expression_bad_equality illustrate the issue.

[VictosVertex]

I don't know how this would work without using bad in the definition itself without applying basically a strict typing system.

Example bool_equivalence_bad

In the example bool_equivalence_bad this issue appears in the leqv operator. But that's currently somewhat expected considering its definition.

_computedIdx(E,val(bool,true)) :- _computeIdx(E,leqv),
    N = #count { IDX : _computeIdx(E,IDX,val(bool,false)) }, N \ 2 = 0.
_computedIdx(E,val(bool,false)) :- _computeIdx(E,leqv),
    N = #count { IDX : _computeIdx(E,IDX,val(bool,false)) }, N \ 2 = 1.

It simply counts the number of false values. If there is a bad value in there, then all that's happening is the counter not counting it as false. So while it only considers valid arguments of the operator, it doesn't fail on invalid ones.

That's the same reason why when we use a wrong type, we will get a warning but we will also still get a value.

So this:

evaluate(leqv,(val(int, 5),(val(bool, false),()))).

yields this:

warning(type(failed_operation),(),((),leqv,(val(int,5),(val(bool,false),()))))
evaluated(leqv,(val(int,5),(val(bool,false),())),val(bool,false))

Example expression_bad_equality

The same holds true for the second example where eq is the problem:

evaluate(eq,(bad,(val(int, 1),()))).

yields

evaluated(eq,(bad,(val(int,1),())),bad)
warning(type(failed_operation),(),((),eq,(bad,(val(int,1),()))))
evaluated(eq,(bad,(val(int,1),())),val(bool,false))

But that's also what this rule states right?:

_computedIdx(E,val(bool,false)) :- _computeIdx(E,eq), _computeIdx(E,1,val(T,V)),
    not _computeIdx(E,0,val(T,V)),
    _type_extensionalEquality(T).

Doesn't this just state "if the second element is a val and the first one is not the same val, while the type of the first one is extensional - then the result false". Well, bad isn't a val and certainly not the same as thesecond element.

Resolution?

I think, if we do not want to use bad directly in the definition, then we have to disallow the rules when not all arguments fit the operator specification.

We could also throw a warning if evaluations yield two values for one expression, but then of course bad would lose its power if the user disables warnings as the system would just continue to work with the "wrongly recovered" value as well, resulting in unexpected behaviour.

[AbdallahS]

Let's leave the type system aside for a moment and focus on the computation.

In principle, every expression should evaluate to exactly one value. So we shouldn't get (for example)

evaluated(eq,(bad,(val(int,1),())),bad)
evaluated(eq,(bad,(val(int,1),())),val(bool,false))

Either we say eq is well-defined on this pair of arguments (it isn't) and we'll get a boolean back and we don't get bad, or it isn't well-defined and we should only get bad back.

In general, suppose we want to evaluate operation(OP,ARGS) and one of the arguments happens to evaluate to bad. Then, we have three cases:

• OP is recoverable and the rest of arguments are setup so that we do recover and get a proper value
• OP is recoverable but the rest of arguments do not let us recover and we will get bad back
• OP is not recoverable so the rest of the arguments don't matter, we will get bad back no matter what.

Distinguishing between case 1 and 2 is best left to the computeIdx mechanism, since it examines all arguments and knows the specfic semantics of OP. So for a recoverable operator, the computeIdx mechanism needs to cater for each argument being possibly bad and generate the suitable result.

For case 3,

• we could ask computeIdx to watch out for bad in any of its arguments and then expect it to output bad. If this is our approach, then we need to fix the computeIdx definition of eq, leqv, etc. so that they don't produce a non-bad computedIdx when bad is present somewhere.
• alternatively, we can bypass the computeIdx mechanism altogether since we already know what the output is. With this approach, we need to fix some rules in direct.lp so that when we see one argument of non-recoverable operator evaluates to bad, we refrain from querying the operator's module (ie, we avoid generating computeIdx instances). This frees the computeIdx rules of non-recoverable operators to ever have to handle bad, because they won't be called upon with bad arguments in the first place.

For the type system, I'm not too sure of the implications at this stage. I can think of two options. Either we explicitly add something akin to | bad to all declarations as input and output (since there's always a possibility for an operator to be passed bad, and to return bad), or we say that the failure/mechanism is implicit for non-recoverable operators (and we somehow update type.lp to skip the generation of type warnings due to bad).

The type system handling is less urgent because having spurious warnings has less consequences than losing the guarantee (bugs notwithstanding) that every expression evaluates to exactly one value (either a proper value (including none,) or bad, but not both and at least one of them). Besides, there's already a bunch of spurious type warnings coming from statements because the typing of statements is not implemented yet, so the user is currently likely to have warning_ignore(type(failed_operation)). somewhere in their encoding anyway. As such, let's keep this issue for the computation aspect and move the type handling to another issue that we can resolve at a later stage.

[AbdallahS]

Doesn't this just state "if the second element is a val and the first one is not the same val, while the type of the first one is extensional - then the result false". Well, bad isn't a val and certainly not the same as thesecond element.

The way I understand bad is as " I couldn't determine this value because of some error, it could be anything!", so equality between 1 and bad could be false if bad stood for 2, it could be true if bad stood for 1, etc. Because of this ambiguity, we can't determine the output, so we say the output is bad. (this is quite different from none as 1 = none should evaluate to false)