robjsoftware.info

Warning: rambling language research post ahead!

I admit it, I am a static typing weenie. Having gotten hooked on autocompletion, real-time code error highlighting, and advanced refactoring support — IntelliJ is my king — I find that it’s hard to imagine doing without.

But that’s not to say that type systems aren’t sometimes a real pain. Particularly ornery is all the machinery around making changes to the type system. Not all of us can be Scott Blum (GWT compiler ninja), and compiler hacking is not a well-known art. But without access to compiler internals, type-system hacking is very hard to come by.

Gilad Bracha, while he was at Sun, had some interesting things to say about pluggable type systems. Now, that paper is somewhat of a gripe fest, in that while it may be clear what he’s complaining about, it’s not entirely clear what to do about it. What does a pluggable type system actually look like?

I occasionally scour the recent proceedings of the ACM for interesting papers. (Any language lawyer who’s not a member of the ACM’s Digital Library is seriously missing out. Also, I’ve got to catch up on Lambda the Ultimate.) Recently in OOPSLA 2006, Andreae, Noble, Markstrum, and Millstein gave some real body to the theory with their paper on JavaCOP, a framework for building pluggable type systems in Java.

One of their examples is a @NotNull annotation to mark variables that can’t have null assigned. Check out their syntax for verifying that no bad assignments happen:

rule checkNonNull (node <<: sym) { 
 where(requiresNonNull(sym)) { 
   require(definitelyNonNull(node)):  
    error(node, "Possibly null expression "+    node+" considered @NonNull");
}}
Working through this, this defines a constraint on all symbols that have the requiresNonNull property (which they implement with the @NotNull annotation on the symbol).  All such symbols further require that the AST node assigned to them definitely has a non-null value.  Their system implements all this as a layered extension to javac, that is able to check eight or so extended type properties in no more than double (at worst) the compile time.
Very interesting stuff, which points (to me, anyway) in the direction of generalizing the research to re-express Java’s whole type system in rules like this.  In other words, they’re starting from Java and layering more type rules on top, but they could also work downwards and re-engineer Java’s existing rules in their framework.
What would be the ultimate goal here?  Well, giving more flexibility to juggle the nominal versus structural issues that Gilad talks about would be one reason.  Another reason would be found in a more recent Gilad paper (apparently presented at Google last fall), about implementing offline objects that provide local support for centralized software services.
Now, if you read this paper after the recent shipment of Google Gears, it has all kinds of interesting ramifications.  Gilad proposes a generic synchronization system implemented by reflective logging of local object modifications, supporting reconciliation on the server by change log replay.  (This is actually very similar to the Dojo Offline model of synchronization, as presented at GDD07 last week.   I wish there were a text post describing the model, because all these video posts and podcasts give me a pain. )  I’m not entirely convinced that model is as generic as he would like, and I will need to bang my head against data-based synchronization some more before I go to operation-based synchronization, but it’s nonetheless thought-provoking.
Pluggable type systems come in when he discusses upgrading local code in a modular way.  It looks to him like a fully static type system such as Java’s has inadequate flexibility for changing shared type definitions at runtime.  This is getting into the arena of major magic — I’m personally very queasy about the whole concept of upgrading code modules that are in mid-execution.  I’d prefer to treat that problem via an Erlang-like model of strict isolation through message passing — the model that the E programming language implements.  (And by the way, if you haven’t bought into capability security yet, read one of Mark Miller’s recent papers already and get with the program!)
At GDD07, I ran into Doug Crockford, who mentioned that he and Mark had discussed taking Google Gears’ support for isolated worker threads and using it to implement securely encapsulated downloadable code.  That squarely jibes with Gilad’s recommendations, and is something that could be prototyped Real Soon Now.  Of course, Gilad’s whole pluggable-type machinery is definitely not on that agenda, but we must walk before we can run.
So where does this leave us?  Seems to me there are several directions to pursue:

Gears provides a reasonably deployable framework for experimenting, not only with offline applications in general, but with an encapsulated framework for mobile code, and with the overall synchronization / update model Gilad discusses.
Pluggable type systems in general, along the lines of the JavaCOP system, provide a rich variety of new data points on the traditionally impoverished “static versus dynamic” axis in programming language design.
The right kind of type system to implement extensible, upgradeable local software objects — particularly local objects with the ability to have their message formats, persistence structure, and inter-module interfaces — is a huge open question, and pluggable type systems give us a much more fine-grained and flexible toolset for experimentation.

I find myself wondering what a JavaCOP framework built into the GWT compiler would look like….
(Does anyone have any links to work on JIT compilation for Javascript?  If Javascript is moving in the direction of being a generic intermediate language, it’d be good to know how fast it can be made.)

Advertisement
Share this:
Twitter
Facebook
Like this:
Like Loading...


	
Related