[JSR308] A simple proposal for recursive annotations

[Lex Spoon]

On Jun 16, 2009, at 12:12 PM, Dr. James J. Hunt wrote:
> 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];")


My proposal was to embed the expressions directly, rather than in a  
string.  That way, it's the Java compiler that does the parsing and  
type checking.  It already has subroutines for that, so it can easily  
do so.  The annotation processor is then provided an abstract syntax  
tree.

Presuming annotations worked that way, you could write the above spec  
like this:

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

Doesn't that look sufficient?


Note that several things must be in scope for this example to work,  
but it doesn't seem like any trouble.

1. "require", "ensure", and "result" must be in scope.  They could be  
imported from static members of a utility class.

2. "i" and "a" must also be in scope.  This initially struck me as  
weird, when I was first thinking about these problems for Scala, but  
over time I came around to allowing it.  It's just too common to want  
to annotate a method and talk about it's parameters.


> 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.

That way works.  However, if you use expressions instead of nested  
annotations, you already get inheritance for free, which is an example  
of what I'm getting at.  If the system makes the single decision to  
reuse the expression language and its type system, then a lot of  
useful expressiveness is inherited (so to speak) by the annotation  
language.

It so happens I have tried out this approach on units, and it  
certainly works for basic examples like the above area method.  By the  
way, I really do like the units example.  It's statically checkable,  
but you can't check it with standard type systems.  Here's the source  
code for my proof of concept:

http://lampsvn.epfl.ch/svn-repos/scala/compiler-plugins/units/trunk

Here is a blog article by someone else showing what it's like to  
install and use the system; it looks similar to JSR 308's goals:

http://www.michaelnygard.com/blog/2009/05/units_of_measure_in_scala.html


In this units system, I used Andrew Kenedy's terminology.  He calls  
9.8 m/s^2 a "measure", whose "scale" is 9.8 and whose "unit" is m/ 
s^s.  In turn, the unit m/s^s has a "dimension" of length/time*time.   
Given this terminology, a "units checker" is really a checker of  
*dimensions*.

To see what the annotations look like, here is a simple example from  
StandardUnits.scala:

  val kg : SimpleUnit @dim(Mass) =  SimpleUnit("kg", Mass, 1.0E3)
This says that the kg unit is of type SimpleUnit @dim(Mass).  This  
type has an annotation, @dim(Mass).  The body of that annotation is an  
arbitrary Scala expression, in this case simply "Mass".  That  
expression could also be usefully evaluated at run time, although  
that's a choice that must be made for any library of annotations.

Here's a more complicated example:
  val J: UnitOfMeasure @dim(Length*Length*Mass/(Time*Time)) =  
unitOf(N*m)

This time, the dimension is Length*Length*Mass/Time*Time.  Again, this  
can be evaluated at a Scala prompt, and similar evaluations take place  
for the run-time checks that the system also allows.

I see no reason this wouldn't work in Java.  It's a simple  
rearrangement of the above code to yield the same thing in Java:
   public static final SimpleUnit @dim(Mass) kg = SimpleUnit("kg",  
Mass, 1.0E3)
   public static final UnitOfMeasure  
@dim(Length.times(Length).times(Mass/(Time.times(Time)))) = unitOf(N *  
m)


Likewise, the area method converts fine:

public Measure @dim(Length.times(Length)) area(Measure @dim(Length)  
length, Measure @dim(Length) height) {
   return length * height;
}

Granted, you might want to tweak the language of dimensions for Java.   
For example, instead of the ugly times() method, you might add a  
square() method:

public Measure @dim(square(Length)) area(Measure @dim(Length) length,  
Measure @dim(Length) height) {
   return length * height;
}



What do you think, James?  Does it look sufficient for units checking  
to allow expressions in the annotations?


Overall, I had meant just to make a little suggestion, but I confess  
this is turning into a real proposal.  Where do things stand now?  If  
there is really pressure to extend the annotation language to support  
things like preconditions, postconditions, and units, then I confess I  
really do propose using Java expressions.  It looks much better to me  
than the alternative of adding multiple extensions to the annotation  
language and still not having as much expressiveness.  I would be  
happy to help out, for example by contributing a reference  
implementation, but I will wait to hear where things are before  
putting any more time into it.


Lex

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.csail.mit.edu/pipermail/jsr308/attachments/20090616/a589b132/attachment.htm