[JSR308] ELTS vs. ARRAY syntax for array annotations

[Michael Ernst]

Igor's message raised an interesting point, on which I would like to
solicit more discussion:

> I believe principle P1 is more important for readability than
> principle P3.


Recall that section B.3 of the proposal states three principles for
the array syntax:

  P1:  Adding array levels should not change the meaning of existing
  annotations.  A textual subpart of a declaration should describe a
  type that is part of the declared type.

  P2:  When two variables appear in a variable declaration, the
  annotations should mean the same thing for both variables.

  P3:  Type annotations before a declaration should refer to the full
  type, just as variable annotations (which occur in the same position
  -- at the very beginning of the declaration) refer to the entire
  variable.

For details, see the proposal: http://groups.csail.mit.edu/pag/jsr308/.

The ELTS syntax (an annotation on brackets refers to the elements)
violates principles P1 and P2.  The ARRAY syntax (an annotation on
brackets refers to the array) violates principle P3.

I would really like to see a syntax that satisfies all the principles,
and that programmers find appealing and in the spirit of Java.  That
doesn't seem possible.  Here are some alternatives:

 * Use ARRAY syntax.  Violate P3.
 * Use ELTS syntax.  Violate P1 and P2.
 * Forbid array annotations.  Case studies on checkers that do and do
   not support array annotations convince me that these are important.
   For example, see section 6 (pages 7-8) of the technical report
     Pluggable type-checking for custom type qualifiers in Java
     http://people.csail.mit.edu/mernst/pubs/custom-types-tr047.pdf
 * Use fully postfix syntax.  I have received many private comments
   that this violates the feel of the Java language, but it is still a
   possibility that has not been ruled out.

I have flip-flopped between the ARRAY and ELTS syntax; neither is
perfect, but they do seem better than the alternatives.  The question
is which is better than the other.  I solicit more comments on this
matter.  (I am not as concerned about the IN-vs-PRE-vs-POST decision,
but perhaps it is linked to the ARRAY-vs-ELTS decision.)


I would ask everyone who responds to show restraint in stating that
one of the syntaxes is "more natural" or "easier for programmers to
understand" than the others.  Over a year ago, I did a very
unscientific study:  I walked around my building asking people in my
building the meaning of annotations like "@Readonly Date[]".  To my
considerable surprise, there was an almost perfect 50-50 split between
the people who chose the ARRAY and the ELTS interpretation.  All of
those people, when the other interpretation (and the principle it
supported) was explained to them, were able to understand the logic
behind it.  We have actually changed our implementation between the
two meanings, and it's been easy to interpret the array annotations
both before and after.  So I believe that both syntaxes are workable
and can become intuitive to programmers.

That said, examples of the syntax can be helpful.  As another note,
I've found that sometimes different annotations lead to different
intuitions (e.g., @Length vs. @Readonly vs. @NonNull), so we should
consider a variety of possible annotations.

                    -Mike