UK Elections

Bit of a departure from the usual, but it's election time, so why not?

Who to vote for - no-one looks conviincing, labour are tired and have made a total mess, plus there is that unpleasent Tony Blair taste left over. The size of the british state is getting ridiculous and the infringements on civil liberties frightening.

Voting Tory would be like selling one's soul to Satan (remember the '80s?), plus Cameron looks like Blair 2.0. The liberal democrats have some good policies (civil liberties, imigration) and actually have a chance of getting some votes this year, but have some stupid policies too (abolishing tuition fees, no nuclear power, etc.). Perhaps a lib-dem/tory coalition might work. What we really need is a proper liberal party - in both economic and social terms. And one with the guts to radically reform the health service (take power away from the GMC, reform doctor training and the doctor's/GMC monopoly) and education (let universities charge what they like, abandon the stupid target of getting stupid people through universities, fix primary/secondary schools a bit (although God knows how to do that)).

So The Economist is probably right, as repulsive as it seems, the tories are probably the best bet for a vote. Now that is a sorry state of affairs, glad I don't actually live in the UK right now.

You wait months for a good seminar...

...and then three come along at once!

Following Monday's seminar Robert was scheduled to talk again on tuesday, this time at the NZCSRSC (student research conference). It sounded like an interesting talk - "How to change the world" is not a modest title. And having perused the slides I am very disappointed not to have attended - it looks like there were a lot of good things, and thinking about your work in terms of impact is an interesting perspective, and one which I have not thought of since working in PLT.

Anyway, I couldn't attend because I was attending another seminar, this one from Rusten Leino on the Dafny language/verifier and other verifcation stuff going on at Microsoft research. It was a very interesting seminar with a very good demo of verification in action. Pretty impressive amount of bugs caught and all proofs done automatically - it was kind of like magic! Really solved the problem I have with a lot of these things, which is that no-one wants to prove their programs. The annotation overhead is still quite high, and I think only a minority of programmers will be able to write the specifications. But, with a little practice, I can imagine writing code with specs in Dafny in a practical way.

Rusten also summarised some of the other verification efforts he is associated with and they have acheived some pretty cool stuff.

"Dynamic framing" sounds cool, and I should try and understand it better.

Overall, I got the feeling that right there was the future of 'safe' programming languages, or at least a sneak peak of it. And, since it's at Microsoft, it actually has a fighting chance of making it into the real world!

Who would have thought...

...that a talk about standards would be interesting? But it was! Robert O'Callahan (Mozilla) just gave a talk about web standards. Standards are dull, and people who care about them tend to be even duller, but this was not a dull talk! It was interesting! Lots of interesting things about the web.

One nice thing is that short interations seem to work better for standards too, just like software. I think this is one of those fundamental computer science truths, kind of like "you can solve any problem with an extra indirection", for any task, shorter iterations are better.

Also, interesting parsing problem - "herebedragons", its obvious what is intended, but how should you parse it? And make a tree that can be manipulated by Javascript etc. And we all thought syntax had been solved thirty years ago. In fact, the web seems to be a whole new world of interesting computer science problems (see the post on Javascript VMs). Now what would be an interesting research topic?

VM talks and assembly language

Google are currently developing two (at least only two are public) VMs: Dalvik and V8. Dalvik is a Java VM (but not a "JVM" - it doesn't run Java byte code) targeted at mobile devices (part of Android), V8 is a Javascript interpreter and part of the Chrome browser. There are talks on both:

Dalvik: http://www.youtube.com/watch?v=ptjedOZEXPM

V8: http://www.youtube.com/watch?v=lZnaaUoHPhs

I recommend you watch both, they are both good, the V8 one in particular really got my juices going (man, I'm such a geek).

I think it is interesting to compare the two as the tackle a similar problem in very different ways. Obviously the source languages are different, in particular, V8 does lots of interesting stuff to optimise Javascript out of the dynamic language tar pit. The goals are different: Dalvik's main goal is to minimise space (also, time, but mainly space) and battery life; V8 is a pure speed machine. Dalvik doesn't do any JITing, V8 is (as I understand it) all JITed. Dalvik is optimised by using a new set of byte codes and a more compressed file format and some neat tricks on internal libraries etc. V8 is optimised by using classes and caching call sites. There's tons more on both VMs in the talks, and lots more stuff for an interesting comparison.

All of this machine hackery inspired me to look again at x86 assembly and architecture (and maybe I'll look at ARM next). I used to think x86 assembly was a big scary mess and best shyed away from. I've always output JVM or MIPS assembly in compilers etc. for this reason. Bu actually, x86 is not too bad! There's a few more instructions that do some pretty interesting things, but it really isn't much worse than other assembly languages. And I find it really interesting finding out how the processor works; maybe there's a closet bit-jockey in me after all.

A rant - empirical analysis

Having typed up my ECOOP notes and gone through the proceedings a bit, I have actually got a little bit angry about the state of affairs concerning empirical analysis.

A few years ago it seemed that any kind of empirical analysis was a bonus and as long as you had a problem and a solution and a soundness proof you were good to go. The obvious problem is that there is nothing to say that your solution addresses the problem, that the problem is serious, or that the solution is practical.

Bit by bit reviewers have started asking for some empirical evidence to answer these questions. Can someone tell me why this fashion started?

I don't have too much of a problem with this, except that we are doing research here, and some of these crazy ideas which aren't practical and don't really solve any problem lead to solutions that are and do. If you press too hard for practicality you lose the paradigm shifting ideas that only seem practical in ten years time.

What has made me angry, is that the pendulum seems to have swung too far: it now seems really hard to get something published without empirical analysis, which makes it hard to be productive unless you have an army of students and constrains some good, but not immediately practical, ideas. Furthermore, there seem to be a few papers published at ECOOP which seem to be half a paper - just the evaluation or motivation section of a decent paper, without any real idea. These seem to have been published on the strength of the empirical analysis alone, without having asked how much of a contribution this analysis actually is.

I agree there is a need for analysing existing work, but some just seems unnecessary and, frankly, boring.

I count four papers at ECOOP that I would reject for being pointless (there is at least one paper (probably more, but I can't be bothered to look through the proceedings again) that is pure analysis and I think is useful). No names, obviously.

I'd be very interested to here othe peoples views on this, cheers!

ECOOP day 3

Tobias gave the first technical talk and was surprisingly bright-eyed; apparently that's what being Swedish does for you. The paper is entitled Loci: Simple Thread-Locality for Java. There is a very simple ownership system (two annotations - shared and thread) where threads own their thread local data and the system restricts references accordingly, thus data is kept thread-local. It's all enforced statically, and they have a compiler. Their empirical evaluation found that most classes could be made thread-local.

Next was Failboxes: Provably Safe Exception Handling presented by Bart Jacobs the younger. These are essentially a safer version of exceptions (although they are layered on top of exceptions, they're not a replacement). The problem with standard exceptions is that side effects made inside a try block will remain even if the try block fails and an exception is thrown. Fail boxes allow non-lexical scoping of expressions and so failure can prevent execution of dependent expressions which are outside the try block.

Weirdest talk of the conference award goes to Yossi Gil presenting "Are we ready for a Safer Construction Environment". The idea is small but sweet and is a restriction on the way objects can be constructed. The problem is that during object construction, objects are 'half-baked' that is, construction has not finished, fields may not have been initialised, and invariants may not have been established. They propose restricting construction to their hard-hat model, which means that means no virtual method calls and no exposure of this to external methods.

Now, whilst this is a solution, it's not very clever, it seems to be along the lines of "if you do nothing, you won't get hurt" and to me seems like it should be a paragraph in a 'how to program' textbook, not a full paper in a PL conference. But, they have done loads of corpus analysis to confirm the obvious, and since that seems to be in fashion now (why? Can someone please tell me why?!), it has got published. Having said that it is something that I would bear in mind if I were making a system where invariants at construction was important, so I guess it should be published somehow...

Christian Haack then talked about Type-Based Object Immutability with Flexible Initialisation. This seems like a lightweight ownership system for immutability. I think the key of it is that you enforce owners-as-dominators (or something like it) during initialisation to ensure an object is initialised 'privately' and then enforce a kind of owners-as-modifiers (it's not total immutability) afterwards. Which is nice as far as it goes. But I feel there is a sweet spot with the immutability/uniqueness/ownership combination which has not quite been hit, although this and other papers are getting close.

Finally, Ali Ibrahim (I think) talked about Remote Batch Invocation for Compositional Object Services. This is an optimisation of RMI so that remote calls are batched together for the sake of efficiency. They introduce a batch keyword to the language, and within the batch scope, the order of execution can be changed so that remote calls are batched. It's all bit cleverer than that, for example, they do 're-forestation' of data structures to improve batching of loops. They have an implementation and plenty of empirical analysis.

ECOOP day 2

Today's invited talk was by Dave Ungar and it felt more like a self-help tutorial than an academic talk. In fact all three of the talks I attended had a whiff of esteem boosting and soul searching about them: are we academics really that insecure in our endeavours or about out role in computer science?

Anyway, Dave still seemed pretty bitter about the lack of success of Self and the way it was handled at Sun, which might well be justified, but didn't fit into the therapeutic tone of the rest of the talk. The points I took from the talk were: interpreters are better than compilers (and this needs technologies such as JIT to realise), design languages on principles rather than examples, and simplicity is better than expressiveness.

The first technical talk of the day was Adding State and Visibility Control to Traits Using Lexical Nesting. The authors seem to back off the founding principles of traits by adding stateful traits (which are now exactly like classes or maybe mixins?) and nesting of objects to give visibility control. Composition is achieved by delegation and delegate methods are automatically generated. Of course, with state you then get back all the old multiple inheritance problems, which are addressed to some extent. So although nice ideas and well-thought out it seems to go completely against Dave Ungar's maxims of simplicity before expressivity and principles before examples.

I liked Modular Visitor Components:..., although I'm not sure if it's even close to practical. This is a possible solution to an extension of the expression problem - the expression families problem. I wasn't quite clear what this was or to what extent previous solutions address it, in particular where virtual classes fall down. The solution was implemented in Scala using a collection of quite terrifying PL technologies - higher order type parameters, variance, traits, and self types. The result is a suitably complex type system that is nicely expressive.

The other joint-best paper of the conference was Debugging Method Names. They find bugs in names such as getString not returning a value or not returning something of type String or setting something etc. They do all this automatically by analysing a whole bunch of programs, which is certainly clever but didn't really seem like a programming languages problem, or even that hard from the talk, maybe the paper better identifies the problems.

ECOOP Day 3 - Day 1 of the main conference

The first invited talk (slides available here, which you should check out for the graphs, if nothing else) of the conference was from Simon Peyton Jones and was about type classes in Haskell, and, more generally, the relation between Haskell and OO langs. The talk was really good, SPJ has so much energy and gives a really, really good presentation. The big point that I took away was that Haskell has universal polymorphism (parametric polymorphism) and OO langs (i.e., Java) typically have subtyping (inclusion polymorphism). I would generalise so far as to say that the primary form of polymorphism in functional languages is universal quantification, and the primary form of polymorphism in OO languages is existential quantification, but then you all know I have a soft spot for the old backwards 'E'.

The talk started with a quick overview of Haskell and then motivated type classes as a solution to the problem of how to do universally quantified functions, but restricted to certain types (eg don't want to have an equals function that can take functions as arguments). I won't pretend to fully understand type classes, but they seem cool. What is really cool, is SPJ's claim that Wadler and Blott just plucked the idea out of thin air!

The next part of the talk compared Haskell type classes to OO dispatch. Both are essentially forms of dynamic dispatch, but type classes can be compiled away, which virtual methods cannot be. Furthermore, type classes dispatch based only on a value's type, whereas virtual methods dispatch on the value itself (by which I assume he means runtime types). Type class dispatch is different to Java overloading too, because overloading is a static mechanism (it can be compiled down to no choice at all at runtime), but type classes dispatch at runtime (even though the mechanism is compiled out statically - actually now I write this I'm not 100% sure how this is difference from OO dispatch, other than OO has subtyping...).

SPJ also talked about things he envies in OO-land. First up was the power of the dot, which seemed to come down to IDE support and overloading - the latter of which no-one in OO-land seems to like anymore! Next were heterogeneous lists, which I think is just another request for existential types, just like subtyping is. He then discussed future work a bit - the most interesting sounding bit of which is type functions.

The first technical paper was Coinductive Type Systems for Object-Oriented Languages, which was joint-best paper of the conference, but went completely over my head. I will return to it later though.

Next, Checking framework Interactions with Relationships presented by Ciera Jaspan. Their FUSION system allows developers to specify relationship constraints, effectively multi-object invariants, which are implicitly time-sensitive (by which I mean that there is no explicit notion of time in their system, but that order matters, these are not static invariants which must be maintained: the developer can specify "x then y" or "x must follow y"). Checking can be sound or complete, but not both, or a pragmatic variant which is neither, but hopefully the most useful in practise.

After lunch, Nick Mitchell talked about Making Sense of Large Heaps, which, I predict, will be a paper that gets a lot of references. He presented a tool, Yeti, which analyses heaps by breaking them into 'data structures' and 'sections'. The essential concepts used in the analysis are those of ownership and domination, and it is interesting to see ownership used to analyse, rather than prescribe.

The last session of the day was great, starting with Implicit Dynamic Frames:... by Jan Smans et al. It is a nice approach to verification by specifying access permissions in pre- and post-conditions. Pure methods and 'predicates' - pure methods which abstract assertions rather than expressions - allow the language to support abstraction.

The next talk - Fine-Grained Access Control with Object-Sensitive Roles, presented by Dan Marino - was great, using Britney Spears' medical notes as motivation. I am very surprised that nothing like this has been done before, it seems so sensible. The idea is that rather than just using roles to do security, you parametrise the roles by the ids of objects so that you get per-object, rather than per-role, security. Good idea, good execution. Also, nice use of effects and existential quantification.

Last talk of the day was Practical API Protocol Checking with Access Permissions presented by Nels Beckman. This uses typestates and access permissions to specify protocols which can be checked by static analysis. This paper is an evaluation of that work, and lo and behold, it works! There are some interesting points raised along the way, such as hasNext methods in JDBC not being pure (which I've come across a while ago, but can't remember where).

ECOOP day 2: IWACO

Viktor Kuncak gave the invited talk, the theme of which is his effort to get "verified abstractions on developers' desks". This boiled down to verifying library code, the hard part of which is accounting for the different state in the library vs. the application. He talked about his tool Jahob, which apparently does the business.

I chaired the first technical session of the day at IWACO, and it was the first session I've chaired at a workshop/conference, so I was a bit nervous. But all the talks were good and it went OK.

The first talk was by Nels Beckman and was about using access permissions to reduce STM overhead. This was a great little talk and had a great presentation of the various kinds of access and how they relate. The relation to STM was straightforward, but looked useful and they had empirical evidence to back it up - although 9% seems not too much of an improvement. It was also interesting that their optimisations incurred more overhead in some cases.

Eric Kerfoot presented the next talk, which used a very simple ownership scheme to avoid deadlock. Although the ownership aspects of this work were not that interesting (and probably not flexible enough for real life), it is good to see an application of ownership. The only problem being that the work seemed to be able to introduce more deadlocks if the wait clauses never become true.

William Retert presented the last talk of the session (and my favourite paper from the workshop) which compared everything even vaguely IWACO related using fractional permissions. This is a nice thing to do and something I'm very interested in seeing. I like being able to see exactly how these different mechanisms relate to each other. Unfortunately, other than encoding them all with fractional permissions, there wasn't much effort to then explain how these permissions relate at an intuitive level. I would have liked to see how their owners-as-effectors property relates to owners-as-modifiers, it is not quite a generalisation. I think it would also be interesting to extend the permissions beyond reading/writing to referencing so that owners-as-dominators could be expressed.

After lunch, Sophia presented work on flexible object invariants. The big point is that object invariants should be first class, and not just treated as syntactic sugar for pre- and post-conditions. An interesting example of invariants that can't be enforced in a tree-like structure are PIPs - Priority Inheritance Protocols, which involve cyclic structures.

I gave my first talk on wildcards in OGJ which went pretty well, and people seemed to 'get', although there was a bit of an atmosphere of "this is interesting, but so what?".

After the coffee break Paley spoke about combining ownership with relationships, in particular tackling the question of how relationships may be mutated with respect to their ownership properties. Finally I gave my second talk on comparing Universes and Ownership Types. Unfortunately, by this time I was mentally and physically exhausted and I was barely coherent for most of the talk and didn't handle the questions too well, which is a shame because the questions were really on point and I could have given more enlightening answers.

ECOOP day 1 - FTfJP and SToP

And so to the conference; first day - the FTfJP and SToP workshops. The former good, the latter great, it really seemed a workshop in the right place at the right time.

I spent the morning at FTfJP, including presenting my paper on wildcards and subtyping, which was surprisingly well received. It seemed to get people thinking and I got good questions. I was very worried that it would be a hard sell and people wouldn't see the point, but thankfully I was proved wrong.

The invited talk was by Todd Millstein and was on his generic effects system. Unfortunately I was rather tired and couldn't pay much attention, but it was a good talk on an interesting topic. I highly recommend the paper which (I think) was at TLDI this year. The most interesting thing I took away from the talk was the relationship between effects and permissions, which is something I've been thinking about myself rather a lot recently.

The first technical talk was A Typed Intermediate Language for Supporting Interfaces by Juan Chen. What I found interesting was the use of existential types for class types which I've also made use of. It is interesting here because she is using them for, essentially, implementation reasons in the intermediate language; specifically to give types to iTables for dispatching method calls on interface types.

Next up was Range Parameterized Types: Use-site Variance without the Existential Questions by Bruno De Fraine which proposes a simpler version of Java wildcards. The system is less complex, but this should not be surprising as it is less complex. In particular there seems no difference from existential types which cannot be unpacked over a scope (i.e., wildcards capture). Although the formalism is direct, it is significantly more complicated (and less elegant) than an existential types system.

Reuben Rowe then presented Semantic Predicate Types for Class-based Object Oriented Programming. This proposed adapting and generalising intersection types to the OO world as predicates and presented an approximation theorem which, I'm afraid, went slightly over my head. I will be reading the paper though...

After lunch I switched workshop and Attended SToP which was a proper workshop (as opposed to a mini-conference) and had a lot of discussion; it was, therefore, running an hour behind schedule. Which meant that I could catch the second half of Phil Wadler's talk. This reminded me how good a speaker he was and also how cool the blame thing is. On the downside, the talk was very similar to the one I saw at ESOP a few months ago. It included the same division of subtyping into four variations and higher order casts, but added polymorphism. This turns out to be surprisingly difficult - it interacts badly with some of the subtyping.

Next was a talk on Diamondback Ruby which I remember being interesting, but my notes of the talk are terrible.

The next talk (I'm on the plane now and so can't look up the titles/authors, sorry) was about typing in scheme and had the interesting conclusion that type checking extended with gradual typing improved expressivity, even when no dynamic typing was used!

Next up: Atsushi Igarashi's student with progress towards gradual typing in FGJ. Mathias didn't seem to think that this was gradual typing at all. They used a type dynamic, denoted with a question mark, but which didn't correspond (with generics) to wildcards. This seemed unnecessarily confusing.

The final talk (presented by Gregor and his crazy hat) analysed Javascript programs in order to find out how many (and which) dynamic features were used. The conclusion seemed to be quite a lot in real life, but in quite fixed patterns. Also that Sunspider is not a realistic set of benchmarks.