Type checker: Issue with type checking of operation with union type arguments

[peterwvj]

The spec below does not type check and we believe it should. It is as if the type checker does not recognize op: A * char and op: B * int as valid solutions for the call when op is declared inside B.

The problem is the same for VDMJ.

class A

operations

public run : () ==> ()
run () ==
let x : A | B = new B()
in
  x.op(x,-1); -- <- ERROR: Member op((A | B), int) is not in scope. 

end A

class B

operations

public op : A * char ==> ()
op (-,-) == skip;

public op : B * int ==> ()
op (-,-) == skip;

end B

If the two operations named op are moved to class A then it type checks without errors.

[tomooda]

I think the point is not the arg type, but the static type of x in x.op. The A class does not have the operation op as the error message says. For example, the following compiles successfully.

let x0 : B = new B() in let x : A | B = new B()
in
  x0.op(x,-1);

[peterwvj]

Yes, you are very right. Thanks for pointing it out.

[ldcouto]

So this is not a bug then? Can we close @peterwvj ?

[nickbattle]

I think this is OK. It's complaining (albeit not that clearly) that there is no common operation in A and B that conforms to the signature. This is why moving one of the operations to A satisfies the TC. Though you could argue that using "possible semantics" this should be allowed, since it would work if x was of type B. Hmm.

[ldcouto]

Does possible semantics apply to op calls as well as values?

[peterwvj]

That's what I'm thinking. If we use possible semantics elsewhere then why does this model not type check without errors?

Anyways, if you move both operations from B to A these classes still don't have op in common (see below), but now the model TCs without errors?

class A

operations

public run : () ==> ()
run () ==
let x : A | B = new B()
in
  x.op(x,-1);

public op : A * char ==> ()
op (-,-) == skip;

public op : B * int ==> ()
op (-,-) == skip;

end A

class B
operations
end B

[ldcouto]

Well, an argument could be made that possible semantics apply to values but not to references. I'm not saying it's the greatest argument of all time, mind you.

What version are you testing this on? I'm getting different results from you on 2.3.0.

[peterwvj]

I'm on 2.3.0 :) I get no TC errors for the spec I just posted. Do you?

[ldcouto]

No, I don't.

What I did originally was move the run op into B and that causes errors. But now I copied your spec and it's fine.

So, there is some weird alphabetical stuff going on here.

[peterwvj]

Just to make sure... I never meant to move run but only the two operations named op.

[ldcouto]

Is there a difference between moving the 2 ops into B or run into A?

There shouldn't, but there is.

[peterwvj]

I guess that was my original point: The original model that I posted have TC errors, whereas the next model I posted does not.

[ldcouto]

No...

The original model has run and the ops in separate classes. The repost has them all in the same class. But, if you have all 3 ops in the B class, it will give an error.

[nickbattle]

Phew... I see I missed a few comments here :)

I can explain what the TC is trying to do (it may be that there are errors, of course). When you make an object call, like "x.op()", and the type of "x" is a union of two or more classes, the TC creates an anonymous pseudo-class that has all of the fn/ops from the union members. If two or more classes define a name "op" with the same number of parameters, those are merged where possible - so "op: nat ==> nat" and "op: nat ==> char" merge to "op: nat ==> nat | char". I think that ops with different numbers of parameters are just overloaded in the pseudo-class. And I can't remember what the hell happens with inherited names that overload etc, but you get the idea. There are also rules about accessibility too (if you try to merge public and protected ops, for example).

Then the TC proceeds by checking the call against the pseudo-class. In effect, if A and B define the ops mentioned above, then the result of "x.op(1)" would be "nat | char", which is what would really happen if x was either A or B.

So looking at the original spec at the top, I think this should be legal (on reflection!), just as when the two ops are moved into the A class itself. Which means we have a bug...! I'll take a look.

[peterwvj]

Okay thanks for explaining this and for taking a look!

[nickbattle]

I've started to look at this. What seems to be happening (in VDMJ) is that the pseudoclass that is created for A|B is actually called "A" (which may be a mistake!). Then, when it is trying to decide whether "x.op" is a private or public binding, it tests whether the type of the "x" has the current class, A, as a supertype (ie. "x.op()" is a private/protected binding, not a public one). So then it sets the environment to just A's methods (as this is private) and hence fails to find either of the "op" methods.

I'll look into changing the name of the pseudoclass to something invented (so that it doesn't think "x.op" is a private binding), but I suspect that may raise other problems.

[peterwvj]

Thanks for explaining this. So just to make sure, you are trying to change the type checker to allow the specification, as originally posted, to type check without errors?

[nickbattle]

I've made some improvements to the pseudoclass generation, including renaming it, and now the type checking looks correct. But there is a new problem: the runtime binding does not match the right operation:

> p new A().run()
Error 4087: Cannot convert B{#2} (B) to A in 'A' (test.vpp) at line 6:11
Stopped in 'A' (test.vpp) at line 6:11
6:            x.op(x,-1); 

So that's trying to bind to "op: A * char" at runtime. I can't remember how the runtime binding is decided, so... it'll take a bit longer :(

Incidentally, I tried this on VDMTools. It says the following:

test.vpp, l. 6, c. 7:
  Error[327] : The operation "op" is not defined in class "A"

That's a slightly different interpretation of the possible semantics. It seems to want all members of the union to provide the operation, whereas VDMJ is content if only one of them does.

(sigh).

[nickbattle]

Hmm. The VDMJ dynamic binding assumes, reasonably, that all of the operations/functions in the object are distinguishable by the types of their parameters - indeed, there is a static TC check to enforce this.

But in this scenario, the pseudoclass created as the union of A and B (and therefore all of the operations/functions in them) has produced a signature for op like, "op: (A|B) * (char|int) ==> ()". So the "types of the parameters" in A|B are themselves a union of all the possibilities, with the overloads rolled up. So when these parameter types are used to lookup the dynamic binding (in the belief that they are distinct), you get one or other of the operations bound at random - on my machine, it fails normally, but works in the debugger!

Intuitively, we ought to be able to look at the actual types of the arguments passed and choose the operation with matching parameter types. But we cannot get a Type from a Value (we can only test whether a Value is of a given Type). So we would have to laboriously check the members of the parameter type unions until we found one that matched the arguments... which is ugly :-(

[nickbattle]

Well, detecting the actual types of the arguments does seem to work. But it ain't pretty.

[peterwvj]

I'm just trying to understand this. So since it must be possible to determine statically what operation is being called then how can the approach of merging the operations work? Does the new approach always guarentee that the same operation is chosen?

[nickbattle]

I don't think it is possible to determine statically which operation is called, in general. You don't know, in general, which class "x:A|B" is, hence where "x.op(args)" will bind. The new approach will always call the same operation given the same arguments.

[ldcouto]

Not to make it many more complicated but if A and B both have an op with the same name and type parameters, there is even less chance of determining what gets called.

So, I guess the type checker should allow it, provided at least 1 of the types has the op; the pog should generate some PO to ensure the right call is always made. I guess the interpreter non-deterministically picks one of the possible operations.

This whole thing seems like such a mess. Why would anyone ever want to make a model like this?

[peterwvj]

Ah, yes you are right. I've always been under the impression that it would be possible to determine statically which operation is being called (ignoring overriding). Combining overloading and union types complicate things a lot and overloading is not even that helpful.

[nickbattle]

Yes Luis, it's quite a mess. It's also a lot more complicated than it appears at first sight. I think the original VDM++ designers made some choices at the level of "hey, let's have classes with instance variables", but didn't realise the many subtle choices that are involved in OO semantics - even for "simple" languages, let alone one that allows things like union types. I can't see why anyone would want to create a model like this either. Its meaning is completely obscured by the OO semantics, whatever they're meant to be.

I've been struggling with this sort of thing since 2008 :) Maybe you can see why I prefer SL!

[ldcouto]

I, too, also prefer SL. But I think we are in the minority.

I'm hopeful that the LB can make some inroads on this stuff this year. To me, a lot of these issues boil down to the interplay between OO and Union types. And that's just not clearly defined.

[nickbattle]

OO and unions do complicate things, but there are enough unresolved issues just with basic OO behaviour. Did you see that paper I presented at Workshop 8?

http://wiki.overturetool.org/images/b/bd/2010battle.pdf

[ldcouto]

Yep, I've read that paper.

IIRC, most of those issues are about deciding what should happen in various situations. And there are proposals/implementations for quite a few of them.

We should take a few of the outstanding ones and really aim for having them solved during this term of the LB.

[nickbattle]

Yes, "deciding what should happen in various situations", as in, "a formal specification language" :-)

It's a lot of work. Even if we can agree the semantics, the changes to VDMJ/Overture would be significant. Would VDMTools ever catch up? Is that a problem, especially if we end up cutting off a lot of Japanese customers with large existing VDM++ models? Or is this done by "classic/vdm10/etc" switches (which is then even more complicated in the internals!).

But yes, in principle, this is what the LB does - though it should be driven by RMs.

[ldcouto]

You're right Nick. It's true that it has to be specified and implemented and that's not nothing. I just meant that the possible solutions to many of those issues are more or less known. Whereas many Union/OO issues are simply unexplored so there is even more work to do. Maybe I'm not explaining it clearly.

Also, I'm not sure we should worry about VDMTools users. I don't know of any successes to convert them to Overture.

I would also like the LB to be more proactive. Waiting for RMs seems... I dunno, like we're settling or something.

[nlmave]

Also, I'm not sure we should worry about VDMTools users. I don't know of any successes to convert them to Overture.

We'll perhaps there are good reasons why they still use those tools (i.e. C++ code generation); and at least the VDM(-SL) operational and static semantics are both defined in VDM-SL itself, so there is actually a specification of what the tool does :-). As far as I know, these specs are still kept fully in line with the tool (ask PGL). Very much not so the case in Overture, which is currently a code-only approach; perhaps with the exception of the VDMJ design documentation. When are we actually going to start to use Overture ourselves to specify and validate what we want?

I would also like the LB to be more proactive. Waiting for RMs seems... I dunno, like we're settling or something.

That's easy to solve: submit the paper(s) from Overture-WS8 (including the onces from Erik Ernst) to a RM; to jumpstart the process. Perhaps it is time to consider VDM-18 (or whatever other acronym we think of) which shows proper language evolvement; backwards compatibility is IMHO not necessarily a hard requirement. Languages like ADA seem to have survived these steps too (albeit being niche languages in their own right).

My provocative two cents worth...

[nickbattle]

It would certainly be interesting to see, and hopefully understand any VDM-SL specification that SCSK maintain for VDM++. But I've only ever seen short sections of it. I think, in the past, CSK regarded that as their IPR rather than a public standard definition of VDM++ semantics. If that has changed, or is about to change, it could be interesting.

But unless we all adopt VDMTools (if that is open-sourced in future) we are looking at a very large job to re-implement "VDMJ" to follow the VDM-SL specification. And I assume VDM-RT won't be included in that spec.

We did submit the OO changes that I proposed in Workshop 8 to the LB as four RMs, as I recall. The minutes should have the details, but the conclusion was that they should be rejected, until "someone" could flesh out the details - the problem was, as I recall, that there are many subtleties and the LB could not solve them all in an obvious way. Given that the job of the LB isn't to solve issues, but rather to progress RMs, it was decided to reject them. That was on Nico's watch.

Perhaps if we want to discuss this further, we should use email rather than this bug! Or perhaps create a new issue to track the discussion?

[ldcouto]

Done and done. See https://github.com/overturetool/language/issues/34

[nickbattle]

Back to the original bug... this is almost working on Overture, but one of PJ's code generation tests has raised an interesting case. It is very similar to the example at the top of this issue, but this time the B class is a subclass of A, and the required operation on A|B is protected-inherited from A:

class A
operations
    protected op : char * nat ==> nat
    op (a,b) == return 1;
end A

class B is subclass of A
operations 
    public go : () ==> nat
    go () ==
    let obj : A | B = new B(),
            a : nat | char = 'a',
            b : nat = 2
    in
        obj.op(a,b);
end B

This gives a TC error, saying "obj.op(nat|char, nat)" is not in scope. The problem is that although the caller ("go") is in B, the pseudoclass created for A|B is not A or a subclass of A (it is called "*union_A_B"). Therefore the protected op method that A contains is not accessible outside the pseudoclass. Hence the error.

So... what to do? Is the union to be regarded as "the same as" all of its members, so that if any of its members call an operation on the union, they can see private/protected names? Or is it not legal to call a non-public operation on a union of classes?

VDMTools is happy with this spec.

[ldcouto]

Possible semantics would say that, as long as one of the members can call the op, then the union can call the op. Right?

/renews objections to possible semantics and op calls

[peterwvj]

Interesting, Nick. I tried this spec in VDMTools with op in A declared as private and VDMTools complains (reasonably) that obj.op(a,b) is an access violation. So if we decide to allow all members to be accessible outside the pseudo class then Overture and VDMTools will work differently for this particular case. Or am I not getting what you are saying?

[ldcouto]

Yeah, I think you're right Peter.

[tomooda]

Hmm, I think one possible semantics is "union_A_B.op is accessible if and only if both A.op and B.op are accessible in the caller's context." Am I missing something?

[tomooda]

I mean the stricter access control will be applied to the union of classes to satisfy subtype rule A <: union_A_B and B <: union_A_B.

[peterwvj]

Yes, I think what you are suggesting sounds reasonable. Is this what you are suggesting too, @nickbattle ?

[ldcouto]

I think...

The subtype rule will only came into play with POs. The type checker would let it pass. It's like assigning a union result to a variable of the type of one of its members.

Although, again, possible semantics and OO... not sure they should mix.

[tomooda]

Louis, yes, that sounds more compatible with other type checking rules of union types. So, the looser access control should be applied to the union of classes so that an instance of either A or B can serve the operation, I suppose?

[tomooda]

No, it won't fit with nominal type system.

[nickbattle]

At the moment, there are two checks performed in the creation of the pesudoclass. Firstly, as it goes through each class member of the union, it eliminates fn/ops that are not accessible by the caller. Then, if it collects more than one operation with the same name, it gives the resulting definition (which has the union of the parameter types) an access specifier that is the "widest" of the two. So a public and a private operation will merge to form a public one.

But in PJ's last codegen test, there is only one operation. So the result will be protected. But at the "x.op" call, the "union_A_B" does not appear to be "of type A or a subclass of A" so op is not in scope.

One solution might be, since the checks above have been performed, to make the resulting fn/ops in the pseudoclass all "public" (ie. unconditionally accessible), since if they weren't accessible by at least one class they would not have ended up in the union. (That's a pragmatic implementation rather than a view of the formal semantics!). That would solve the problem with PJ's test, I think.

[nickbattle]

And please don't ask about what happens with static and async. My head might explode... :-(

[nickbattle]

I've pushed the fixes that I have, including the "public" hack above, to ncb/development. There may be more problems in this area (and much discussion has been sparked), but I think the changes I have are an improvement and certainly "fix" the problems listed in this issue.

[ldcouto]

So, what did you end up going with? Most permissive possible semantics or?

[nickbattle]

Yes - well, the individual ops/fns access is checked and eliminated if they are inaccessible, but anything that gets through that becomes "public" (generally accessible) in the pseudoclass. So on the grounds that at least one of the class' members is accessible, the member in the union is. That's defensible :-)

[ldcouto]

I think so, although I would like @tomooda to comment on it. He seemed to have an objection regarding the nominal type system. To be honest, I don't see one but I'd like to know.

[nickbattle]

Though perhaps wider comments on the type system belong in the new LB discussion issue you created?