Ad hoc type restriction

[Manu Sridharan]

 Hi all, regarding what the Checker Framework and similar tools can do:

WHAT I WANT: To be able to instead say this:
>
>     public void dial(@PhoneNumber String number) {
>         ... // do whatever
>     }
>
> AND have the following be true:
>
> At compile time...
>
>> I get a warning or error if any code tries to invoke dial() with a
>> "plain" String parameter, or assign a plain String to a  @PhoneNumber
>> String
>> There is some well-defined, compiler-sanctioned way to validate a phone
>> number, using custom logic I define, so I can assign it to a @PhoneNumber
>> String without said error/warning. Even if it involves @SuppressWarnings,
>> I'll take it.
>>
> At runtime...
>
>> No explicit check of the number parameter is performed by the dial() method
>> (efficiency)
>> The dial() method is guaranteed (modulo sneaky tricks) that number is always
>> a valid phone number
>>
> Obviously you can replace @PhoneNumber with any other assertion. For
> example: public void editProfile(@LoggedIn User user) { ... }
>
> Is the above possible using the checker framework? I couldn't figure out
> how, though that may be due to my own lack of ability.
>

This is all mostly possible via the Checker Framework and similar
approaches.  You wouldn’t need @SuppressWarnings annotations for validation
either, due to type refinement
<https://checkerframework.org/manual/#type-refinement>.  And, for this type
of property, where you’re essentially trying to introduce new subtypes of
an existing type and then enforce type compatibility at assignments, the
implementation effort to write the checker is pretty low.  And features
like generics would also be handled out of the box.

In terms of the “guarantee” that dial always gets a valid phone number,
that requires that all code executed at runtime was checked by the
checker.  If dial might get invoked by unchecked code (e.g., if it’s part
of the public API of some library), then some kind of runtime checks are
probably still needed inside dial.  (I’m assuming that reflection, dynamic
creation of classes, etc. count as “sneaky tricks” but those are also
potentially problematic.)

In terms of the challenges of running the Checker Framework / barriers to
adoption: adding the Checker Framework to your build is not too hard; it’s
just another annotation processor plus the corresponding flags to enable /
configure the checks you want.  As implemented the Checker Framework can
introduce a significant build-time overhead (potentially 5X or greater),
which may be too much to incur on every compile.  This is not fundamental;
NullAway takes a similar approach and we measured the overhead to be around
10%.  But reducing overhead of the Checker Framework itself may require
significant work.  One can run the Checker Framework in a CI job separate
from the normal build, but this delays feedback to the developer.

Honestly I think the biggest barrier to adoption is writing the necessary
annotations to get the checker to initially pass; for an extant large code
base this can be significant work, depending on the property.  There is
research on inferring these annotations for existing code bases (paper 1
<https://kelloggm.github.io/martinjkellogg.com/papers/ase2023-camera-ready.pdf>,
paper 2 <https://manu.sridharan.net/files/FSE23Practical.pdf>).

Best,
Manu

On Oct 14, 2025 at 18:09:46, Brian Goetz <brian.goetz at oracle.com> wrote:

> There's nothing wrong with annotations being scanned by frameworks.
> Indeed, the entire point of annotations is to allow code authors to
> decorate source declarations with "structured comments" in a way that is
> scrutable, both statically and dynamically, to frameworks and tooling*.
> What annotations are _not_ for is to impart semantics _at the Java language
> level_.  Annotation plumbing is a service the language and compiler perform
> for the benefit of libraries and frameworks, but it recuses itself from
> being a beneficiary of that service.
>
>
> (*At this point someone will typically pipe in "But the compiler is a
> tool.  Ha!  I am very clever."  But remember, the Java compiler has no
> discretion whatsoever about program semantics.  That discretion belongs
> purely to the language specification.)
>
> On 10/14/2025 8:49 PM, Olexandr Rotan wrote:
>
> The next question in this dialog (which I've only had a few zillion times)
>> is "what about frameworks that use reflection to drive semantics."  But
>> that one kind of answers itself when you think about it, so I'll just skip
>> ahead now.)
>
>
> Just out of curiosity, what was the motivation behind the annotations with
> runtime retention if they are not expected to be scanned for by frameworks?
> Even if talking about things like aspect-oriented programming, if advice
> does not alter the behaviour of the invocation, it will most likely be
> designed to produce some side-effect, which is also a semantics change
>
> On Tue, Oct 14, 2025 at 7:32 PM Brian Goetz <brian.goetz at oracle.com>
> wrote:
>
>> WHAT I WANT: To be able to instead say this:
>>
>>     public void dial(@PhoneNumber String number) {
>>         ... // do whatever
>>     }
>>
>> AND have the following be true:
>>
>>    - At compile time...
>>       - I get a warning or error if any code tries to invoke dial() with
>>       a "plain" String parameter, or assign a plain String to a  @PhoneNumber
>>       String
>>       - There is some well-defined, compiler-sanctioned way to validate
>>       a phone number, using custom logic I define, so I can assign it to a @PhoneNumber
>>       String without said error/warning. Even if it involves
>>       @SuppressWarnings, I'll take it.
>>    - At runtime...
>>       - No explicit check of the number parameter is performed by the
>>       dial() method (efficiency)
>>       - The dial() method is guaranteed (modulo sneaky tricks) that number
>>       is always a valid phone number
>>
>> Obviously you can replace @PhoneNumber with any other assertion. For
>> example: public void editProfile(@LoggedIn User user) { ... }
>>
>> Is the above possible using the checker framework? I couldn't figure out
>> how, though that may be due to my own lack of ability.
>>
>>
>> Yes, but you get no implicit conversion from String to @PhoneNumber
>> String -- you have to call a method to explicitly do the conversion:
>>
>>     @PhoneNumber String validatePhoneNumber(String s) { ... do the thing
>> ... }
>>
>> This is just a function from String -> @PN String, which just happens to
>> preserve its input after validating it (or throws if validation fails.)
>>
>> A custom checker can validate that you never assign to, pass, return, or
>> cast a non-PN String when a PN String is expected, and generate diagnostics
>> accordingly (warnings or errors, as you like.)
>>
>> But even if it is possible via checker framework or otherwise, I don't
>> see this being done in any widespread fashion, which seems like pretty
>> strong evidence that it's too hard.
>>
>>
>> It's not that hard, but it _is_ hard to get people to adopt this stuff.
>> Very few anno-driven type system extensions have gained any sort of
>> adoption, even if they are useful and sound.  (And interestingly, a corpus
>> search found that the vast majority of those that are used have to do with
>> nullity management.)
>>
>> Why don't these things get adopted?   Well, friction is definitely a part
>> of it.  You have to set up a custom toolchain configuration.  You have to
>> do some work to satisfy the stricter type system, which is often fussy and
>> annoying, especially if you are trying to add it to existing code.  You
>> have to program in a dialect, often one that is underspecified.   Libraries
>> you use won't know that dialect, so at every boundary between your code and
>> library code that might result in a new PhoneNumber being exchanged, you
>> have to introduce some extra code or assertion at the boundary.  And to
>> many developers, this sounds like a lot of extra work to get marginally
>> increased confidence.
>>
>> There is similar data to observe in less invasive static analysis, too.
>> When people first encounter a good static analysis tool, they get really
>> excited, it finds a bunch of bugs fairly quickly, and they want to build it
>> into their methodology.  But somewhere along the line, it falls away.  Part
>> of it is the friction (you have to run it in your CI, and on each developer
>> workstation, with the same configuration), and part of it is diminishing
>> returns.  But most developers don't feel like they are getting enough for
>> the effort.
>>
>> Of course, the more we can decrease the friction, the lower the payback
>> has to be to make it worthwhile.
>>
>> But I think it's OK for certain "sticky notes" to be understood by the
>> compiler, and have the compiler offer corresponding assistance in verifying
>> them (which it is already doing - see below). I also agree that having
>> annotations affect the generated bytecode ("runtime semantics") is a big
>> step beyond that, but maybe that's not necessary in this case.
>>
>>
>> There are a few "sticky notes" that the "compiler" does in fact
>> understand, such as @Override or @FunctionalInterface.  (I put "compiler"
>> in quotes because the compiler doesn't get to have an opinion about
>> anything semantic; that's the language spec's job.)  But these have a
>> deliberately limited, narrow role: they capture scrutable structural
>> assertions that require (per language spec!) the compiler to statically
>> reject some programs that don't conform to the assertions, but they never
>> have any lingusitic semantics for correct programs.   That is, for a
>> correct program P with annotations, stripping all annotations out of P MUST
>> produce a semantically equivalent program.  (The next question in this
>> dialog (which I've only had a few zillion times) is "what about frameworks
>> that use reflection to drive semantics."  But that one kind of answers
>> itself when you think about it, so I'll just skip ahead now.)
>>
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20251015/fbb184d3/attachment-0001.htm>