Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add lost qualifier to viewpointtest type checker #827

Open
wants to merge 30 commits into
base: master
Choose a base branch
from

Conversation

Ao-senXiong
Copy link
Member

@Ao-senXiong Ao-senXiong commented Aug 3, 2024

Fixes #576

@Ao-senXiong
Copy link
Member Author

Fixes #576

TODO: lost is not reflexive

@Ao-senXiong
Copy link
Member Author

Fixes #576

TODO: lost is not reflexive

This is implemented in 76a9f40, but how to improve the error message remain as a questions.

Copy link
Member

@wmdietl wmdietl left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

framework/tests/viewpointtest/LostNonReflexive.java Outdated Show resolved Hide resolved
@@ -17,6 +17,7 @@ void foo() {
void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) {
@A Object a = new @A VarargsConstructor(aObj);
@B Object b = new @B VarargsConstructor(bObj);
// :: error: (argument.type.incompatible)
@Top Object top = new @Top VarargsConstructor(topObj);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is a tricky one.
For other uses of Top, we want Lost as the result, because the actual receiver could be some subtype of Top.
E.g. in ref.m(x) if ref has static type Top, it could still point to an A object and we need to use Lost to avoid a confusion.

For constructor invocations, that argument doesn't hold - we always instantiate the object with the most concrete type - there is an actual Top object and invoking it with Top is okay.

This is different from PICO and Universes, where one can never have an object with concrete type Readonly.

I don't know what to do with this now... Maybe forbid creating Top objects? Or document that handling of Top is a bit inconsistent?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Forbid creating Top objects sounds good to me. Does it apply all systems that use viewpoint adapation?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not to all VP systems. But if VP with some qualifier results in Lost, that qualifier probably can't be created - Lost comes from not knowing some relationship. If one can create an object of that type, one knows the relationship.
So in this system, forbidding Top makes sense.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done!

@wmdietl wmdietl assigned Ao-senXiong and unassigned wmdietl Aug 19, 2024
@Ao-senXiong Ao-senXiong removed their assignment Aug 27, 2024
Copy link
Member

@wmdietl wmdietl left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for wrapping this up!

framework/src/test/java/viewpointtest/quals/Lost.java Outdated Show resolved Hide resolved
framework/src/test/java/viewpointtest/quals/Lost.java Outdated Show resolved Hide resolved
@@ -17,6 +17,7 @@ void foo() {
void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) {
@A Object a = new @A VarargsConstructor(aObj);
@B Object b = new @B VarargsConstructor(bObj);
// :: error: (argument.type.incompatible)
@Top Object top = new @Top VarargsConstructor(topObj);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not to all VP systems. But if VP with some qualifier results in Lost, that qualifier probably can't be created - Lost comes from not knowing some relationship. If one can create an object of that type, one knows the relationship.
So in this system, forbidding Top makes sense.

@wmdietl wmdietl assigned Ao-senXiong and unassigned wmdietl Oct 3, 2024
@Ao-senXiong Ao-senXiong assigned wmdietl and unassigned Ao-senXiong Oct 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Lost qualifier should be added to type systems with viewpoint adaptation functionality.
2 participants