Ad hoc type restriction

[Archie Cobbs]

On Thu, Oct 30, 2025 at 9:38 PM Rob Ross <rob.ross at gmail.com> wrote:

> Contracts, `runtime` and `compile time`...
>

All good thoughts.

   1. Strongly-typed languages like Java are favored for complex
   programming tasks because of the rich tools they provide to programmers
   allowing one to prove to oneself that the code's behavior will be correct.
   This is Java in a nutshell!
   2. In general, such tools will operate at *both* compile/build time and
   runtime - and they should do so in a coherent way.

The observation I'm trying to make in this thread is: Java gives its own
tools the ability to operate seamlessly across both domains (compile-time
and runtime) but it makes it difficult for the programmer to add their own
tools that operate seamlessly across both domains.

Heck, even the compile-only tools are difficult - for evidence of this,
count how many import com.sun.tools.javac... statements there are in
the checker framework...

For example, in Java I can say: Foo x = (Foo)y; This will be checked at
both compile time (is the compile-time type of y ever assignable to Foo?)
and at runtime (CHECKCAST). Moreover it's necessary that it be checked at
both compile-time and at runtime because at compile-time we have some, but
not all, of the relevant information. Since we want errors to be detected
as soon as possible, we detect what we can at compile time and leave the
rest to runtime. These two checks are really the same check, just spread
across two different domains - they are "coherent".

In an ideal world, I should be able to define my own custom type
restriction, with both compile-time and runtime components, and have it
checked coherently at both compile-time and runtime.

An experiment I'm working on (very slowly) is to determine how hard it is
to create such a tool using what we have today.

The least clunky plan I've come up with so far is:

1. Create a new meta-annotation (e.g., @TypeTag) that you would use like
this:

  /**
   * Annotates declarations of type {@link String} for which
   * the value must be non-null and a valid E.164 phone number.
   */
  @Target(ElementType.TYPE_USE)  @TypeTag(appliesTo = String.class,
validatedBy = PhoneNumberChecker.class)
  public @interface PhoneNumber {
  }

2. Create a checker framework plugin extending the Subtyping checker that
does the user-defined type restriction stuff at compile time (e.g.,
@PhoneNumber
String x)
3. Create a bytecode analyzer that looks for CAST
RuntimeInvisibleTypeAnnotations and inserts corresponding runtime checks
(e.g. PhoneNumberChecker.check(x))
4. Require both of the above to be included in your build (maybe they could
be wrapped into a single maven plug-in?)

-Archie

-- 
Archie L. Cobbs
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20251031/9c9ef5c1/attachment-0001.htm>