[JSR308] A simple proposal for recursive annotations

[Dr. James J. Hunt]

Dear Jonathan,

The idea of the recursive annotation proposal was not to make "the
annotation language to be significantly more sophisticated than the
annotated language."  Currently, the annotation language is quite weak,
so the proposal would add a bit of expressive power to annotations.

The idea is also not to define a "programming language within program
language" as the other poster suggested.  The whole idea of a
specification language for formal verification was just an example of
what could be done with a simple extension for subtypes and recursion in
annotations.  The formulation of such a language would be a subject for
another JSR.

Note that one can already nest one annotation in another:

public @interface A
{
  public B value() default @B;
}

public @interface B
{
  public int value() default 0;
}

Just not recursively:

public @interface A
{
  public B value() default @B;
}

public @interface B
{
  public A value() default @A; // Error due to cycle
}

So nested annotations is not the same thing.

There are really only two changes being proposed: enable single
inheritance among annotations and allow indirect recursion within
annotation definitions.  With these two facilities, one could write much
more powerful type refinement systems, without much additional
complication to the annotation syntax.

In the language, one would need to allow for extends in @interface
statements; the circular annotation check would have to be modified a
bit; and a reference for the parent annotation would be needed in the
class file.  These issues are best delt with once one has implemented
the changes.

As for using Java syntax for annotations, that is perhaps desirable, but
more difficult to implement.  You example is too short for me to see if
what you intend would work for a specification language.  It would be
nicer to write something like

@Spec("\require i >= 0 && i < a.length();
       \ensure \result == elements[i];")

instead of

@Spec(require = [@Eval(value = ">=",
                       args = [@Value("i"), @Int(0)])
                 @Eval(value = "<", 
                       args = [@Value("i"),
                               @Invoke(value = "length",      
                                       args = [@Value("a")])],
      ensure = [@Eval(value = "==",
                      args = [@Result,
                              @Element(value = "elements",
                                       index = @Value("i"))])

but parsing this in downstream tools, i.e. tools that no longer have
access to the source code, would be challenging in practice, since the
parse context of the expression would no longer be available.

The advantage of the second form is that the parsing is done by the
annotation parser.  All new constructs are defined in a consistent manor
via annotation definitions.  No changes need to be made to the tools.

That is not to say, that one could not have a preprocessor that converts
the first form into the second at the source level.  In fact, that would
be possible with this proposal, but JSR 308 does not have to define such
a parser.  One could even use annotations on the annotations to help
build the the preprocessor.

Using Java like syntax as you propose does not address the issue of
subtype refinement either.  There are interesting uses for numerical
calculation checking when one can tag the units used and understand
their relationship.  For example, if @Meter and @Square are both
subtypes of @UnitExpression, then one could check things like whether
the cast below is correct or not, even at the byte code level.

public @Unit(@Square(@Meter)) int area(@Unit(@Meter) int length,
                                       @Unit(@Meter) int width)
{
  return (@Unit(@Square(@Meter)) int)length * width;
}

Mixing units would be easy to catch.

Remember, that adding this feature does not force you to use it in your
code, but it does enable useful features for software verification.

Sincerely,
James
 

On Mon, 2009-06-08 at 12:22 -0400, Lex Spoon wrote:
> On Jun 7, 2009, at 11:11 PM, Jonathan Aldrich wrote:
> > > > (because the annotations in the static checking system may be
> > > > parameterized in different ways than Java type
> > > > parameterization).
> > > I admit this strikes me the same way as it struck an earlier
> > > poster.  It looks like a bad trajectory for the annotation
> > > language to be significantly more sophisticated than the annotated
> > > language.
> > 
> > Sorry, I wasn't proposing anything more than just the ability to
> > build up annotations recursively, like any recursive data structure
> > in Java. It turns out that's enough to encode parameterization in
> > annotation-based type systems.  If you thought I was proposing
> > adding "native type parameters" to annotations, well, that would be
> > interesting but as you say is clearly outside the scope of the JSR.
> > 
> > 
> > For examples of where you might want to encode "annotation
> > parameters" in different places in a library than already have type
> > parameters, see my earlier message to the list.
> 
> 
> I presume you are talking about this thread from October:
> 
> 
> https://lists.csail.mit.edu/pipermail/jsr308/2008-October/000487.html
> 
> 
> I have now read the above message.  I thought a few days ago that you
> meant some form of self-referential annotations.  Instead, you seem to
> be talking about allowing annotations to be used in places where
> literals are currently required.  I might have chosen "nested
> annotations" to avoid the self-referential connotation, but let's go
> with recursive.  Indeed it's a narrower scope than I realized.
>  However, my conclusion is the same.  Let's dig in.
> 
> 
> I agree with you that there is a welcome expressiveness increase in
> what you describe.  The examples you give remind me strongly of recent
> ETHZ work on "universe" types, and that work certainly benefited from
> Scala's analogous features.  However, I still think a language is
> better served if its annotation language reuses the core language's
> expression language rather than designing its own.  The main benefit
> is one of orthogonality, although it also looks like less work.
> 
> 
> First let's consider whether it's sufficient.  As far as I can tell,
> using expression forms such as new expressions and array literals
> would suffice for your use cases, just as they sufficed for the
> Universe types group.  What do you think?  The recipe is
> straightforward: imagine Java syntax to construct the type, and then
> change the initial "new" to "@".
> 
> 
> For example, here is a sequence based on an example from the October
> email:
> 
> 
> @OwnershipArgs({@Shared}) // recursive annotations
> new OwnershipArgs(new Shared()) // run-time type
> @OwnershipArgs(new Shared()) // expressions within annotations
> 
> 
> 
> 
> I believe this example works out fine.  Can you think of examples
> where the expressions approach would be problematic?
> 
> 
> Sufficiency is not the only issue, of course. Let's look at the two
> you raise here:
> 
> 
> 
> 
> > > If the annotation language seems too constraining, I would propose
> > > what we did for Scala's annotations.  Specifically, Scala allows
> > > arbitrary expressions to be embedded within the annotations.  That
> > > approach keeps the annotations group from becoming a
> > > general-purpose language design group, it allows a very general
> > > language of annotations, and it provides synergy with the
> > > underlying language.  As one example of this synergy, someone
> > > designing an a set of annotations can arrange that evaluating the
> > > embedded expression would give a run-time representation of an
> > > equivalent type.
> > 
> > That would be great, both in terms of expressiveness and a nicer
> > syntax for saying complex things.  But I think it would also be a
> > much bigger change than recursive annotations, which are uglier
> > syntactically but can at least express what you want....
> 
> 
> I have the opposite conclusions: the ones you propose are better
> syntax, but take more work.  I wonder where we are not matching up in
> our analysis?
> 
> 
> For the quality of the syntax, I believe the October email is better,
> especially for array literals.  However, it strikes me as ideally
> something better taken up in the core language.  For example,  Java
> could allow  "new Foo" if the constructor has no parameters.
>  Also, Java could allow "{foo1, foo2}" as an array whenever the
> context makes the array type clear.  Is the core language sufficiently
> stuck that the annotations group is ready to vote no confidence on it
> and make our own?
> 
> 
> For the necessary amount of work, much of the appeal to me is to reuse
> existing design work!  All that is needed for the expressions version
> is to decide on how to pickle the information into class files and to
> extend the API to give access to the information.  The October email
> implies strictly additional work: designing the new syntactic forms
> for annotations themselves.
> 
> 
> Perhaps I can provide one clarification that I didn't mention in my
> last email.  It is certainly not necessary to allow *all* Java
> expressions.  In particular, drop anonymous inner classes.
> 
> 
> 
> 
> 
> 
> > > All this said, it first seems important to accomplish 308's main
> > > task of allowing annotations on types at all.  Extending the set
> > > of annotations is a further step beyond the main scope, isn't it?
> > 
> > There are a set of annotation expressiveness tweaks already in the
> > proposal which are not directly "allowing annotations on types" but
> > are supportive of that.  I'd put recursive annotations in that
> > category, with the justification of encoding annotation
> > parameterization and/or mimicking/shadowing the existing (recursive)
> > structure of types in Java.  It's a judgment call--but my sense is
> > that if we can figure out the details, this is a high-value addition
> > and is as well in scope as other items in the current proposal.
> 
> 
> My mistake.
> 
> 
> Overall, I believe I now see what you are getting at with
> expressiveness.  It still strikes me as a helpful finesse, though, to
> reuse the core language's expression syntax rather than design a new
> one.
> 
> 
> Lex
> 
> 
-- 
Dr. James J. Hunt      * CEO aicas group       * Tel: +49 721 663968 22

aicas incorporated
69 West Rock Ave.      * New Haven, CT 06515   * USA
http://www.aicas.com   * Tel: +1 203 676 9807  *

Business Filing Number: 0002879819, State of Connecticut
President: Dr. James J. Hunt, Secretary/Treasurer: David P. Reddy

aicas --- allerton interworks computer automated systems GmbH
Haid-und-Neu-Straße 18 * D-76131 Karlsruhe     * Deutschland (Germany)
http://www.aicas.com   * Tel: +49 721 663968 0 * FAX: +49 721 663968 99

USt-Id: DE216375633, Handelsregister HRB 109481, AG Mannheim
Geschäftsführer: Dr. James J. Hunt