Open or Closed set of concepts?

[stefjoosten]

Trigger of the discussion

In issue #437, @RieksJ used Ampersand v3.5.1[development:28036cb] to compile

{-01-} CONTEXT BugX IN ENGLISH
{-02-}
{-03-} CLASSIFY Concern ISA Variable
{-04-}
{-05-} varValue :: Variable * VarValue [UNI]
{-06-} varTrace :: Variable * Assignment [UNI,INJ]
{-07-} asmValue :: Assignment * VarValue [UNI,TOT]
{-08-}
{-09-} RULE "one": (I[Variable]-I[Concern]);varValue |- varTrace;asmValue
{-10-} RULE "two": (I[Variable]-I[Concern]) |- varTrace;(I-asmValue;asmValue~)
{-11-}
{-12-} ENDCONTEXT

This resulted in the following output:

Error at symbol () in file BugX.adl at line 10 : 51
  Cannot disambiguate: I
  Please add a signature.
  You may have intended one of these:
  I[Concern]
  I[Variable]

Note that line 10:51 refers to the I in I-asmValue;asmValue~.

After spending quite some time, Rieks discovered that RULE "two" does not match at the very end, i.e. the target concept of the expression I-asmValue;asmValue~ does not match the target concept of the left hand side of the rule. He wants a better error message.

@sjcjoosten commented "there is no way for the type checker to determine the type of (I-asmValue;asmValue~) without knowing the type of the I used there, since - takes the type of its first argument. Solving the ambiguity first should help you get the error message you wanted."

Rieks commented "I am flabbergasted. In the rule I occurs three times, two of which have their concept specified. For the third I, it seems obvious to me that its concept should be Assignment - I do not see what other concept could possibly be used here since Assignments are not in any CLASSIFY statement. In a similar fashion, I cannot think of any other possible type for (I-asmValue;asmValue~) than [Assignment*Assignment]. It is not ambiguous at all. Still, you tell me that for you there is no way to determine the type. So what am I missing here, or what?"

Analysis

Rieks reasons from the assumption of a Closed set of Concepts (hereafter: CsoC). All concepts are contained in the script. The concepts are Concern, Variable, VarValue, and Assignment. Now the type checker has to make a choice as to which of these four fits I on line 10 : 51. Both the target of varTrace and the source of asmValue are Assignment. The concept Assignment is involved in no generalization or specialization whatsoever. So in a closed world, there is no ambiguity: Assignment is the only possible type for I on line 10 : 51.

Sebastiaan reasons from the assumption of an Open set of Concepts (hereafter: OsoC), and there may be more concepts than the ones contained in the script. Now assume that there may be a concept C, which is a specialization (i.e. a subset) of Assignment. Obviously, I[Assignment]-asmValue;asmValue~ has a different value than I[C]-asmValue;asmValue~. So the expression is ambiguous and must be rejected.

The issue

Since Sebastiaan is sticking with the OsoC, I am afraid that the error message #437 (comment) will not be a satisfactory solution for Rieks in the long run, even if this message is good enough for Rieks' specific example.

Rieks' argument that "it seems natural" is insufficient for me. If we would go for the "natural" things, we would be following many bad habits that are considered "natural" in the IT-world. In our project, we do things differently for very good reasons. These good reasons are what I am looking for. For now, I can only use my personal preference to justify a choice between the CsoC or the OsoC. And personal preference is too little to go on. By the way, I would prefer a CsoC intuitively (as Rieks does). But we won't do so until we have better arguments.

So now I am curious to learn all the solid arguments for either CsoC or OsoC. I have but a few:

• CsoC can produce better type errors, because there are fewer choices to be made. This argument is supported by Rieks' argumentation and example, which is not much to support the argument.
• OsoC is what we have now in our type system. This argument is not in favour of either assumption, but it defines the status quo.
• OsoC is implementable, because it is implemented in our current system. Sebastiaan, are you saying (above) that you don't believe that CsoC is implementable (efficiently)? If so, I think we must challenge that; I find it difficult to believe. We have to get to the bottom of that.

[sjcjoosten]

I believe there are several reasons why to use OsoC. The main reason is that we want Ampersand scripts to be modular, so let's assume the set of all types will be extended in the future. Consequently, a rule like I = V in a script that has exactly one concept, should be ambiguous, as there is no way to say that there is no other concept.

On the implementation of CsoC (or of error messages that assume CsoC), I think this is tricky because of efficiency reasons.

To be more precise: I believe that the type suggestion problem for CsoC is NP-hard.
I define the type suggestion problem for CsoC as follows:

input: a parsable ampersand expression and a set of relation declarations and concept-ISA rules. The size of the script (in a parsable layout) is the size of the input.
problem: is there a type annotation (fully annotating every relation, I, V, and unary complement in the ampersand expression) such that the expression is well typed.

Note that determining whether a fully annotated expression is well typed is the same for CsoC and OsoC.

It is trivial to see that the type suggestion problem for CsoC is in NP. I have no proof to support that it is NP-hard (and therefore NP-complete), nor do I think such a proof would be interesting, as I believe the OsoC to be a better way to go regardless of whether the type suggestion problem for CsoC is NP hard. So I'm not really eager to get to the bottom of that.

[sjcjoosten]

A small remark on this part of Stef's comment:

in a closed world, there is no ambiguity: Assignment is the only possible type for I on line 10 : 51.

Assignment is also an impossible type, as it does not rid the expression of type errors. That is: there are no valid types for the I on line 10.