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

Lost qualifier should be added to type systems with viewpoint adaptation functionality. #576

Open
AndrewShf opened this issue Sep 29, 2023 · 0 comments · May be fixed by #827
Open

Lost qualifier should be added to type systems with viewpoint adaptation functionality. #576

AndrewShf opened this issue Sep 29, 2023 · 0 comments · May be fixed by #827

Comments

@AndrewShf
Copy link
Member

AndrewShf commented Sep 29, 2023

Imagine a standard lattice like this:

      TOP
       |
       |
       v
A      B       RDQ
       |
       |
       v
     BOTTOM

where TOP is the top type in the lattice, BOTTOM is the bottom type in the lattice and RDQ (receiver-dependent-qualifier) is for viewpoint adaptation.

Suppose this type system also supports viewpoint adaptation and a piece of code written like this:

   class Demo {
     @RDQ Object f;

    void adaptation(@Top Demo top) {
        top.f = new @A Object(); // allowed
    }
   }

This looks fine, top.f has type TOP |> RDQ = TOP by the viewpoint adaptation law and thus can be assigned by a subtype object (the @A Object)

However, if the method is invoked like this, we would lost our type safety.

@B Demo o;
adaptation(o);

In the above code o has type B and o.f has type B as well but in the method invocation, the field is assigned to a type A object which is not a subtype of type B.

This problem could cause serious type safety issues in some type systems, for example, the immutability type system.
We could add a lost qualifier (which was introduced in the Generic Universe Type paper) as the type when the top qualifier looking at a RDQ qualifier. In that case if the variable has type lost, assignment operation is forbidden.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant