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.
Wednesday, December 16, 2009
Wednesday, July 22, 2009
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!
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.
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.
Tuesday, July 21, 2009
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.
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.
Monday, July 20, 2009
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).
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).
Wednesday, July 15, 2009
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.
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.
Monday, July 13, 2009
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.
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.
Friday, July 10, 2009
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!
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!
Wednesday, July 08, 2009
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.
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.
Sunday, June 21, 2009
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.
Saturday, June 13, 2009
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.
Monday, June 08, 2009
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).
Sunday, May 31, 2009
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
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
Friday, May 15, 2009
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.
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
To join go to http://ecs.victoria.ac.nz/mailman/listinfo.cgi/pl-group
Tuesday, May 12, 2009
ETAPS report (finally)
I've been putting this off for ages and I've finally lost motivation to write a new report. Instead I will reprint the report I produced as part of my funding requirements. Sorry it's not as good as some of the other conference reports. Lesson learned: write the blog as you go, don't leave it until later.
The YOGI Project: Software Property Checking via Static Analysis and Testing
This project sought to combine static analysis with testing to verify programs written in C. The main application has been to verify drivers; at which it has, apparently, been successful. The system is of course undecidable --- it is possible that their algorithm does not terminate. If the algorithm does terminate, then it either finds an error in the code or produces a proof that the program satisfies its specification.
Well-Typed Programs can't be Blamed
This paper (presented brilliantly by Phil Wadler) is another step towards combining dynamic and static typing. The main contribution is that defiing the `can't be blamed' property: ``in a program with both dynamic and statically typed parts, if a type error occurs, then it must be the fault of the dynamically typed part''. This is essentially a formulation of type soundness for hybrid/gradually typed systems.
I found the four variations of subtyping, and how these relate with co- and contravariance, very interesting.
Exploring the Design Space of Higher-order Casts
Similar to the previous talk , this work addresses the problem of type safety in hybrid/gradually typed systems. The contribution here is the use of higher-order casts, that is, casts over function types (which cannot be statically checked). By labelling each cast (with blame labels) and propagating these labels during execution, the source of runtime errors can be accurately reported.
The system is formalised using a calculus with coercions to model casts; coercions are normalised, and blame labels propagated through normalisation. Several approaches for assigning blame are presented.
I particularly like this work as inaccurate error messages are a very real problem when programming, and this paper presents a solution to some of these problems.
Is Structural Subtyping Useful? An Empirical Study
This work presents an empirical study of Java programs and shows that certain benefits of structural subtyping may be beneficial in a Java-like language. The motivation is that dynamic languages with structural typing are growing in popularity, and so it is sensible to ask if elements of these systems could be useful in more static languages.
The study was undertaken by inferring structural types in the programs and checking when the nominal types were too precise in comparison to the (minimal) structural types. These results were further broken down into cases where there is no possible nominal supertype and where there is; the implication being that in the former case, structural types would be of benefit.
The study found that most types were over-specified (which is unsurprising --- one wouldn't expect all fields and methods of a class to be used in every method), but furthermore that suitable nominal types did not usually exist, that the required structural types were usually small, and that these structural types were not used often --- which implies that they are not worth making into named interfaces.
My criticism of the work is that just because some of the benefits of structural types are beneficial does not mean that structural types are the best solution, and this aspect is not addressed in the paper. That said, the analysis itself is important and, without the link to motivating structural types, ranks as one of the most interesting papers in the conference.
An Interval-based Inference of Variant Parametric Types
This talk presented an interesting and useful way to infer inference annotations. However, the talk was let down by some misunderstandings of variant parametric types and Java wildcards, for example, assuming they have the same semantics, which is wrong. It was also unclear what role annotations on receivers played in the inference algorithm, versus being present in the source language.
The Financial Crisis, a Lack of Contract Specification Tools: What can Finance Learn from Programming Language Design
This was an interesting, mostly non-technical, invited talk which described a mechanism for sepcifying financial contracts using types. The author spoke about some details of their system and his business which runs it. The motivation is that financial trades are not well-understood, in particular, the contracts which specify them are informal and imprecise. The solution is essentially modelling trades like a programming language entity.
Global Principal Typing in Partially Commutative Asynchronous Sessions
The contribution of this work is a session based type system for the Pi Calculus and some interesting meta-theoretic results. Subtyping is sound and complete, and inference is shown to find a principal typing.
Automatic Parallelisation with Separation Logic
This work uses separation logic to perform an independence analysis of expressions. A trace semantics with sophisticated labelling facilitates this. The result is an analysis of a program's footprint which can be used to parallelise expressions.
Deny-Guarantee Reasoning
This work extends rely-guarantee reasoning to handle fork/join concurrency. The crucial concept is interference: some action which affects the state of the program; rely-guarantee creates interferences, but interference must be constant to support forking. Deny-guarantee uses separation logic techniques to split interference, this is used to ensure consistency of interference across forked threads. This technique is similar to fractional permissions. Another crucial concept is the thread predicate, which is a predicate in separation logic which gives a postcondition when and if a thread is joined.
A Basis for Verifying Multi-threaded Programs
Based on fractional permissions, this idea supports complex concurrency primitives (including fork/join, as in the previous talk). Permissions are extended with more complex operations, such as sharing and unsharing. Complex specifications can be written and verified by the system, which also prevents deadlock.
The YOGI Project: Software Property Checking via Static Analysis and Testing
This project sought to combine static analysis with testing to verify programs written in C. The main application has been to verify drivers; at which it has, apparently, been successful. The system is of course undecidable --- it is possible that their algorithm does not terminate. If the algorithm does terminate, then it either finds an error in the code or produces a proof that the program satisfies its specification.
Well-Typed Programs can't be Blamed
This paper (presented brilliantly by Phil Wadler) is another step towards combining dynamic and static typing. The main contribution is that defiing the `can't be blamed' property: ``in a program with both dynamic and statically typed parts, if a type error occurs, then it must be the fault of the dynamically typed part''. This is essentially a formulation of type soundness for hybrid/gradually typed systems.
I found the four variations of subtyping, and how these relate with co- and contravariance, very interesting.
Exploring the Design Space of Higher-order Casts
Similar to the previous talk , this work addresses the problem of type safety in hybrid/gradually typed systems. The contribution here is the use of higher-order casts, that is, casts over function types (which cannot be statically checked). By labelling each cast (with blame labels) and propagating these labels during execution, the source of runtime errors can be accurately reported.
The system is formalised using a calculus with coercions to model casts; coercions are normalised, and blame labels propagated through normalisation. Several approaches for assigning blame are presented.
I particularly like this work as inaccurate error messages are a very real problem when programming, and this paper presents a solution to some of these problems.
Is Structural Subtyping Useful? An Empirical Study
This work presents an empirical study of Java programs and shows that certain benefits of structural subtyping may be beneficial in a Java-like language. The motivation is that dynamic languages with structural typing are growing in popularity, and so it is sensible to ask if elements of these systems could be useful in more static languages.
The study was undertaken by inferring structural types in the programs and checking when the nominal types were too precise in comparison to the (minimal) structural types. These results were further broken down into cases where there is no possible nominal supertype and where there is; the implication being that in the former case, structural types would be of benefit.
The study found that most types were over-specified (which is unsurprising --- one wouldn't expect all fields and methods of a class to be used in every method), but furthermore that suitable nominal types did not usually exist, that the required structural types were usually small, and that these structural types were not used often --- which implies that they are not worth making into named interfaces.
My criticism of the work is that just because some of the benefits of structural types are beneficial does not mean that structural types are the best solution, and this aspect is not addressed in the paper. That said, the analysis itself is important and, without the link to motivating structural types, ranks as one of the most interesting papers in the conference.
An Interval-based Inference of Variant Parametric Types
This talk presented an interesting and useful way to infer inference annotations. However, the talk was let down by some misunderstandings of variant parametric types and Java wildcards, for example, assuming they have the same semantics, which is wrong. It was also unclear what role annotations on receivers played in the inference algorithm, versus being present in the source language.
The Financial Crisis, a Lack of Contract Specification Tools: What can Finance Learn from Programming Language Design
This was an interesting, mostly non-technical, invited talk which described a mechanism for sepcifying financial contracts using types. The author spoke about some details of their system and his business which runs it. The motivation is that financial trades are not well-understood, in particular, the contracts which specify them are informal and imprecise. The solution is essentially modelling trades like a programming language entity.
Global Principal Typing in Partially Commutative Asynchronous Sessions
The contribution of this work is a session based type system for the Pi Calculus and some interesting meta-theoretic results. Subtyping is sound and complete, and inference is shown to find a principal typing.
Automatic Parallelisation with Separation Logic
This work uses separation logic to perform an independence analysis of expressions. A trace semantics with sophisticated labelling facilitates this. The result is an analysis of a program's footprint which can be used to parallelise expressions.
Deny-Guarantee Reasoning
This work extends rely-guarantee reasoning to handle fork/join concurrency. The crucial concept is interference: some action which affects the state of the program; rely-guarantee creates interferences, but interference must be constant to support forking. Deny-guarantee uses separation logic techniques to split interference, this is used to ensure consistency of interference across forked threads. This technique is similar to fractional permissions. Another crucial concept is the thread predicate, which is a predicate in separation logic which gives a postcondition when and if a thread is joined.
A Basis for Verifying Multi-threaded Programs
Based on fractional permissions, this idea supports complex concurrency primitives (including fork/join, as in the previous talk). Permissions are extended with more complex operations, such as sharing and unsharing. Complex specifications can be written and verified by the system, which also prevents deadlock.
Saturday, May 09, 2009
Papers, papers, ...
I have had a few papers accepted to ECOOP workshops recently, they will be up on my website (which I know needs updating) in a week or so, once I have made the suggested changes. The papers are:
OGJ Gone Wild with James Noble at IWACO '09, we use wildcards to mimic the magic 'This' owner in OGJ, thus using only the Java type system (and a couple of coding patterns) to support parametric ownership types.
Comparing Universes and Existential Ownership Types with Werner Dietl at IWACO '09, we show that Universes and a restriction of Jo\exists are equivalent, and thus that the two systems reflect the same underlying hierarchy.
On Subtyping, Wildcards, and Existential Types with Sophia Drossopoulou at FTfJP '09, we use existential types to model both subclassing and wildcards, and show that the two mechanisms can be modelled in a unified way, and that wildcards are a natural mechanism for expressing subtype variance.
OGJ Gone Wild with James Noble at IWACO '09, we use wildcards to mimic the magic 'This' owner in OGJ, thus using only the Java type system (and a couple of coding patterns) to support parametric ownership types.
Comparing Universes and Existential Ownership Types with Werner Dietl at IWACO '09, we show that Universes and a restriction of Jo\exists are equivalent, and thus that the two systems reflect the same underlying hierarchy.
On Subtyping, Wildcards, and Existential Types with Sophia Drossopoulou at FTfJP '09, we use existential types to model both subclassing and wildcards, and show that the two mechanisms can be modelled in a unified way, and that wildcards are a natural mechanism for expressing subtype variance.
Friday, May 01, 2009
Things I like in a programming language
I posted a while back about things I dislike in programming languages, and it was a fairly long list, so in order to appear balanced and not too biased, here is a list of things I like in programming languages (perhaps not all at the same time):
Objects
Classes
Multiple inheritance with traits/mixins
Virtual Classes
Virtual Classes some more (with Tribe typing)
Static types
Dynamic typing
Higher order functions/closures
Readable syntax
Good error messages
Loads of other stuff that I can't think about right now...
Objects
Classes
Multiple inheritance with traits/mixins
Virtual Classes
Virtual Classes some more (with Tribe typing)
Static types
Dynamic typing
Higher order functions/closures
Readable syntax
Good error messages
Loads of other stuff that I can't think about right now...
Wednesday, April 29, 2009
Climbing the Coq learning wall
So I am currently trying to learn Coq, this is a monstrous and Herculean task. It is one of those things where the learning curve is so steep as to deserve a climbing grade (I reckon about v6 for the intersection of the bouldering and PLT communities).
I have the Coq art book winging its way to me, but due to my remote location at the end of the earth (from the perspective of shipping companies, to everyone else I am in the capital of a developed country a days flight from Europe), it hasn't arrive nearly a month after ordering.
But, I Benjamin Pierce teaches a course on Coq and has made the lecture notes (which are all Coq scripts) available online (link is to 07's course schedule which has the whole course, as opposed to the current one):
http://www.seas.upenn.edu/~cis500/cis500-s09/index.html
This is an excellent tutorial for learning Coq from a PLT perspective and I highly recommend it - more so than any of the other Coq resources I've found online.
So, although tough, learning Coq is actually fun, and I hope will be useful. At the moment doing full proofs for a full calculus seems too daunting, but I can see that it is not as bad as some people make out, and hopefully once I have the hang of things will not be too hard. Also seems like a very interesting place to do research - there are so many things crying out to be studied.
I have the Coq art book winging its way to me, but due to my remote location at the end of the earth (from the perspective of shipping companies, to everyone else I am in the capital of a developed country a days flight from Europe), it hasn't arrive nearly a month after ordering.
But, I Benjamin Pierce teaches a course on Coq and has made the lecture notes (which are all Coq scripts) available online (link is to 07's course schedule which has the whole course, as opposed to the current one):
http://www.seas.upenn.edu/~cis500/cis500-s09/index.html
This is an excellent tutorial for learning Coq from a PLT perspective and I highly recommend it - more so than any of the other Coq resources I've found online.
So, although tough, learning Coq is actually fun, and I hope will be useful. At the moment doing full proofs for a full calculus seems too daunting, but I can see that it is not as bad as some people make out, and hopefully once I have the hang of things will not be too hard. Also seems like a very interesting place to do research - there are so many things crying out to be studied.
Friday, April 10, 2009
Busy, busy
Sorry for no ETAPS report thus far. It will be coming soon. I have been very busy, jetting around, having very interesting discussions in London and LA and writing papers for ECOOP workshops. I visited Todd Millstein et al at UCLA and I blog a little about that too, all after easter.
For now I am back in NZ and going to visit Taupo tomorrow morning....
For now I am back in NZ and going to visit Taupo tomorrow morning....
Friday, March 27, 2009
ETAPS 09
So, I've now moved to New Zealand, and in time there will be a post about all that, but right now I am back in the UK, in fact back in York, my childhood home - weirdly this is the longest I've spent in York for about 8 years and I'll have circumnavigated the globe to do it.
Anyway, ETAPS is at York university, which is very pretty - lots of grass and a lake and some ugly old buildings. It also, apparently, has the highest duck to student ratio in the UK. The downside of the venue is that most of us are staying in student halls, which although cheap(-ish) are not particularly luxurious. Pokey is a word that comes to mind - I at first mistook the bathroom for a cupboard. They also have a temporal-tardis-like effect - they appear older on the inside than on the outside!
Anyway, the first two days had interesting sounding talks, but were well outside my area of knowledge and so I gained little. Once ESOP started, however, there were many interesting talks and I will describe these in the following blog posts (over a few days).
Anyway, ETAPS is at York university, which is very pretty - lots of grass and a lake and some ugly old buildings. It also, apparently, has the highest duck to student ratio in the UK. The downside of the venue is that most of us are staying in student halls, which although cheap(-ish) are not particularly luxurious. Pokey is a word that comes to mind - I at first mistook the bathroom for a cupboard. They also have a temporal-tardis-like effect - they appear older on the inside than on the outside!
Anyway, the first two days had interesting sounding talks, but were well outside my area of knowledge and so I gained little. Once ESOP started, however, there were many interesting talks and I will describe these in the following blog posts (over a few days).
Sunday, January 25, 2009
ESOP paper
As I noted below (I think), my supervisor (Sophia) and I have had a paper accepted to ESOP 09 which is in march in York, England. The title is existential quantification for ownership variance and it can be downloaded here.
I'm moving to NZ tomorrow and looking forward to starting some proper research, as opposed to continuously correcting my thesis. Although not looking forward to the 27.5 hr flight so much.
I'm moving to NZ tomorrow and looking forward to starting some proper research, as opposed to continuously correcting my thesis. Although not looking forward to the 27.5 hr flight so much.
Sunday, January 04, 2009
Busy, busy,...
A quick update: on the academic front I have submitted my thesis and passed the viva with minor corrections, which I am working on now. Sophia and I have a paper accepted at ESOP 09 (link coming soon) on existential ownership for variance. Other than that I've been trying to learn Coq, which turns out to be very difficult. On the personal side, I got married and have been busy saying bye-bye to relatives and friends before we head off to NZ; talking of which, I got my visa yesterday, so now all I need to do is finish my thesis corrections and pack.
Subscribe to:
Posts (Atom)