Error 3268: Empty sequence cannot be applied appears inappropriately

[ivor-spence]

Description

Error 3268 is reported even when the expression should not be evaluated.

Steps to Reproduce

In the quick interpreter type

let s = [] in forall i in set inds s & s(i) > 1

Expected behavior: [What you expect to happen]

This expression is vacuously true so I would expect the result "true"

Actual behavior: [What actually happens]

Error 3268: Empty sequence cannot be applied in 'DEFAULT' (console) at line 1:40

Reproduces how often: [What percentage of the time does it reproduce?]

Every time

Versions

Which version of Overture are you using? Also, please include the OS and what version of the OS you're running.

Overture 2.5.4 on Windows 10.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[peterwvj]

Thanks for reporting. I can confirm that this problem is present in both Overture 2.6.2 and VDMJ.

[nickbattle]

This should be a simple problem, by the look of it. I'll look into it when I'm back in the UK next week.

[nickbattle]

This is interesting. It is a simple matter to suppress the check that empty sequences cannot be indexed, but then that would naively allow expressions like to pass the type check, when they are clearly going to fail. The point about the example in this bug is that the expression is never actually evaluated and so the fact that s is empty does not matter. But the type checker cannot generally distinguish (statically) what will and will not be executed.

VDMTools gives the same type checking error as VDMJ/Overture in this example - saying that an empty sequence cannot be applied, though it does also (usefully) give a warning that an empty sequence is being used in a set bind.

Not sure what's best to do in this case. Opinions?

[peterwvj]

Thanks for explaining.

Strictly speaking the interpreter should be able to evaluate the expression, I think we can agree on that. But then again I can't convince myself that writing expressions like this brings any true value. For these reaons, I think the most correct thing to do is to raise a warning instead of an error, but honestly I'm not sure it's worthwhile implementing this change. Assuming we decide to leave the tool unchanged (which I'm fine with), we could add a comment in the tool manual saying that type-checking of sequence applications is strict and does not allow application of empty sequences regardless of where the expression appears.

[tomooda]

Interesting. I tink this is like inferring type in then/else clauses in some sense.
Is it possible to infer that s after the & is typed seq1 of ? and the type checker skips empty check against s(i)?

[nickbattle]

But on what basis can we infer that "s = []" is type seq1?

[tomooda]

Well,
In the forall expression, s(i) > 1 would be evaluated if and only if inds s is set1.
So, we can infer inds s is typed set1 in the context of s(i) > 1.
Then we can infer that s is typed seq1 because inds s is not empty.
Of course, inds s is actually empty, but we can assume that s is seq1 within the local context of the forall's body expression.
I think this is just like if expression. Assuming that we have if is_nat(x) then x + 1 else ..., we can assume that x in the context of x + 1 is typed nat because of the if expression regardless the actual value of x.

[nickbattle]

Ah, I see what you mean. Interesting. But in general it's quite a tricky thing to infer - there is an arbitrary expression involving possibly multiple variables in the binding, and from that we have to infer some type-qualification of the variable(s) concerned if the clause dependent on the bind is evaluated.

It would be relatively easy to make inferences for a few common cases, perhaps. I'll have a look.

[tomooda]

Yes, quantifiers part is not too many(forall, exists, exists1, iota, set/seq/map comprehension, let-be-st, for, for-all), but rules like (inds s):seq1 of t⊢s:set of t is hard to cover all cases.
(s1 inter s2):set1 ⊢ s1, s2:set1
(power s1):set1 ⊢ s1:set1
(dunion s1):set1 ⊢ s1:set1
(dinter s1):set1 ⊢ s1:set1
(elms s):seq1 of t⊢s:set of t
(inds s):seq1 of t⊢s:set of t
(reverse s):seq1 of t⊢s:set of t
are the rules that came up to my mind.
(If we had map1 type, type inference rules could be more comprehensive)

[peterwvj]

I'm questioning whether this is actually worthwhile doing. I mean, why complicate type-checking just so we can handle non-sense expressions? After all, isn't it more correct to report a warning?

[ivor-spence]

I sympathise with what you say and of course it is not my decision but I think it seems nonsense to you because you are thinking of a user typing in this expression with an empty sequence. My situation is an example of the general case where some system is generating vdm text and passing it to vdmj for evaluation. In this context it may well happen that the test needs to be applied to an empty sequence and as things stand the library does not return the result which the language specifies. A warning is perhaps not appropriate if there is no human user at the time? I should add that I have found the library to be extremely reliable and a great help with what I am doing, so thanks to all involved in its development. Ivor From: Peter W. V. Tran-Jørgensen <[email protected]> Sent: 14 September 2018 10:58 To: overturetool/overture <[email protected]> Cc: Ivor Spence <[email protected]>; Author <[email protected]> Subject: Re: [overturetool/overture] Error 3268: Empty sequence cannot be applied appears inappropriately (#689) I'm questioning whether this is actually worthwhile doing. I mean, why complicate type-checking just so we can handle non-sense expressions? After all, isn't it more correct to report a warning? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub<#689 (comment)>, or mute the thread<https://github.com/notifications/unsubscribe-auth/AjQdYW2VfFEpF48ioAvfMzdK2lFwIpVhks5ua33AgaJpZM4WXa3F>.

[peterwvj]

Thanks! I'm happy to hear that you find the tools useful!

Please help me understand, if there's no human present at the time why may a warning not be appropriate? A warning still allows you to execute the model (unlike type-errors which prevent you from doing that). So just to clarify, all the warning is doing is telling you that you may be doing something you did not intend. If, however, an empty sequence application is executed then that would yield a runtime error.

[nickbattle]

But if an empty sequence was passed to the example expression, the body of the forall expression would never be evaluated, so it would be fine. The problem is that we are aggressively raising a type error for a situation that will not occur.

I'll see what we can do with Tomo's inference idea. We already do do some of this "forward" inference with tests and preconditions that include is_nat and the like, so it may not be too much work.

[ivor-spence]

OK, I had not realised that. I thought that when you talked about a warning you meant from overture rather than vdmj. My code has clearly interpreted the vdmj warning as an error which meant that there was no valid value. If there is still a value of “true” available with the warning then my problem is solved. My apologies for that. From: Peter W. V. Tran-Jørgensen <[email protected]> Sent: 14 September 2018 15:15 To: overturetool/overture <[email protected]> Cc: Ivor Spence <[email protected]>; Author <[email protected]> Subject: Re: [overturetool/overture] Error 3268: Empty sequence cannot be applied appears inappropriately (#689) Thanks! I'm happy to hear that you find the tools useful! Please help me understand, if there's no human present at the time why may a warning not be appropriate? A warning still allows you to execute the model (unlike type-errors which prevent you from doing that). So just to clarify, all the warning is telling you is that you may be doing something you did not intend. If, however, an empty sequence application is executed then that would yield a runtime error. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub<#689 (comment)>, or mute the thread<https://github.com/notifications/unsubscribe-auth/AjQdYdZBrHXWEbVc8cyd-13brEOQAT1pks5ua7nmgaJpZM4WXa3F>.

[nickbattle]

There's a small bug that is causing the warning to be suppressed in VDMJ/Overture (the inds typecheck is not propagating the emptiness of its argument to the emptiness of its result). That's easy to fix. But the typecheck error for the body of the forall would still remain.

The existing mechanism for qualifying types, for example when an is_nat is used in a conditional, won't work for bindings without some changes. I'm trying to find a way to do it without too much change!

[nickbattle]

Incidentally, the same kind of error occurs with empty maps ("Empty map cannot be applied" errors) that are inside some sort of conditional defence.

The search for an uncomplicated way to solve this internally continues... :-(