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
Sunday, May 31, 2009
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...
Subscribe to:
Posts (Atom)