Well my notes get sparser by the day and I attribute this to conference fatigue rather than fewer good talks, so here is my rather brief account of day two at ECOOP.
The first paper I would like to describe was on UpgradeJ and the talk was given by Gavin Biermann. To be honest I thought this problem had been solved because I have not seen any work addressing it recently, but it seems I am wrong, and just as well because this was one of my favourite talks. The problem is to dynamically update running Java programs, which entails all sorts of headaches: Gavin started off the talk by warning that this was a topic for experts, not novice programmers. Although, after everything was explained it didn't actually seem _that_ hard, perhaps in real life it is more difficult (which begs the question - "how much can this stuff be encapsulated?"). Anyway, they propose a scheme of class upgrading with explicit (and multiply co-existing) versions; furthermore, upgrading is explicit too. I kind of like this approach - no surprises! There are lots of nice little features, such as fixing classes at a certain version or allowing them to upgrade, or allowing possibly breaking upgrades etc. Also, it is rather conservative, in a good way, you can not rely on versions being loaded at some point to call the upgraded code. I wonder if it is possible to rollback versions too. I suspect so, seeing as the system, is conservative type-wise, but I guess I'll have to read the paper to find out...
Next was Donna Vali... (sorry Donna! My internet has gone down, and I will be too lazy to check this later) talking about her system for mixing nominal and structural subtyping. I've looked at this work a few times before (see blog posts below vvv). I like it, it has a nice mixture of the features of both type systems and it seems well thought through. My only quibble is that it is hard enough to convince programmers to use types and I wonder if they will get enough benefit to deal with the extra overhead. Actually, I suspect they would, if they tried, but I also suspect that they are mostly to lazy to try and that language designers are too risk averse to try too. Also, the real joy of structural typing comes from the flexibility, and this has to be lost in order to accommodate nominal subtyping, so I am very interested to see how flexible the system is. I will read the paper and find out! And something to think about - Donna gives objects a structural and a nominal type, the structural type has a clear run-time counterpart - the record, and an object can be thought of as a record and a brand (the nominal part of its type). BUT, what is a brand? Is there a runtime entity that can exist without an object and captures the essential features of this mysterious brand? I am very interested to know, so if anyone has any ideas, please let me know!
The day was wrapped up with Gilad Bracha's summer school talk on his new language Newspeak, which was very popular (I would be a little gutted if my talk was scheduled for this time) and brought on a lot of George Orwell puns. Anyway, it was a great talk, Gilad is a wonderful speaker,and the language is interesting and abides by a lot of very sensible rules. One thing I lied was the design philosophy - you think of a rule, and everything else just kind of follows from it, no exceptions.
After all this intellectual tomfoolery we had the conference banquet in the evening. This was in a touristy taverna in Paphos town where the music was too loud and the entertainment was very cheesy, and apparently provided by perverts. If I ever have daughters they will never set foot in Paphos as long as I live. James Noble started a very entertaining speech, including heckling some tourists at one point, but was quite rudely cut off by the band halfway through, which is a shame since it looked like it was going to be the only entertaining conference speech in history. This was followed by more 'entertainment', not least of which was my supervisor, Sophia, dancing with performers and generally enjoying herself (there is video, although I have not received it yet...). We made a sharp exit, and had an enjoyable night chatting with various ECOOP people in various ECOOP places.
I'm a research engineer at Mozilla working on the Rust compiler. I have history with Firefox layout and graphics, and programming language theory and type systems (mostly of the OO, Featherweight flavour, thus the title of the blog). http://www.ncameron.org @nick_r_cameron
Wednesday, July 30, 2008
Tuesday, July 29, 2008
ECOOP day 1
And so to the main conference. First of all I would like to brag that our paper was nominated for best paper, which is very flattering, unfortunately we didn't win, but at least we have something to aim for next year :-)
The day started (well, after the usual welcome chit chat) with an invited talk about transactions, that dialled the usual numbers about multicores and concurrency being the next big thing, and transactions being _the_ way to address the whole concurrency problem, and asked the question "are these transactions the same as we were talking about 30 years ago?"
Following this was my talk, which went swimmingly, although I was still a little rushed at the end, although I still managed to finish (almost) on time and earn myself a pear.
Unfortunately I was to drained emotionally to pay any attention to the nest talk, which is a shame because it looked really interesting and I will definitely be reading the paper - it was about mixing inheritance between languages.
Later, I attended the summer school talk on JavaCOP which was very interesting and really sold the concept. They basically implement pluggable types, a concept of which I am a very big fan, and allow you to add your own type systems to Java. I think it is defiantly worth looking at a bit closer and I will do this as soon as I have some time (which really means after my thesis is finished). In a nutshell: you write extra types as annotations to your Java code, and define a bunch of predicates that makes them all work and JavaCOP compiles it all into a class file which can then check the programs you annotated. It all seems like an interesting and practical idea with probably a never ending list of extra things that could be added.
I rounded off the day with another summer school talk, this time by Jonathan Aldritch on SASyLF - a proof assistant for students. This was a great session and we all had a go at making and running SASyLF proofs. It got me even more convinced that I must learn how to use one of these proof assistant things. There seemed two novelties with SASyLF: first that it is really aimed at the ECOOP (rather than POPL) crowd, and so has natively a lot of things that you waste a lot of time doing in other proof assistants; secondly, it is aimed at students, which means you have to spell everything out and can't tell it do as much as it can with guidance at any point. Most people seemed to regard this as a shame as they'd like to be able to use it since it is adapted to their needs. There was much talk of some kind of professor switch to make things quicker whilst still making students understand everything, but this seemed impractical from a security point of view. Anyway, it was all very cool!
The day started (well, after the usual welcome chit chat) with an invited talk about transactions, that dialled the usual numbers about multicores and concurrency being the next big thing, and transactions being _the_ way to address the whole concurrency problem, and asked the question "are these transactions the same as we were talking about 30 years ago?"
Following this was my talk, which went swimmingly, although I was still a little rushed at the end, although I still managed to finish (almost) on time and earn myself a pear.
Unfortunately I was to drained emotionally to pay any attention to the nest talk, which is a shame because it looked really interesting and I will definitely be reading the paper - it was about mixing inheritance between languages.
Later, I attended the summer school talk on JavaCOP which was very interesting and really sold the concept. They basically implement pluggable types, a concept of which I am a very big fan, and allow you to add your own type systems to Java. I think it is defiantly worth looking at a bit closer and I will do this as soon as I have some time (which really means after my thesis is finished). In a nutshell: you write extra types as annotations to your Java code, and define a bunch of predicates that makes them all work and JavaCOP compiles it all into a class file which can then check the programs you annotated. It all seems like an interesting and practical idea with probably a never ending list of extra things that could be added.
I rounded off the day with another summer school talk, this time by Jonathan Aldritch on SASyLF - a proof assistant for students. This was a great session and we all had a go at making and running SASyLF proofs. It got me even more convinced that I must learn how to use one of these proof assistant things. There seemed two novelties with SASyLF: first that it is really aimed at the ECOOP (rather than POPL) crowd, and so has natively a lot of things that you waste a lot of time doing in other proof assistants; secondly, it is aimed at students, which means you have to spell everything out and can't tell it do as much as it can with guidance at any point. Most people seemed to regard this as a shame as they'd like to be able to use it since it is adapted to their needs. There was much talk of some kind of professor switch to make things quicker whilst still making students understand everything, but this seemed impractical from a security point of view. Anyway, it was all very cool!
FTfJP and the DLS
So on to day 2 of the conference, where I mainly attended FTfJP and briefly popped into the Dynamic Languages Symposium.
First of all I'd like to bing attention to my colleague, Alex Summers' talk, which was a good talk, but more importantly the work is interesting. Actually I have been a little bit involved with it (only a little though) so I have heard a lot of teh stuff he talked about. But, I think it is very interesting, it is about adding static fields and methods to the universe type system. Frankly, I think this is a terrible idea, we should just avoid static anything like the plague (see Gilad's summer school talk and (I think) an earlier blog post), but if you're going to do it, then it turns out to be an interesting problem with no easy solution (the best kind, or worst, depending on your point of view).
The next great talk was by Stefen Wehr who talked about wildcards (a topic very close to my heart). He is concerned with decidability, admitedly not directly. In his work he shows that _a_ model for wildcards and another for interfaces in JavaGI, both of which use a similar kind of existential type, are undecidable. This is obviously interesting since decidability of wildcards is still an open question, which I'd love to look at if I had the time and skills, but I have neither, so I have to make do with reading interesting papers like this one.
The next talk of note was at the DLS, it was an invited talk given by Laurence Tratt entitled Language Design: Back to the Future?. The gist of the talk was that all current languages are almost identical and language designers are not really being creative. He also claimed there are some valuable things that people have done and that have been ignored. I kind of agree, although I don't agree that it is due to a lack of creativity on the part of language designers - there are plenty of fairly wild ideas floating around, but it is true that most never make it into real life languauges. He seemed to concentrate on 'micro' level language features such as new expressions, which is an area (I thinK) that has been neglected in research lately in favour of more 'macro' ideas - such as ownership types, different object meta-models etc. I was a little inspired by the speaker to think a bit more about language culture. His point is that programmers, lanaguage designers, and researchers are all absorbed in a certain culture of a language - the paradigm, the programming idioms, way of thinking, etc. It would be interesting to see some research on this - to charecterise and compare these programming cultures and the effects they have on programming languages, and importantly, vice versa. A quote I liked was that innovative language features were destined to have "some spotty twat at the front take the piss out of it".
I'm afraid that by this point I was a little drained and failed to make any meaningful notes, but I'd like to draw attention to the last two talks of the day that I thought were interesting - Rok Strnisa on the Java Module System and Samir Genaim and Fausto Spoto on constancy analysis
And an interesting thought from one of the talks - if we have an underlying database implementation (for example) that only has a next method as an accessor that returns null at the end of the table. If we wish to implement a wrapper with a hasNext method, then this method will have an internal side effect (it must cache the returned row, if it is not null), but logically it should be pure. Can this be handled elegantly in the various ownership/invariants/effects systems that are around?
First of all I'd like to bing attention to my colleague, Alex Summers' talk, which was a good talk, but more importantly the work is interesting. Actually I have been a little bit involved with it (only a little though) so I have heard a lot of teh stuff he talked about. But, I think it is very interesting, it is about adding static fields and methods to the universe type system. Frankly, I think this is a terrible idea, we should just avoid static anything like the plague (see Gilad's summer school talk and (I think) an earlier blog post), but if you're going to do it, then it turns out to be an interesting problem with no easy solution (the best kind, or worst, depending on your point of view).
The next great talk was by Stefen Wehr who talked about wildcards (a topic very close to my heart). He is concerned with decidability, admitedly not directly. In his work he shows that _a_ model for wildcards and another for interfaces in JavaGI, both of which use a similar kind of existential type, are undecidable. This is obviously interesting since decidability of wildcards is still an open question, which I'd love to look at if I had the time and skills, but I have neither, so I have to make do with reading interesting papers like this one.
The next talk of note was at the DLS, it was an invited talk given by Laurence Tratt entitled Language Design: Back to the Future?. The gist of the talk was that all current languages are almost identical and language designers are not really being creative. He also claimed there are some valuable things that people have done and that have been ignored. I kind of agree, although I don't agree that it is due to a lack of creativity on the part of language designers - there are plenty of fairly wild ideas floating around, but it is true that most never make it into real life languauges. He seemed to concentrate on 'micro' level language features such as new expressions, which is an area (I thinK) that has been neglected in research lately in favour of more 'macro' ideas - such as ownership types, different object meta-models etc. I was a little inspired by the speaker to think a bit more about language culture. His point is that programmers, lanaguage designers, and researchers are all absorbed in a certain culture of a language - the paradigm, the programming idioms, way of thinking, etc. It would be interesting to see some research on this - to charecterise and compare these programming cultures and the effects they have on programming languages, and importantly, vice versa. A quote I liked was that innovative language features were destined to have "some spotty twat at the front take the piss out of it".
I'm afraid that by this point I was a little drained and failed to make any meaningful notes, but I'd like to draw attention to the last two talks of the day that I thought were interesting - Rok Strnisa on the Java Module System and Samir Genaim and Fausto Spoto on constancy analysis
And an interesting thought from one of the talks - if we have an underlying database implementation (for example) that only has a next method as an accessor that returns null at the end of the table. If we wish to implement a wrapper with a hasNext method, then this method will have an internal side effect (it must cache the returned row, if it is not null), but logically it should be pure. Can this be handled elegantly in the various ownership/invariants/effects systems that are around?
Tuesday, July 22, 2008
ECOOP '08, Cyprus
This is turning into nothing more than a conference blog, and I apologise if anyone actually reads this (actually, at least one or two people do, as I found out - hello!). Its not that I've stopped having ideas, its just that I've been very busy. I'm now in Israel, en route to Egypt to write my thesis (yes, it is a good idea, actually). I have a little time to write a little in the blog, so here is my summary of ECOOP...
ECOOP this year was in Cyprus, not an altogether popular choice, since getting there from anywhere except London was a nightmare, but I came from London so I was happy. Also happy to be very close to the beach and for it to be very warm, thus making for a very enjoyable conference. Well, except for the fact that I was working a little and had a walk to the hotel and it was hot and I inevitably sweat so much I spent most of the conference smelling like a tramp, but hey.
Anyway, the first day was IWACO, which was great. I really like this little workshop and enjoyed nearly all the papers, so you could go worse than go to http://www.cs.purdue.edu/homes/wrigstad/iwaco08/programme.html and read them all! Some comments on some of the talks follow:
First was Jonathan Aldritch's invited talk - the theme of which was making ownership types systems usable by real programmers. It was a great talk and he discussed a lot of aspects that make type systems more or less likely to ever make it into real langauges. He talked about the adoptability and applicability of ownership systems - adoptability concentrated on making these systems easier to use: less annotations, more inference, etc. And how to get the programmer to give the right guidance to the compiler to do inference. Applicability was basically about offering less strict organisation than classical ownership types - such as existential types (!), multiple ownership (!), domains, etc. He also encouraged us to _actually_ study more code to find the strucure of large software.
Alex Potanin then talked about unifying ownership and immutability by using generics, which is a very interesting idea at its early stages.
I gave a talk on existential types for ownership variance, which uses the nice clean framework of existential types to give owner variance without the kind of hackery we use in, for eg, MOJO.
The talk by Nicholas D. Matsakis and Thomas R. Gross was also good. They parameterise types with partitions that restrict effects and use this information to ensure thread safety. It seemed to me like a more fine-grained version of atomic sections, since they restrict the atomic-ness (i.e., the non interfernce of effects) to a parition, while atomic sections apply to the whole heap. I also wonder what would happen if you allowed some kind of variant partitions, like wildcards (not that I'm developing a one-track mind for wildcards or anything).
John Boyland gave a good position paper, which basically said non-linear reasoning (ownership) is better for reasoning about non-linear problems, specifically volatile fields, than linear reasoning (seperation logic).
The talks were rounded off by some interesting demos and a talk about J* by Dino from Queen Mary's, which inspired me to read the seperation logic literature, which I've been meaning to do for a while, but never got round to...
James Noble made the astute comment that some kind of ownership was creeping into seperation logic techniques in order to address certain problems. Also the composite pattern is the new subject-observer - it is difficult to model since you go bottom-up, breaking all the invariants as you go, and then repair them all. I wonder what we will do for motivation when we finish the design patterns book.
ECOOP this year was in Cyprus, not an altogether popular choice, since getting there from anywhere except London was a nightmare, but I came from London so I was happy. Also happy to be very close to the beach and for it to be very warm, thus making for a very enjoyable conference. Well, except for the fact that I was working a little and had a walk to the hotel and it was hot and I inevitably sweat so much I spent most of the conference smelling like a tramp, but hey.
Anyway, the first day was IWACO, which was great. I really like this little workshop and enjoyed nearly all the papers, so you could go worse than go to http://www.cs.purdue.edu/homes/wrigstad/iwaco08/programme.html and read them all! Some comments on some of the talks follow:
First was Jonathan Aldritch's invited talk - the theme of which was making ownership types systems usable by real programmers. It was a great talk and he discussed a lot of aspects that make type systems more or less likely to ever make it into real langauges. He talked about the adoptability and applicability of ownership systems - adoptability concentrated on making these systems easier to use: less annotations, more inference, etc. And how to get the programmer to give the right guidance to the compiler to do inference. Applicability was basically about offering less strict organisation than classical ownership types - such as existential types (!), multiple ownership (!), domains, etc. He also encouraged us to _actually_ study more code to find the strucure of large software.
Alex Potanin then talked about unifying ownership and immutability by using generics, which is a very interesting idea at its early stages.
I gave a talk on existential types for ownership variance, which uses the nice clean framework of existential types to give owner variance without the kind of hackery we use in, for eg, MOJO.
The talk by Nicholas D. Matsakis and Thomas R. Gross was also good. They parameterise types with partitions that restrict effects and use this information to ensure thread safety. It seemed to me like a more fine-grained version of atomic sections, since they restrict the atomic-ness (i.e., the non interfernce of effects) to a parition, while atomic sections apply to the whole heap. I also wonder what would happen if you allowed some kind of variant partitions, like wildcards (not that I'm developing a one-track mind for wildcards or anything).
John Boyland gave a good position paper, which basically said non-linear reasoning (ownership) is better for reasoning about non-linear problems, specifically volatile fields, than linear reasoning (seperation logic).
The talks were rounded off by some interesting demos and a talk about J* by Dino from Queen Mary's, which inspired me to read the seperation logic literature, which I've been meaning to do for a while, but never got round to...
James Noble made the astute comment that some kind of ownership was creeping into seperation logic techniques in order to address certain problems. Also the composite pattern is the new subject-observer - it is difficult to model since you go bottom-up, breaking all the invariants as you go, and then repair them all. I wonder what we will do for motivation when we finish the design patterns book.