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).
No comments:
Post a Comment