[Checkers] Type Declaration Qualifiers

[Michael Ernst]

Mahmood-

Thanks for bringing this up.

> For a given type declaration 'class @Interned Foo { ... }', the  
> Interning checker assumes that 'Foo' and '@Interned Foo' are  
> equivalent.  In other words, every use of Foo is actually '@Interned  
> Foo'.

There is a slightly different way to look at this, as syntactic sugar.

Let's ignore for the moment that every use of 'Foo' is actually '@Interned
Foo'.

Every use of Foo in the program must be of @Interned type.  A declaration
such as "Foo myFoo;" is illegal; only "@Interned Foo myFoo" is legal.
However, it seems unhelpful to users that the short form is illegal and the
long form is always required.  Therefore, the checker can be viewed as
transforming every use of "Foo" into "@Interned Foo" and then proceeding
with type-checking as normal.


how to write in    how to write with
original syntax    syntactic sugar     meaning            effect

Foo                n/a                 any Foo, whether   type error
                                       interned or not

@Interned Foo      Foo                 an interned Foo    OK

n/a                @Interned Foo       an interned Foo    syntax error (to
                                                          avoid confusion)


So the syntactic sugar transforms the second column into the first column,
and then type-checking proceeds as usual.

I don't know whether this should be considered part of the "implicit type
qualifier" from section 2.6 of the Checker Framework Manual, or part of the
default, or some other special-case mechanism.  It feels like it might
possibly be useful in other type systems.

In this interpretation, the meanings of the @Interned and @Mutable type
qualifiers on a declaration may not be so very different, though the syntax
is treated differently on uses.  And I concede that this may not be at all
obvious and should perhaps be better documented in the manual.

Does this make sense?  I may still be missing something.

> How should one express that a type cannot be Immutable?

Can you give a use case for when one would want to say this?  It seems that
doing so would foreclose some useful code idioms.  I may wish to specify
that a given value should not be mutated, even if it's of a mutable type.
And, I may wish to subclass a given class and override all the setters.

                    -Mike