Ad hoc type restriction

[Brian Goetz]

> 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...
>       o 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
>       o 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...
>       o No explicit check of thenumber parameter is performed by the
>         dial() method (efficiency)
>       o Thedial() 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/20251014/301912f7/attachment-0001.htm>