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.

Banquet Speech

Last night was the conference banquet and William Cook gave the speech and it was good. I thought I would blog about it now, while it's fresh in my mind, even though this post will be out of order.

The speech involved William doing a strip tease from industry suit to academic shorts and t-shirt; luckily he stopped there (but kudos to SPJ - "we want more!").

The theme of the talk was industry and academia and also a bit of motivation for academics. There were many interesting points raised, including: industry are not as slow/conservative as we think; industry have lots of ideas - problems and solutions; industry need complete, not partial, solutions; and many more.

One point I thought was intersting was about the WWW: William wondered why it was an industrial, not academic invention, and suggested this was a shortcoming of academia: apparently, the fundamentals were done in academia, but putting it all together was not "publishable" and so was never tackled. I think that this is a perfect synergy between academia and industry. Academia tackled the fundamental problems, which it was it does best - small, difficult, abstract, and, presumably, not commericially viable problems., and insustry used the academic research to produce a 'product' - something academia couldn't do easily because it requires a lot of work, and shouldn't do, because it involves work that is alredy well-understood.

The other thing that made me think from William's talk was his idea that one should have a "purpose" in research or anything else. I tend to have short term goals, but realise that I have no longer term purpose in my research. I thimk, this has been something I've been looking for, subconciously, but haven't yet found. And he is right, that nearly all academics who I look up to, have obvious purposes in their work (although often more than one, it seems). So the search is on!

Ecoop '09

Ah, ECOOP is here again. This year, the world's sweatiest conference on object-oriented programming is being held in Genova, Italy. It's a lovely city full of very old and expensive-looking buildings, mostly old palaces - I am amazed that there could be so many palaces in one city! The conference is being held in one such palace and it is an awe-inspiring place for a conference - the conference room would suit the Queen better than a bunch of shabby academics. The food is also much better than normal - even the coffee is drinkable. On the downside, there is no aircon, so it is very hot and sweaty, there are not enough power points, the wifi has issues, and there are three toilets to be shared amongst 200 or so delegates - not good. It is also expensive, but hey.

I arrived on friday and headed to the aquarium, which was amazing. Dolphins, sharks, turtles, penguins, seals, and many, many fish - it was great to hang out with underwater stuff again. Also hummingbirds which were so cool, buzzing around and hovering and twisting around in the air, one of the nicest things I've seen really.

I then met up with Dave Clarke and the Swedes (although Dave is really swedish, it just doesn't say that in his passport), it was great to catch up with everyone, just a shame Nik and Maria weren't sticking around for the conference.

So, in the next few posts I'll go over some of the talks that I enjoyed. But first some general impressions: much less language design stuff - there are barely any formal systems in the proceedings and those are not really proposing new features. SToP (Scripts To Programs) was the most popular workshop, and gradual/hybrid typing seems to be very much in fashion right now. Ownership seems to be losing peoples' interest - which makes me sad, but I guess there has been a lot of work in the area. In fact I would say people are looking beyond static type systems in general a lot more (although there is still lots of interest in verification). Effects seems to be everywhere though, or at least effect-like things, which made me think of effects. A lot of empirical studies of one kind or another are around. Dynamic languages (not just dynamic typing) seem to be popular, and reflection in particular is getting talked about (although I haven't seen any papers). Much fewer industry poeple, although I guess that is to be expected with the economy, and ECOOP hasn't had a strong industry presence for a while. More people have multiple papers.

Corrections

I've edited the post before last ("an opinion on...") because the blogger editor did funny things to angle brackets (turning them into invisible html elements) which made all the types look stupid. Serves me right for only proofreading in the editor, not the blog.

Papers online

I've put the papers I mentioned a few posts back online, they are all at ECOOP workshops. You can find them here.

An Opinion on Ownership Types (generics)

I've been thinking a bit about ownership and generics and I have formed an opinion that I wish to share. I imagine that some people will disagree, but that could be interesting.

Ownership and generics are both desirable in a language: (to paraphrase the OGJ paper) generics let you say I have a list of books (rather than just a list) and ownership types let you say this is my book (rather than just a book). It is also desirable to have both, that is, to say this is a list of my books; and both are needed - there is no overlap in expressivity.

There are basically two ways to combine generics and ownership: orthogonally, where both are present and fulfil their standard tasks without much overlap, and the mixed approach, where type parameters provide the ownership information. (My terminology, and I don't think it is very good terminology at that). Jo\exists, generic universes, and generic confinement fall into the first camp, OGJ, OIGJ, WOGJ, etc. fall into the second.

Example in the orthogonal style:

List<owner,X> {

List<owner,X> next;

X datum;

}

Example in the mixed style:

List<Owner,X> {

List<Owner,X> next;

X datum;

}

So, not much difference in this example, but the subtle difference is an important one: the first example has two kinds of parameter (context parameters and type parameters) and the second example only has type parameters - the type rules are tweaked slightly to enforce ownership.

My opinion is twofold: first that adding generics adds expressive power to an ownership language and second that the orthogonal way, with an adjustment, is the better way to do things, and furthermore, in this case you don't need context parameters at all (other than the owner).

So first off, the 'generics are good' bit: a non-generic list only lets you express the owner of the list and the owner of objects in the list. A generic list lets you express these things and other contexts relevant to objects in the list; for example, List<world,Button<>this,win>, I'm imagining a list of buttons where the buttons have fields owned by the window they're placed in. Without generics the best I could do is List<world,this>, I have to forget about the window the buttons are in (as well as the fact that they are buttons, obviously).

Second, the adjustment, in regular ownership types the owner and other context parameters are usually grouped together. However, if you look at the type rules they are often treated differently, or the owner is treated as a special case. This is made explicit in Joe_3 and some other calculi by putting the owner before the type and separating it from the other context parameters: eg, world:List<this> for a list owned by world containing objects owned by this.

My opinion is that the owner context should be treated differently to the other context parameters and should not be a type parameter. This is because I think that although the behaviour is similar (almost the same as) a context or type parameter it does something extra and different and that it is confusing to confuse the two concepts. This means that type parameters in my ideal system are all just type parameters, there is no special This or World types with special meaning.

Now what is nice is that with generics you no longer need context parameters: you can trivially replace any context parameter with a type parameter and the actual context parameter a, with the actual type parameter a:Object. However, I believe you don't really need to do even this, because any extra context parameters should be in some way tied to a type parameter, so there is a natural way to include the type parameters.

Technical note: when we consider bounds we have to think about context parameters again. For example, in List<X>, what is the upper bound on X? Well in Java it would be Object, but we need an owner, so we could follow OGJ and assume the owner is implicitly present, ie, the upper bound is x:Object where x is an implicitly declared, fresh formal context. Or we could use existential types, ie, the upper bound is \exists x.(x:Object), or in wildcard syntax, ?:Object.

Just looking at the existential types syntax there makes me wonder if it should be (\exists x.x):Object or \exists x.(x:Object), and if there is any difference, and even what the precise meaning of the former is (which are kind of left over questions from the Jo\exists paper that I should think about answering).

Visit to LA

On the way back from ETAPS in the UK I stopped off in LA to visit Todd Millstein and some friends. Visiting UCLA was great fun and very interesting. I delivered a slightly rambling and jet-lagged talk about ownership, existential types, and wildcards and had some interesting discussions with Todd and his PhD students. They are doing some really interesting things on permissions, effects, and more; look out for their upcoming papers.

I also paid a visit to the Museum of Jurassic Technology. This is a museum in the old school sense - meant to entertain as much as educate. It is part living art, part museum, part collection of curios. It is probably the most fun I've had in a museum and many of the exhibits were genuinely beautiful and/or fascinating. If you ever have the misfortune of passing through LA, then I highly recommend a visit, it will improve your time in LA by an order of magnitude

Some light relief

A brief, incomplete, and mostly wrong history of programming languages

The funniest thing written about programming languages since James Noble's ECOOP '08 speech. Thanks to Alex Summers for the link.

PL-Group at VUW

I am in the process of resurrecting PL-Group meetings at VUW. This should be a regular meeting to discuss all kinds of programming language research, both our own and other peoples in the form of papers; kind of like a reading group, but with the aim of fostering more communication and collaboration between people doing PL research at VUW. I have taken over a mailing list to coordinate the whole affair, and hopefully it will feature lots of interesting discussions about PL research. If anyone is interested, I invite you to join the mailing list (even if you're unlikely ever to visit NZ for a meeting) and contribute your thoughts and comments on anything interesting which arises.

To join go to http://ecs.victoria.ac.nz/mailman/listinfo.cgi/pl-group