[JSR308] annotations as arguments to annotations

[Jonathan Aldrich]

Dear JSR 308 team,

First, I'd like to express my appreciation to Michael and the JSR 308 
team for their work in improving the Java annotations system!  My 
students are all using JSR 175 annotations in our static analysis 
research, but have found them to be sorely lacking, and JSR 308 
addresses many of the issues.

I think one addition, however, would really increase expressiveness in a 
major way: allowing arbitrary annotations as arguments to annotations. 
This is mentioned in Section D.4.2. of the current JSR 308 proposal, as 
a possible extension that is currently out of scope.  I would argue we 
should add it to the scope of the proposal.

The main benefit of this is that it allows one to define little 
recursive data structures with annotations.  Annotation constants are 
useful, but if you want to describe any interesting type system--which 
is a very common mode of usage for annotations--it's very likely that 
you'll want this.  There are two basic use cases: type parameterization 
and structured annotations.


1) Type Parameterization.  Every interesting type system has 
parameterization, because of the reasoning it enables in the case of 
reused library code.

Of course, JSR 308 allows you to annotate type parameters directly. 
That's really important and convenient, but it doesn't solve the problem 
in the general case.  In particular, the type system you are layering on 
top of Java using annotations may require parameters in different places 
than Java's.  In that case, the JSR 308 support doesn't help you, unless 
you want to add a gratuitous type parameter to Java (almost certainly a 
bad idea).  In fact, allowing annotations as arguments to annotations is 
expressive enough that it can simulate JSR 308's support for annotating 
type parameters.  Thus from an expressiveness point of view, annotations 
as annotation arguments is more important that annotating type 
parameters (but of course annotating type parameters is still really 
valuable from a usability perspective).

To illustrate the need for this feature, imagine you have a little 
effect system for tracking whether code does I/O, and you want to encode 
this with annotations.  An IO method might be written as:

@IOEffect void println(String data);

Whereas a method without an IO effect might be written:

@NoIOEffect int computeIt(int data);

Now let's say you've got a Listener interface with a single callback 
method.  The callback method in the Listener interface may or may not 
have effects, so we want to have an "effect parameter" on the Listener 
that expresses whether the callback has I/O effects.  That way the 
interface can be reused across implementations that are effectful or 
not.  The declaration might be:

@IOEffectParam("E") interface Listener {
      @IOEffectParam("E") void notify();
}

Now, we there are several ways we might use the listener:

@IOEffectActual(@IOEffect) Listener effectfulListener = ...;

@IOEffectActual(@NoIOEffect) Listener notEffectfulListener = ...;

@IOEffectActual(@IOEffectParam("F")) Listener effectDependsOnContext = ...;

In the first case, the listener's callback method has an effect, in the 
second it doesn't, and in the third it may have one depending on some 
effect parameter "F" that is currently in scope.

Note that the Listener class, like many Java listeners, doesn't have or 
need type parameters.  We're using parameterization in the IOEffect type 
system in a place where there's no parameterization in the underlying 
Java type system, so we can't just piggyback on Java's generics.

If JSR 308 doesn't support this, the only way to simulate it is going 
out of the type annotation system by encoding parameters in strings. 
All of my annotation based research projects are doing this right now, 
but it's really ugly, and takes away a lot of the benefits that 
annotations were supposed to yield.  You start getting annotations like:

@OwnedBy("unique<A<shared>,owned>")

(This example is from our ownership system; here the pointer is unique, 
but the type has two ownership parameters, one of which is owned by the 
ownership parameter A and the other is owned by the "owned" domain, and 
the thing that is owned by A has its own parameter which is owned by the 
global "shared" domain.  See my student Marwan's paper in IWACO '07 for 
details...it's truly ugly.  JSR308 will help the cases where the 
ownership and type parameters match, but we know there are many cases 
where there are ownership parameters that are not type parameters, and 
in these cases we'll still have to use the string hack.)

For the effect type system described above, the situation isn't quite as 
bad as this--mainly because the type system itself is dead simple--but 
you still get a frustrating system where you have to write actual 
parameters in string notation whereas concrete declarations are 
annotations.  In other words, you write things like:

@IOEffect void println(String data);
@IOEffectActual("IOEffect") Listener effectfulListener = ...;

and it's highly annoying that "IOEffect" can't be written as @IOEffect 
as it is when it's directly on a method.

I'm speculating here, but I think if you look at the proposals for using 
annotations as a type refinement mechanism, you'll find that most of 
them need type parameterization to handle real programs well, and you'll 
also find plenty of examples where the type refinement needs to 
parameterize in ways that don't match Java's type parameterization. 
We've found that's certainly true for ownership types.  I suspect lots 
of people are going to need this, even if they haven't tested their type 
system on enough real-world examples to realize it yet, and we're sure 
to regret it if we don't put it in the spec.



2) Structured Annotations.  Sometimes annotations themselves have an 
interesting internal structure.  Again, this internal structure could be 
represented as strings, but if a concept can be either an annotation 
directly on a declaration or part of a more complex annotation, it's 
much cleaner to represent it as an annotation in both cases.  For 
example, one could imagine encoding a logic quite nicely:

@Implies(@Predicate("I think"), @Predicate("I am"))

instead of

@Formula("(I think) => (I am)")

We have a real (research) application of this in my group: the 
lightweight typestate verification system my student Kevin Bierhoff is 
developing (see his OOPSLA '07 paper) requires little linear logic 
formulas to be embedded in annotations.  An implementation based on JSR 
175 would use strings, but it would be nicer to use @Annotations to 
express the internal structure.


------------------


I'm really curious about why this feature was not supported in the 
original spec; it seems like an "obvious" extension but perhaps the 
developers of JSR 175 didn't see the compelling benefits for 
representing type refinement systems, or were uncertain about whether it 
might cause implementation issues.  If anyone has insight I'd be 
interested to hear it.

I don't see any immediate "gotchas" in implementing such a proposal but 
I'd be happy to lead or contribute to an experimental implementation to 
be sure.

Thanks,

Jonathan