Pluggable Types on Lambda-the-Ultimate
Interestingly, Erik Meijer had an interesting post on optional/pluggable types on Lambda-The-Ultimate. It’s provoked quite a response, which is fun to read. Besides, it has the nicest title I've ever seen.
Erik has roots in the Haskell community, but he’s been very open minded on typing issues (certainly more open-minded than me!), has changed his views on the subject over time, and says so publicly. He deserves a lot of credit for that.
One point I'd like to add is that the pluggable types hypothesis has two elements to it. The more controversial one is that mandatory typing should be avoided altogether. The second is that one should be able to plug in additional type systems. This latter point applies even to when one does have a mandatory type system, as is the case in Java. Even hard core type theorists have some interest in this point, since it means that new and valuable type systems can get used in practice, without the huge hurdle of getting them to be part of a language definition.
Posted at 12:16AM Feb 18, 2006 by gbracha in Java |
Annotations: Toward Pluggable Types
One of the new language constructs introduced in Java 5 was annotations. The potential of this feature is larger than many people realize. At the same time, like any construct, it is open to abuse. Hence this blog entry.
One of the more interesting things one can do is define annotations that support optional static analyses. For example, consider an annotation like @NonNull, that signifies that a variable should never hold null. If this annotation is used consistently, a tool can check that such variables indeed never become null at run time. You could say good bye to null pointer exceptions!
This is just one example (albeit, perhaps the most important one) of annotations being used to define an optional type system. It is very important to understand what one can and cannot accomplish in this way.
Since I like being negative, let me start by saying what you cannot do:
You cannot change the run-time behavior of the program
You cannot prevent an otherwise legal program form compiling or executing
Annotations can never be used to change the semantics of a program, or to cause compilation to fail. All annotations do is attach information (metadata) to parts of the program. Tools can then interpret the metadata as they see fit; however, the meaning of a program is fixed by the Java language specification, and cannot be altered.
Occasionally I get asked where in the specs is this stated. The answer, of course, is that the specs don’t have to state any such thing. They already give a definition of what any piece of source code means, and a conformant Java compiler must abide by that specification, and cannot change that meaning.
The fact that a program means the same thing everywhere is at the core of the value proposition of the Java platform. Everyone can read a program and understand what it is going to do; the meaning doesn’t change because of a given installations preferences, local libraries or configurations. That is what helps the Java programming language be such a valuable lingua franca across the industry.
Now, on the positive side, you can plug in a wide variety of semantic analyses or type systems, and get reports on potential errors in your programs. Optional type systems are type systems where the type annotations are syntactically optional, and (more important) the types never influence run-time semantics. Optional types are a perfect fit with annotations.
By definition, one can’t dynamically test for an optional type property of an object. While this may seem to be a limitation, the fact that optional types don’t effect the run time means that different optional type disciplines can co-exist without interacting with each other. That means you can plug in multiple, distinct analyzers/tools//typecheckers. This has the potential to enable pluggable
types.
The annotation system may need a bit of a boost in some cases, because an analyzer may need annotations not just on declarations, but on additional language constructs.
For example, the Javari research project at MIT, which allows you to distinguish between ordinary and read-only references, would require annotations wherever types can appear (including casts and type parameters, which are not currently supported).
In principle, it would be nice if you could attach annotations to every node in the abstract syntax tree. Indeed, even comments could be viewed as annotations. As Michael Van de Vanter has noted, if comments are treated as meaningful metadata belonging to well defined nodes in the AST, refactoring tools can preserve them reliably. However, adding annotations at essentially arbitrary program points poses significant syntactic challenges, so don’t expect that anytime soon.
Posted at 08:17PM Feb 16, 2006 by gbracha in Java | Comments[11]